(set-logic QF_ABV)
(declare-fun _substvar_433_ () (_ BitVec 32))
(declare-fun _substvar_434_ () (_ BitVec 32))
(declare-fun _substvar_502_ () (_ BitVec 32))
(declare-fun _substvar_504_ () (_ BitVec 32))
(declare-fun _substvar_507_ () (_ BitVec 32))
(declare-fun _substvar_535_ () (_ BitVec 32))
(declare-fun _substvar_538_ () (_ BitVec 1))
(declare-fun _substvar_545_ () (_ BitVec 2))
(declare-fun _substvar_552_ () (_ BitVec 1))
(declare-fun _substvar_555_ () (_ BitVec 32))
(declare-fun _substvar_559_ () (_ BitVec 32))
(declare-fun _substvar_570_ () (_ BitVec 1))
(declare-fun _substvar_820_ () Bool)
(declare-fun _substvar_823_ () Bool)
(declare-fun _substvar_826_ () Bool)
(declare-fun _substvar_965_ () (_ BitVec 1))
(declare-fun _substvar_1382_ () (_ BitVec 1))
(declare-fun _substvar_1419_ () (_ BitVec 32))
(declare-fun _substvar_1432_ () (_ BitVec 32))
(declare-fun _substvar_1436_ () (_ BitVec 32))
(declare-fun _substvar_1644_ () Bool)
(declare-fun _substvar_2253_ () (_ BitVec 32))
(declare-fun _substvar_3048_ () (_ BitVec 32))
(define-fun |UNROLL#2126| () (_ BitVec 1) (ite _substvar_1644_ #b0 _substvar_1382_))
(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 (= ((_ extract 0 0) _substvar_538_) #b1))
(define-fun |UNROLL#2384| () (_ BitVec 1) (ite |UNROLL#2385| #b1 #b0))
(define-fun |UNROLL#2383| () Bool (= ((_ extract 0 0) |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 (= ((_ extract 0 0) |UNROLL#2426|) #b1))
(define-fun |UNROLL#2424| () (_ BitVec 32) (ite |UNROLL#2425| (_ bv0 32) _substvar_502_))
(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_504_) true))
(assert |UNROLL#2911|)
(define-fun |UNROLL#3845| () Bool (not (= ((_ extract 0 0) _substvar_545_) #b1)))
(define-fun |UNROLL#3849| () Bool (= _substvar_504_ (_ 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 (= ((_ extract 0 0) _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 (= ((_ extract 0 0) |UNROLL#4165|) #b1) (_ bv0 32) _substvar_1419_))
(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_507_))
(assert |UNROLL#5143|)
(define-fun |UNROLL#6191| () (_ BitVec 32) _substvar_507_)
(define-fun |UNROLL#6190| () (_ BitVec 32) (ite _substvar_820_ #b00000000000000000000000000000000 |UNROLL#6191|))
(define-fun |UNROLL#5701| () Bool (= |UNROLL#6190| _substvar_3048_))
(assert |UNROLL#5701|)
(define-fun |UNROLL#6749| () (_ BitVec 32) _substvar_3048_)
(define-fun |UNROLL#6748| () (_ BitVec 32) |UNROLL#6749|)
(define-fun |UNROLL#6259| () Bool (= |UNROLL#6748| _substvar_1432_))
(assert |UNROLL#6259|)
(define-fun |UNROLL#7307| () (_ BitVec 32) _substvar_1432_)
(define-fun |UNROLL#7306| () (_ BitVec 32) (ite _substvar_823_ #b00000000000000000000000000000000 |UNROLL#7307|))
(define-fun |UNROLL#6817| () Bool (= |UNROLL#7306| _substvar_1436_))
(assert |UNROLL#6817|)
(define-fun |UNROLL#7865| () (_ BitVec 32) _substvar_1436_)
(define-fun |UNROLL#7864| () (_ BitVec 32) |UNROLL#7865|)
(define-fun |UNROLL#7375| () Bool (= |UNROLL#7864| _substvar_535_))
(assert |UNROLL#7375|)
(define-fun |UNROLL#8423| () (_ BitVec 32) _substvar_535_)
(define-fun |UNROLL#8422| () (_ BitVec 32) (ite _substvar_826_ #b00000000000000000000000000000000 |UNROLL#8423|))
(define-fun |UNROLL#7933| () Bool (= |UNROLL#8422| _substvar_2253_))
(assert |UNROLL#7933|)
(push 1)
(assert false)
(set-info :status unsat)
(check-sat)
(pop 1)
(define-fun |UNROLL#9005| () Bool (= _substvar_2253_ (_ bv0 32)))
(define-fun |UNROLL#8491| () Bool (= (ite |UNROLL#9005| #b1 #b0) _substvar_965_))
(assert |UNROLL#8491|)
(push 1)
(assert (not (= ((_ extract 0 0) _substvar_965_) #b1)))
(set-info :status sat)
(check-sat)
(exit)