(set-logic QF_ABV)
(declare-fun _substvar_423_ () (_ BitVec 32))
(declare-fun _substvar_424_ () (_ BitVec 32))
(declare-fun _substvar_486_ () (_ BitVec 1))
(declare-fun _substvar_529_ () (_ BitVec 1))
(declare-fun _substvar_532_ () (_ BitVec 32))
(declare-fun _substvar_536_ () (_ BitVec 32))
(declare-fun _substvar_538_ () (_ BitVec 32))
(declare-fun _substvar_545_ () (_ BitVec 32))
(declare-fun _substvar_547_ () (_ BitVec 32))
(declare-fun _substvar_550_ () (_ BitVec 32))
(declare-fun _substvar_555_ () (_ BitVec 32))
(declare-fun _substvar_557_ () (_ BitVec 32))
(declare-fun _substvar_560_ () (_ BitVec 1))
(declare-fun _substvar_565_ () (_ BitVec 2))
(declare-fun _substvar_569_ () (_ BitVec 1))
(declare-fun _substvar_570_ () (_ BitVec 32))
(declare-fun _substvar_573_ () (_ BitVec 32))
(declare-fun _substvar_787_ () Bool)
(declare-fun _substvar_823_ () Bool)
(declare-fun _substvar_931_ () (_ BitVec 1))
(declare-fun _substvar_942_ () (_ BitVec 32))
(declare-fun |UNROLL#2334| () (Array (_ BitVec 5) (_ BitVec 32)))
(assert (= (ite _substvar_787_ #b0 _substvar_529_) _substvar_560_))
(define-fun |UNROLL#2376| () (_ BitVec 1) (ite (= ((_ extract 0 0) (ite (= ((_ extract 0 0) _substvar_560_) #b1) #b1 #b0)) #b1) #b1 #b0))
(define-fun |UNROLL#2499| () (_ BitVec 32) (select |UNROLL#2334| ((_ extract 19 15) (ite (= ((_ extract 0 0) (ite (= ((_ extract 0 0) _substvar_560_) #b1) #b1 #b0)) #b1) (_ bv0 32) _substvar_547_))))
(assert (and (= |UNROLL#2376| _substvar_931_) (= |UNROLL#2499| _substvar_424_) (= (ite (= ((_ extract 0 0) (ite (= ((_ extract 0 0) _substvar_560_) #b1) #b1 #b0)) #b1) (_ bv0 32) _substvar_547_) _substvar_423_) true))
(define-fun |UNROLL#3338| () (_ BitVec 32) _substvar_424_)
(assert (and (= _substvar_931_ (_ bv0 1)) (= (concat (_ bv0 1) (ite (= (bvand _substvar_423_ #b00000000000000000000000001001000) #b00000000000000000000000001000000) #b1 #b0)) _substvar_565_) (= |UNROLL#3338| _substvar_550_) true))
(assert (= (ite (not (= ((_ extract 0 0) _substvar_565_) #b1)) #b0 (ite (= _substvar_550_ (_ bv0 32)) #b1 #b0)) _substvar_569_))
(assert (= (ite (= ((_ extract 0 0) (ite (or false false (= ((_ extract 0 0) _substvar_569_) #b1) false) #b1 #b0)) #b1) (_ bv0 32) _substvar_532_) _substvar_573_))
(define-fun |UNROLL#5034| () (_ BitVec 32) _substvar_573_)
(assert (= |UNROLL#5034| _substvar_570_))
(define-fun |UNROLL#5636| () (_ BitVec 32) _substvar_570_)
(assert (= |UNROLL#5636| _substvar_555_))
(define-fun |UNROLL#6191| () (_ BitVec 32) _substvar_555_)
(assert (= |UNROLL#6191| _substvar_545_))
(define-fun |UNROLL#6749| () (_ BitVec 32) _substvar_545_)
(assert (= |UNROLL#6749| _substvar_536_))
(define-fun |UNROLL#7307| () (_ BitVec 32) _substvar_536_)
(assert (= (ite _substvar_823_ #b00000000000000000000000000000000 |UNROLL#7307|) _substvar_942_))
(assert (= _substvar_942_ _substvar_557_))
(define-fun |UNROLL#8423| () (_ BitVec 32) _substvar_557_)
(assert (= |UNROLL#8423| _substvar_538_))
(push 1)
(assert false)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (= (ite (= _substvar_538_ (_ bv0 32)) #b1 #b0) _substvar_486_))
(push 1)
(assert (not (= ((_ extract 0 0) _substvar_486_) #b1)))
(set-info :status sat)
(check-sat)
(exit)