; set_to true (equal)
(define-fun |lets_party::1::SECS_HOUR!0@1#2| () (_ BitVec 32) (_ bv3600 32))

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

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

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

; set_to true (equal)
(define-fun |lets_party::1::1::hour!0@1#2| () (_ BitVec 32) (bvudiv (bvurem |lets_party::input!0@1#1| (_ bv86400 32)) (_ bv3600 32)))