(set-logic QF_ABV)
(declare-fun _substvar_38_ () (_ BitVec 64))
(declare-fun _substvar_39_ () (_ BitVec 1))
(declare-fun _substvar_72_ () (_ BitVec 64))
(assert (= _substvar_72_ _substvar_38_))
(define-fun |UNROLL#7933| () Bool (and true (= (_ bv0 1) _substvar_39_) (= _substvar_38_ (_ bv0 64))))
(push 1)
(assert false)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (= (ite (= _substvar_39_ #b1) #b1 (_ bv0 1)) (_ bv0 1)))
(set-info :status sat)
(check-sat)
(exit)