; set_to true (equal)
(define-fun |is_it_friday::1::SECS_DAY!0@1#2| () (_ BitVec 32) (_ bv86400 32))

; set_to true (equal)
(define-fun |is_it_friday::1::dayno!0@1#2| () (_ BitVec 32) (bvudiv |is_it_friday::input!0@1#1| (_ bv86400 32)))

; set_to true (equal)
(define-fun |is_it_friday::1::wday!0@1#2| () (_ BitVec 32) (bvurem (bvadd (_ bv4 32) |is_it_friday::1::dayno!0@1#2|) (_ bv7 32)))