(define c3967452::bool true)
(define c6235236::(bitvector 8) (mk-bv 8 0))
(define v11238708::(bitvector 8))
(define o11096724::bool (= c6235236 v11238708))
(define o11025272::bool (and o11096724 c3967452))
(define v11022668::(bitvector 32))
(define v11076860::(bitvector 32))
(define o11052260::bool (= v11022668 v11076860))
(define o11172524::bool (and o11025272 o11052260))
(define o11176208::bool (ite o11096724 o11172524 c3967452))
(define v11111308::(bitvector 8))
(define o11175408::bool (= v11111308 c6235236))
(define o11002432::bool (and o11175408 c3967452))
(define o11045532::bool (and o11176208 o11002432))
(define c3958328::(bitvector 32) (mk-bv 32 0))
(define v11247560::(bitvector 32))
(define o11245476::bool (/= c3958328 v11247560))
(define o4247164::bool (or o11045532 o11245476))
(define o11235472::bool (/= c3967452 o4247164))

(assert o11235472)
(check)
(show-model)

(eval o11235472)
(eval o4247164)
(eval o11245476)
(eval c3958328)
(eval o11045532)
(eval o11175408)
(eval o11176208)
(eval o11172524)
(eval o11052260)
(eval o11052260)
(eval o11025272)
(eval o11096724)
(eval c6235236)
(eval c3967452)