(set-logic QF_ABV)
(declare-fun _substvar_2121_ () (_ BitVec 32))
(declare-fun _substvar_2149_ () (_ BitVec 1))
(declare-fun _substvar_2406_ () (_ BitVec 64))
(declare-fun _substvar_2501_ () (_ BitVec 1))
(declare-fun _substvar_2553_ () (_ BitVec 1))
(declare-fun _substvar_2595_ () (_ BitVec 1))
(declare-fun _substvar_2639_ () (_ BitVec 64))
(declare-fun _substvar_2688_ () (_ BitVec 1))
(declare-fun _substvar_2702_ () (_ BitVec 64))
(declare-fun _substvar_2710_ () (_ BitVec 1))
(declare-fun _substvar_2741_ () (_ BitVec 32))
(declare-fun _substvar_2769_ () (_ BitVec 64))
(declare-fun _substvar_2783_ () (_ BitVec 1))
(declare-fun _substvar_2798_ () (_ BitVec 1))
(declare-fun _substvar_2805_ () (_ BitVec 1))
(declare-fun _substvar_2809_ () (_ BitVec 1))
(declare-fun _substvar_2821_ () (_ BitVec 1))
(declare-fun _substvar_2840_ () (_ BitVec 1))
(declare-fun _substvar_2882_ () (_ BitVec 64))
(declare-fun _substvar_2888_ () (_ BitVec 64))
(declare-fun _substvar_2891_ () (_ BitVec 64))
(declare-fun _substvar_2897_ () (_ BitVec 1))
(declare-fun _substvar_2912_ () (_ BitVec 1))
(declare-fun _substvar_2921_ () (_ BitVec 64))
(declare-fun _substvar_2938_ () (_ BitVec 64))
(declare-fun _substvar_2942_ () (_ BitVec 1))
(declare-fun _substvar_3254_ () Bool)
(declare-fun _substvar_3277_ () Bool)
(declare-fun |UNROLL#4008| () (Array (_ BitVec 5) (_ BitVec 32)))
(define-fun |UNROLL#4173| () (_ BitVec 32) (select |UNROLL#4008| (_ bv0 5)))
(define-fun |UNROLL#4027| () Bool (= |UNROLL#4173| _substvar_2121_))
(assert |UNROLL#4027|)
(define-fun |UNROLL#5012| () (_ BitVec 32) _substvar_2121_)
(define-fun |UNROLL#5011| () (_ BitVec 32) |UNROLL#5012|)
(define-fun |UNROLL#4585| () Bool (= |UNROLL#5011| _substvar_2741_))
(assert |UNROLL#4585|)
(define-fun |UNROLL#5266| () Bool (and (= ((_ extract 0 0) _substvar_2149_) #b1) _substvar_3254_))
(define-fun |UNROLL#5265| () Bool |UNROLL#5266|)
(define-fun |UNROLL#5275| () (_ BitVec 32) (bvadd _substvar_2741_ (_ bv0 32)))
(define-fun |UNROLL#5274| () (_ BitVec 32) (bvadd |UNROLL#5275| (_ bv0 32)))
(define-fun |UNROLL#5279| () Bool (= ((_ extract 0 0) |UNROLL#5274|) #b1))
(define-fun |UNROLL#5270| () Bool (or false false |UNROLL#5279| false))
(define-fun |UNROLL#5269| () Bool (not |UNROLL#5270|))
(define-fun |UNROLL#5264| () Bool (and |UNROLL#5265| |UNROLL#5269|))
(define-fun |UNROLL#5263| () (_ BitVec 1) (ite |UNROLL#5264| #b1 #b0))
(define-fun |UNROLL#5262| () Bool (= ((_ extract 0 0) |UNROLL#5263|) #b1))
(define-fun |UNROLL#5537| () Bool (not |UNROLL#5262|))
(define-fun |UNROLL#5536| () Bool |UNROLL#5537|)
(define-fun |UNROLL#5535| () (_ BitVec 1) (ite |UNROLL#5536| _substvar_2149_ (_ bv0 1)))
(define-fun |UNROLL#5534| () (_ BitVec 1) |UNROLL#5535|)
(define-fun |UNROLL#5548| () Bool |UNROLL#5537|)
(define-fun |UNROLL#5547| () (_ BitVec 1) (ite |UNROLL#5548| #b0 _substvar_2149_))
(define-fun |UNROLL#5545| () (_ BitVec 1) |UNROLL#5547|)
(define-fun |UNROLL#5544| () (_ BitVec 1) |UNROLL#5545|)
(define-fun |UNROLL#5143| () Bool (and (= |UNROLL#5534| _substvar_2805_) (= |UNROLL#5544| _substvar_2821_)))
(assert |UNROLL#5143|)
(define-fun |UNROLL#5768| () Bool (not (= ((_ extract 0 0) _substvar_2821_) #b1)))
(define-fun |UNROLL#5767| () Bool |UNROLL#5768|)
(define-fun |UNROLL#5766| () Bool |UNROLL#5767|)
(define-fun |UNROLL#5765| () (_ BitVec 1) (ite |UNROLL#5766| #b1 #b0))
(define-fun |UNROLL#5730| () (_ BitVec 1) |UNROLL#5765|)
(define-fun |UNROLL#5724| () (_ BitVec 1) |UNROLL#5730|)
(define-fun |UNROLL#5714| () (_ BitVec 1) |UNROLL#5724|)
(define-fun |UNROLL#5712| () (_ BitVec 1) |UNROLL#5714|)
(define-fun |UNROLL#5711| () (_ BitVec 1) |UNROLL#5712|)
(define-fun |UNROLL#6093| () (_ BitVec 1) _substvar_2821_)
(define-fun |UNROLL#6092| () (_ BitVec 1) |UNROLL#6093|)
(define-fun |UNROLL#6146| () (_ BitVec 1) _substvar_2805_)
(define-fun |UNROLL#6145| () (_ BitVec 1) |UNROLL#6146|)
(declare-fun |UNROLL#6240| () (Array (_ BitVec 5) (_ BitVec 32)))
(define-fun |UNROLL#5701| () Bool (and (= |UNROLL#5711| _substvar_2553_) (= |UNROLL#6092| _substvar_2688_) (= |UNROLL#6145| _substvar_2710_)))
(assert |UNROLL#5701|)
(define-fun |UNROLL#6267| () (_ BitVec 1) _substvar_2553_)
(define-fun |UNROLL#6654| () (_ BitVec 1) (ite _substvar_3277_ _substvar_2688_ #b0))
(define-fun |UNROLL#6651| () (_ BitVec 1) |UNROLL#6654|)
(define-fun |UNROLL#6650| () (_ BitVec 1) |UNROLL#6651|)
(define-fun |UNROLL#6719| () (_ BitVec 64) (ite (= ((_ extract 0 0) _substvar_2710_) #b1) _substvar_2882_ (_ bv0 64)))
(define-fun |UNROLL#6718| () (_ BitVec 64) |UNROLL#6719|)
(define-fun |UNROLL#6791| () (Array (_ BitVec 5) (_ BitVec 32)) |UNROLL#6240|)
(declare-fun |UNROLL#6798| () (Array (_ BitVec 5) (_ BitVec 32)))
(define-fun |UNROLL#6259| () Bool (and (= |UNROLL#6267| _substvar_2897_) (= |UNROLL#6650| _substvar_2912_) (= |UNROLL#6718| _substvar_2888_) (= |UNROLL#6791| |UNROLL#6798|)))
(assert |UNROLL#6259|)
(define-fun |UNROLL#6823| () (_ BitVec 1) _substvar_2897_)
(define-fun |UNROLL#7262| () (_ BitVec 1) _substvar_2912_)
(define-fun |UNROLL#7261| () (_ BitVec 1) |UNROLL#7262|)
(define-fun |UNROLL#7344| () Bool (= _substvar_2921_ _substvar_2888_))
(define-fun |UNROLL#6817| () Bool (and (= |UNROLL#6823| _substvar_2840_) (= |UNROLL#7261| _substvar_2595_) (= (ite |UNROLL#7344| #b1 #b0) _substvar_2809_) (= _substvar_2921_ _substvar_2938_)))
(assert |UNROLL#6817|)
(define-fun |UNROLL#7379| () (_ BitVec 1) _substvar_2840_)
(define-fun |UNROLL#7835| () (_ BitVec 64) (ite (= ((_ extract 0 0) _substvar_2595_) #b1) _substvar_2702_ (_ bv0 64)))
(define-fun |UNROLL#7834| () (_ BitVec 64) |UNROLL#7835|)
(define-fun |UNROLL#7375| () Bool (and (= |UNROLL#7379| _substvar_2783_) (= |UNROLL#7834| _substvar_2406_) (= _substvar_2938_ _substvar_2891_)))
(assert |UNROLL#7375|)
(define-fun |UNROLL#8393| () (_ BitVec 64) _substvar_2406_)
(define-fun |UNROLL#8392| () (_ BitVec 64) |UNROLL#8393|)
(define-fun |UNROLL#8404| () (_ BitVec 1) _substvar_2783_)
(define-fun |UNROLL#8418| () Bool (bvult _substvar_2406_ _substvar_2891_))
(define-fun |UNROLL#7933| () Bool (and (= |UNROLL#8392| _substvar_2639_) (= |UNROLL#8404| _substvar_2942_) (= _substvar_2891_ _substvar_2769_)))
(assert |UNROLL#7933|)
(push 1)
(assert false)
(check-sat)
(pop 1)
(define-fun |UNROLL#8480| () Bool true)
(define-fun |UNROLL#8485| () Bool (= ((_ extract 0 0) _substvar_2501_) #b1))
(define-fun |UNROLL#8488| () Bool (= ((_ extract 0 0) _substvar_2798_) #b1))
(define-fun |UNROLL#8479| () Bool (and |UNROLL#8480| |UNROLL#8485| |UNROLL#8488|))
(assert |UNROLL#8479|)
(define-fun |UNROLL#8927| () (_ BitVec 1) (ite (= ((_ extract 0 0) _substvar_2942_) #b1) #b1 (_ bv0 1)))
(define-fun |UNROLL#8926| () (_ BitVec 1) |UNROLL#8927|)
(define-fun |UNROLL#9018| () Bool (= _substvar_2769_ _substvar_2639_))
(define-fun |UNROLL#8491| () Bool (and (= (ite |UNROLL#9018| #b1 #b0) _substvar_2798_) (= |UNROLL#8926| _substvar_2501_)))
(assert |UNROLL#8491|)
(check-sat)
(exit)