(set-logic QF_ABV)
(declare-fun _substvar_433_ () (_ BitVec 32))
(declare-fun _substvar_434_ () (_ BitVec 32))
(declare-fun _substvar_493_ () (_ BitVec 32))
(declare-fun _substvar_503_ () (_ BitVec 32))
(declare-fun _substvar_505_ () (_ BitVec 32))
(declare-fun _substvar_508_ () (_ BitVec 32))
(declare-fun _substvar_535_ () (_ BitVec 32))
(declare-fun _substvar_538_ () (_ BitVec 1))
(declare-fun _substvar_541_ () (_ BitVec 1))
(declare-fun _substvar_545_ () (_ BitVec 2))
(declare-fun _substvar_548_ () (_ BitVec 32))
(declare-fun _substvar_552_ () (_ BitVec 1))
(declare-fun _substvar_555_ () (_ BitVec 32))
(declare-fun _substvar_559_ () (_ BitVec 32))
(declare-fun _substvar_560_ () (_ BitVec 32))
(declare-fun _substvar_564_ () (_ BitVec 1))
(declare-fun _substvar_570_ () (_ BitVec 1))
(declare-fun _substvar_788_ () Bool)
(declare-fun _substvar_820_ () Bool)
(declare-fun _substvar_823_ () Bool)
(declare-fun _substvar_826_ () Bool)
(declare-fun _substvar_1397_ () (_ BitVec 32))
(declare-fun _substvar_1402_ () (_ BitVec 32))
(define-fun |UNROLL#2126| () (_ BitVec 1) (ite _substvar_788_ #b0 _substvar_564_))
(declare-fun |UNROLL#2334| () (Array (_ BitVec 5) (_ BitVec 32)))
(define-fun |UNROLL#1795| () Bool (= |UNROLL#2126| _substvar_538_))
(assert |UNROLL#1795|)
(define-fun |UNROLL#2385| () Bool (= _substvar_538_ #b1))
(define-fun |UNROLL#2384| () (_ BitVec 1) (ite |UNROLL#2385| #b1 #b0))
(define-fun |UNROLL#2383| () Bool (= |UNROLL#2384| #b1))
(define-fun |UNROLL#2417| () (_ BitVec 1) #b1)
(define-fun |UNROLL#2382| () (_ BitVec 1) (ite |UNROLL#2383| |UNROLL#2417| #b0))
(define-fun |UNROLL#2376| () (_ BitVec 1) |UNROLL#2382|)
(define-fun |UNROLL#2366| () (_ BitVec 1) |UNROLL#2376|)
(define-fun |UNROLL#2364| () (_ BitVec 1) |UNROLL#2366|)
(define-fun |UNROLL#2363| () (_ BitVec 1) |UNROLL#2364|)
(define-fun |UNROLL#2426| () (_ BitVec 1) |UNROLL#2384|)
(define-fun |UNROLL#2425| () Bool (= |UNROLL#2426| #b1))
(define-fun |UNROLL#2424| () (_ BitVec 32) (ite |UNROLL#2425| (_ bv0 32) _substvar_503_))
(define-fun |UNROLL#2500| () (_ BitVec 5) ((_ extract 19 15) |UNROLL#2424|))
(define-fun |UNROLL#2499| () (_ BitVec 32) (select |UNROLL#2334| |UNROLL#2500|))
(define-fun |UNROLL#2353| () Bool (and (= |UNROLL#2363| _substvar_570_) (= |UNROLL#2499| _substvar_434_) (= |UNROLL#2424| _substvar_433_) true))
(assert |UNROLL#2353|)
(define-fun |UNROLL#2919| () (_ BitVec 1) _substvar_570_)
(define-fun |UNROLL#3070| () (_ BitVec 32) (bvand _substvar_433_ #b00000000000000000000000001001000))
(define-fun |UNROLL#3069| () Bool (= |UNROLL#3070| #b00000000000000000000000001000000))
(define-fun |UNROLL#3063| () (_ BitVec 2) (concat (_ bv0 1) (ite |UNROLL#3069| #b1 #b0)))
(define-fun |UNROLL#3338| () (_ BitVec 32) _substvar_434_)
(define-fun |UNROLL#3337| () (_ BitVec 32) |UNROLL#3338|)
(define-fun |UNROLL#2911| () Bool (and (= |UNROLL#2919| (_ bv0 1)) (= |UNROLL#3063| _substvar_545_) (= |UNROLL#3337| _substvar_505_) true))
(assert |UNROLL#2911|)
(define-fun |UNROLL#3845| () Bool (not (= ((_ extract 0 0) _substvar_545_) #b1)))
(define-fun |UNROLL#3849| () Bool (= _substvar_505_ (_ bv0 32)))
(define-fun |UNROLL#3847| () (_ BitVec 1) (ite |UNROLL#3849| #b1 #b0))
(define-fun |UNROLL#3844| () (_ BitVec 1) (ite |UNROLL#3845| #b0 |UNROLL#3847|))
(define-fun |UNROLL#3843| () (_ BitVec 1) |UNROLL#3844|)
(define-fun |UNROLL#3469| () Bool (= |UNROLL#3843| _substvar_552_))
(assert |UNROLL#3469|)
(define-fun |UNROLL#4047| () Bool (= _substvar_552_ #b1))
(define-fun |UNROLL#4046| () Bool |UNROLL#4047|)
(define-fun |UNROLL#4043| () Bool (or false false |UNROLL#4046| false))
(define-fun |UNROLL#4171| () (_ BitVec 1) (ite |UNROLL#4043| #b1 #b0))
(define-fun |UNROLL#4165| () (_ BitVec 1) |UNROLL#4171|)
(define-fun |UNROLL#4188| () (_ BitVec 32) (ite (= |UNROLL#4165| #b1) (_ bv0 32) _substvar_493_))
(define-fun |UNROLL#4027| () Bool (= |UNROLL#4188| _substvar_559_))
(assert |UNROLL#4027|)
(define-fun |UNROLL#5034| () (_ BitVec 32) _substvar_559_)
(define-fun |UNROLL#5033| () (_ BitVec 32) |UNROLL#5034|)
(define-fun |UNROLL#4585| () Bool (= |UNROLL#5033| _substvar_555_))
(assert |UNROLL#4585|)
(define-fun |UNROLL#5636| () (_ BitVec 32) _substvar_555_)
(define-fun |UNROLL#5635| () (_ BitVec 32) |UNROLL#5636|)
(define-fun |UNROLL#5634| () (_ BitVec 32) |UNROLL#5635|)
(define-fun |UNROLL#5633| () (_ BitVec 32) |UNROLL#5634|)
(define-fun |UNROLL#5632| () (_ BitVec 32) |UNROLL#5633|)
(define-fun |UNROLL#5143| () Bool (= |UNROLL#5632| _substvar_508_))
(assert |UNROLL#5143|)
(define-fun |UNROLL#6191| () (_ BitVec 32) _substvar_508_)
(define-fun |UNROLL#6190| () (_ BitVec 32) (ite _substvar_820_ #b00000000000000000000000000000000 |UNROLL#6191|))
(define-fun |UNROLL#5701| () Bool (= |UNROLL#6190| _substvar_1397_))
(assert |UNROLL#5701|)
(define-fun |UNROLL#6749| () (_ BitVec 32) _substvar_1397_)
(define-fun |UNROLL#6748| () (_ BitVec 32) |UNROLL#6749|)
(define-fun |UNROLL#6259| () Bool (= |UNROLL#6748| _substvar_548_))
(assert |UNROLL#6259|)
(define-fun |UNROLL#7307| () (_ BitVec 32) _substvar_548_)
(define-fun |UNROLL#7306| () (_ BitVec 32) (ite _substvar_823_ #b00000000000000000000000000000000 |UNROLL#7307|))
(define-fun |UNROLL#6817| () Bool (= |UNROLL#7306| _substvar_1402_))
(assert |UNROLL#6817|)
(define-fun |UNROLL#7865| () (_ BitVec 32) _substvar_1402_)
(define-fun |UNROLL#7864| () (_ BitVec 32) |UNROLL#7865|)
(define-fun |UNROLL#7375| () Bool (= |UNROLL#7864| _substvar_535_))
(assert |UNROLL#7375|)
(assert (= (ite _substvar_826_ #b00000000000000000000000000000000 _substvar_535_) _substvar_560_))

(push 1)
(assert false)
(check-sat)
(pop 1)

(assert (= (= _substvar_560_ (_ bv0 32)) _substvar_541_))
(push 1)
(assert (not (= _substvar_560_ (_ bv0 32))))
(check-sat)
(exit)