(set-logic QF_ABV)
(declare-fun _substvar_2495_ () (_ BitVec 32))
(declare-fun _substvar_3015_ () (_ BitVec 32))
(declare-fun _substvar_3127_ () (_ BitVec 32))
(declare-fun _substvar_3228_ () (_ BitVec 1))
(declare-fun _substvar_3286_ () (_ BitVec 1))
(declare-fun _substvar_3390_ () (_ BitVec 2))
(declare-fun _substvar_3425_ () (_ BitVec 32))
(declare-fun _substvar_3465_ () (_ BitVec 1))
(declare-fun _substvar_3466_ () (_ BitVec 32))
(declare-fun _substvar_3481_ () (_ BitVec 32))
(declare-fun _substvar_3496_ () (_ BitVec 32))
(declare-fun _substvar_3573_ () (_ BitVec 1))
(declare-fun _substvar_3618_ () (_ BitVec 32))
(declare-fun _substvar_3659_ () (_ BitVec 32))
(declare-fun _substvar_3756_ () (_ BitVec 1))
(declare-fun _substvar_3759_ () (_ BitVec 32))
(declare-fun _substvar_3769_ () (_ BitVec 32))
(declare-fun _substvar_3797_ () (_ BitVec 32))
(declare-fun _substvar_4098_ () Bool)
(declare-fun _substvar_4136_ () Bool)
(declare-fun _substvar_4142_ () Bool)
(declare-fun _substvar_4148_ () Bool)
(declare-fun _substvar_4241_ () (_ BitVec 32))
(define-fun |UNROLL#2126| () (_ BitVec 1) (ite _substvar_4098_ #b0 _substvar_3573_))
(declare-fun |UNROLL#2334| () (Array (_ BitVec 5) (_ BitVec 32)))
(define-fun |UNROLL#1795| () Bool (and (= |UNROLL#2126| _substvar_3228_) true))
(assert |UNROLL#1795|)
(define-fun |UNROLL#2385| () Bool (= ((_ extract 0 0) _substvar_3228_) #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_3015_))
(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_3756_) (= |UNROLL#2499| _substvar_3659_) (= |UNROLL#2424| _substvar_3618_) true))
(assert |UNROLL#2353|)
(define-fun |UNROLL#2919| () (_ BitVec 1) _substvar_3756_)
(define-fun |UNROLL#3070| () (_ BitVec 32) (bvand _substvar_3618_ #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_3659_)
(define-fun |UNROLL#3337| () (_ BitVec 32) |UNROLL#3338|)
(define-fun |UNROLL#2911| () Bool (and (= |UNROLL#2919| (_ bv0 1)) (= |UNROLL#3063| _substvar_3390_) (= |UNROLL#3337| _substvar_4241_) true))
(assert |UNROLL#2911|)
(define-fun |UNROLL#3845| () Bool (not (= ((_ extract 0 0) _substvar_3390_) #b1)))
(define-fun |UNROLL#3849| () Bool (= _substvar_4241_ (_ 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 (and (= |UNROLL#3843| _substvar_3465_) true))
(assert |UNROLL#3469|)
(define-fun |UNROLL#4047| () Bool (= ((_ extract 0 0) _substvar_3465_) #b1))
(define-fun |UNROLL#4048| () Bool true)
(define-fun |UNROLL#4046| () Bool (and |UNROLL#4047| |UNROLL#4048|))
(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_3769_))
(define-fun |UNROLL#4027| () Bool (and (= |UNROLL#4188| _substvar_3481_) true))
(assert |UNROLL#4027|)
(define-fun |UNROLL#5034| () (_ BitVec 32) _substvar_3481_)
(define-fun |UNROLL#5033| () (_ BitVec 32) |UNROLL#5034|)
(define-fun |UNROLL#4585| () Bool (and (= |UNROLL#5033| _substvar_3466_) true))
(assert |UNROLL#4585|)
(define-fun |UNROLL#5636| () (_ BitVec 32) _substvar_3466_)
(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 (and (= |UNROLL#5632| _substvar_2495_) true))
(assert |UNROLL#5143|)
(define-fun |UNROLL#6191| () (_ BitVec 32) _substvar_2495_)
(define-fun |UNROLL#6190| () (_ BitVec 32) (ite _substvar_4136_ #b00000000000000000000000000000000 |UNROLL#6191|))
(define-fun |UNROLL#5701| () Bool (and (= |UNROLL#6190| _substvar_3797_) true))
(assert |UNROLL#5701|)
(define-fun |UNROLL#6749| () (_ BitVec 32) _substvar_3797_)
(define-fun |UNROLL#6748| () (_ BitVec 32) |UNROLL#6749|)
(define-fun |UNROLL#6259| () Bool (and (= |UNROLL#6748| _substvar_3425_) true))
(assert |UNROLL#6259|)
(define-fun |UNROLL#7307| () (_ BitVec 32) _substvar_3425_)
(define-fun |UNROLL#7306| () (_ BitVec 32) (ite _substvar_4142_ #b00000000000000000000000000000000 |UNROLL#7307|))
(define-fun |UNROLL#6817| () Bool (and (= |UNROLL#7306| _substvar_3759_) true))
(assert |UNROLL#6817|)
(define-fun |UNROLL#7865| () (_ BitVec 32) _substvar_3759_)
(define-fun |UNROLL#7864| () (_ BitVec 32) |UNROLL#7865|)
(define-fun |UNROLL#7375| () Bool (and (= |UNROLL#7864| _substvar_3127_) true))
(assert |UNROLL#7375|)
(define-fun |UNROLL#8423| () (_ BitVec 32) _substvar_3127_)
(define-fun |UNROLL#8422| () (_ BitVec 32) (ite _substvar_4148_ #b00000000000000000000000000000000 |UNROLL#8423|))
(define-fun |UNROLL#7933| () Bool (and (= |UNROLL#8422| _substvar_3496_) true))
(assert |UNROLL#7933|)
(push 1)
(assert false)
(set-info :status unsat)
(check-sat)
(pop 1)
(define-fun |UNROLL#9005| () Bool (= _substvar_3496_ (_ bv0 32)))
(define-fun |UNROLL#8491| () Bool (and (= (ite |UNROLL#9005| #b1 #b0) _substvar_3286_) true))
(assert |UNROLL#8491|)
(push 1)
(assert (not (= ((_ extract 0 0) _substvar_3286_) #b1)))
(set-info :status sat)
(check-sat)
(exit)