(set-logic QF_ABV)
(declare-fun _substvar_944_ () (_ BitVec 1))
(declare-fun _substvar_957_ () (_ BitVec 32))
(declare-fun _substvar_958_ () (_ BitVec 32))
(declare-fun _substvar_978_ () (_ BitVec 1))
(declare-fun _substvar_1053_ () (_ BitVec 32))
(declare-fun _substvar_1055_ () (_ BitVec 32))
(declare-fun _substvar_1056_ () (_ BitVec 1))
(declare-fun _substvar_1057_ () (_ BitVec 1))
(declare-fun _substvar_1060_ () (_ BitVec 64))
(declare-fun _substvar_1061_ () (_ BitVec 1))
(declare-fun _substvar_1065_ () (_ BitVec 64))
(declare-fun _substvar_1067_ () (_ BitVec 64))
(declare-fun _substvar_1069_ () (_ BitVec 64))
(declare-fun _substvar_1070_ () (_ BitVec 1))
(declare-fun _substvar_1074_ () (_ BitVec 64))
(declare-fun _substvar_1075_ () (_ BitVec 32))
(declare-fun _substvar_1080_ () (_ BitVec 1))
(declare-fun _substvar_1136_ () (_ BitVec 1))
(declare-fun _substvar_1164_ () (_ BitVec 1))
(declare-fun _substvar_1168_ () (_ BitVec 1))
(declare-fun _substvar_1170_ () (_ BitVec 1))
(declare-fun _substvar_1171_ () (_ BitVec 1))
(declare-fun _substvar_1174_ () (_ BitVec 1))
(declare-fun _substvar_1179_ () (_ BitVec 1))
(declare-fun _substvar_1181_ () (_ BitVec 1))
(declare-fun _substvar_1184_ () (_ BitVec 1))
(declare-fun _substvar_1186_ () (_ BitVec 1))
(declare-fun _substvar_1187_ () (_ BitVec 1))
(declare-fun _substvar_1188_ () (_ BitVec 1))
(declare-fun _substvar_1409_ () Bool)
(declare-fun _substvar_1820_ () Bool)
(declare-fun _substvar_1823_ () Bool)
(declare-fun |UNROLL#4566| () (Array (_ BitVec 5) (_ BitVec 32)))
(define-fun |UNROLL#4617| () Bool (and _substvar_1823_ _substvar_1820_))
(define-fun |UNROLL#4616| () (_ BitVec 1) (ite |UNROLL#4617| #b1 #b0))
(define-fun |UNROLL#4615| () Bool (= ((_ extract 0 0) |UNROLL#4616|) #b1))
(define-fun |UNROLL#4649| () (_ BitVec 1) #b1)
(define-fun |UNROLL#4614| () (_ BitVec 1) (ite |UNROLL#4615| |UNROLL#4649| #b0))
(define-fun |UNROLL#4608| () (_ BitVec 1) |UNROLL#4614|)
(define-fun |UNROLL#4598| () (_ BitVec 1) |UNROLL#4608|)
(define-fun |UNROLL#4596| () (_ BitVec 1) |UNROLL#4598|)
(define-fun |UNROLL#4595| () (_ BitVec 1) |UNROLL#4596|)
(define-fun |UNROLL#4658| () (_ BitVec 1) |UNROLL#4616|)
(define-fun |UNROLL#4657| () Bool (= ((_ extract 0 0) |UNROLL#4658|) #b1))
(define-fun |UNROLL#4656| () (_ BitVec 32) (ite |UNROLL#4657| _substvar_1053_ (_ bv0 32)))
(define-fun |UNROLL#4655| () (_ BitVec 5) ((_ extract 24 20) |UNROLL#4656|))
(define-fun |UNROLL#4654| () (_ BitVec 32) (select |UNROLL#4566| |UNROLL#4655|))
(define-fun |UNROLL#4585| () Bool (and (= |UNROLL#4595| _substvar_1188_) (= |UNROLL#4654| _substvar_1075_)))
(assert |UNROLL#4585|)
(define-fun |UNROLL#5151| () (_ BitVec 1) _substvar_1188_)
(define-fun |UNROLL#5562| () (_ BitVec 32) _substvar_1075_)
(define-fun |UNROLL#5561| () (_ BitVec 32) |UNROLL#5562|)
(define-fun |UNROLL#5143| () Bool (and (= |UNROLL#5151| _substvar_1056_) (= |UNROLL#5561| _substvar_1055_)))
(assert |UNROLL#5143|)
(define-fun |UNROLL#5707| () (_ BitVec 1) _substvar_1056_)
(define-fun |UNROLL#5834| () (_ BitVec 32) _substvar_1055_)
(define-fun |UNROLL#5833| () (_ BitVec 32) (bvadd (_ bv0 32) |UNROLL#5834|))
(define-fun |UNROLL#5832| () (_ BitVec 32) (bvadd |UNROLL#5833| (_ bv0 32)))
(define-fun |UNROLL#5837| () Bool (= ((_ extract 0 0) |UNROLL#5832|) #b1))
(define-fun |UNROLL#5828| () Bool (or false false |UNROLL#5837| false))
(define-fun |UNROLL#5827| () Bool (not |UNROLL#5828|))
(define-fun |UNROLL#5822| () Bool |UNROLL#5827|)
(define-fun |UNROLL#5821| () (_ BitVec 1) (ite |UNROLL#5822| #b1 #b0))
(define-fun |UNROLL#5820| () Bool (= ((_ extract 0 0) |UNROLL#5821|) #b1))
(define-fun |UNROLL#5773| () Bool (or false false |UNROLL#5820| false))
(define-fun |UNROLL#6038| () Bool (not |UNROLL#5773|))
(define-fun |UNROLL#6104| () Bool |UNROLL#6038|)
(define-fun |UNROLL#6103| () (_ BitVec 1) (ite |UNROLL#6104| (_ bv0 1) _substvar_1170_))
(define-fun |UNROLL#6102| () (_ BitVec 1) |UNROLL#6103|)
(define-fun |UNROLL#5701| () Bool (and (= |UNROLL#5707| _substvar_944_) true (= |UNROLL#6102| _substvar_1070_) true))
(assert |UNROLL#5701|)
(define-fun |UNROLL#6263| () (_ BitVec 1) _substvar_944_)
(define-fun |UNROLL#6382| () Bool (= ((_ extract 0 0) _substvar_1070_) #b1))
(define-fun |UNROLL#6381| () Bool |UNROLL#6382|)
(define-fun |UNROLL#6380| () Bool |UNROLL#6381|)
(define-fun |UNROLL#6379| () (_ BitVec 1) (ite |UNROLL#6380| #b1 #b0))
(define-fun |UNROLL#6378| () Bool (= ((_ extract 0 0) |UNROLL#6379|) #b1))
(define-fun |UNROLL#6685| () (_ BitVec 32) (ite |UNROLL#6378| (_ bv0 32) _substvar_957_))
(define-fun |UNROLL#6259| () Bool (and (= |UNROLL#6263| _substvar_1136_) true true true (= |UNROLL#6685| _substvar_958_)))
(assert |UNROLL#6259|)
(define-fun |UNROLL#6949| () (_ BitVec 32) (bvadd _substvar_958_ (_ bv0 32)))
(define-fun |UNROLL#6948| () (_ BitVec 32) (bvadd |UNROLL#6949| (_ bv0 32)))
(define-fun |UNROLL#6947| () Bool (= ((_ extract 0 0) |UNROLL#6948|) #b1))
(define-fun |UNROLL#6945| () Bool |UNROLL#6947|)
(define-fun |UNROLL#6944| () Bool |UNROLL#6945|)
(define-fun |UNROLL#7214| () (_ BitVec 1) (ite |UNROLL#6944| #b1 #b0))
(define-fun |UNROLL#7288| () (_ BitVec 1) _substvar_1136_)
(define-fun |UNROLL#6817| () Bool (and true (= |UNROLL#7214| _substvar_978_) true true (= |UNROLL#7288| _substvar_1080_)))
(assert |UNROLL#6817|)
(define-fun |UNROLL#7392| () (_ BitVec 1) _substvar_978_)
(define-fun |UNROLL#7391| () Bool (= ((_ extract 0 0) |UNROLL#7392|) #b1))
(define-fun |UNROLL#7519| () (_ BitVec 1) (ite |UNROLL#7391| #b1 #b0))
(define-fun |UNROLL#7513| () (_ BitVec 1) |UNROLL#7519|)
(define-fun |UNROLL#7812| () (_ BitVec 1) (ite (= ((_ extract 0 0) _substvar_1080_) #b1) #b1 #b0))
(define-fun |UNROLL#7809| () Bool (= ((_ extract 0 0) |UNROLL#7812|) #b1))
(define-fun |UNROLL#7808| () (_ BitVec 1) (ite |UNROLL#7809| #b1 (_ bv0 1)))
(define-fun |UNROLL#7807| () (_ BitVec 1) |UNROLL#7808|)
(define-fun |UNROLL#7820| () (_ BitVec 1) (ite (= ((_ extract 0 0) |UNROLL#7513|) #b1) #b0 _substvar_1168_))
(define-fun |UNROLL#7819| () (_ BitVec 1) |UNROLL#7820|)
(define-fun |UNROLL#7375| () Bool (and true true (= |UNROLL#7807| _substvar_1186_) (= |UNROLL#7819| _substvar_1171_) (= _substvar_1067_ _substvar_1060_)))
(assert |UNROLL#7375|)
(define-fun |UNROLL#8369| () (_ BitVec 1) _substvar_1171_)
(define-fun |UNROLL#8368| () (_ BitVec 1) |UNROLL#8369|)
(define-fun |UNROLL#8366| () (_ BitVec 1) _substvar_1186_)
(define-fun |UNROLL#8365| () (_ BitVec 1) |UNROLL#8366|)
(define-fun |UNROLL#8393| () (_ BitVec 64) (ite (= ((_ extract 0 0) _substvar_1171_) #b1) (_ bv0 64) _substvar_1069_))
(define-fun |UNROLL#8392| () (_ BitVec 64) |UNROLL#8393|)
(define-fun |UNROLL#8418| () Bool (bvult _substvar_1069_ _substvar_1060_))
(define-fun |UNROLL#8417| () Bool (and (= ((_ extract 0 0) |UNROLL#8368|) #b1) |UNROLL#8418|))
(define-fun |UNROLL#8416| () Bool |UNROLL#8417|)
(define-fun |UNROLL#8415| () (_ BitVec 1) (ite |UNROLL#8416| #b1 _substvar_1057_))
(define-fun |UNROLL#8413| () (_ BitVec 1) |UNROLL#8415|)
(define-fun |UNROLL#8410| () (_ BitVec 1) |UNROLL#8413|)
(define-fun |UNROLL#7933| () Bool (and (= |UNROLL#8365| _substvar_1164_) true (= |UNROLL#8392| _substvar_1065_) true (= |UNROLL#8410| _substvar_1061_) (= _substvar_1060_ _substvar_1074_)))
(assert |UNROLL#7933|)
(push 1)
(assert false)
(set-info :status unsat)
(check-sat)
(pop 1)
(define-fun |UNROLL#8485| () Bool (= ((_ extract 0 0) _substvar_1181_) #b1))
(define-fun |UNROLL#8488| () Bool (or (= ((_ extract 0 0) _substvar_1187_) #b1) (not (= ((_ extract 0 0) _substvar_1184_) #b1))))
(define-fun |UNROLL#8479| () Bool (and |UNROLL#8485| |UNROLL#8488|))
(assert |UNROLL#8479|)
(define-fun |UNROLL#8926| () (_ BitVec 1) (ite (= ((_ extract 0 0) _substvar_1164_) #b1) #b0 _substvar_1174_))
(define-fun |UNROLL#9001| () Bool (= ((_ extract 0 0) _substvar_1061_) #b1))
(define-fun |UNROLL#9000| () (_ BitVec 1) (ite |UNROLL#9001| #b1 #b0))
(define-fun |UNROLL#8999| () (_ BitVec 1) |UNROLL#9000|)
(define-fun |UNROLL#8998| () (_ BitVec 1) |UNROLL#8999|)
(define-fun |UNROLL#9018| () Bool (= _substvar_1074_ _substvar_1065_))
(define-fun |UNROLL#9020| () (_ BitVec 1) #b1)
(define-fun |UNROLL#9019| () (_ BitVec 1) |UNROLL#9020|)
(define-fun |UNROLL#8491| () Bool (and (= |UNROLL#8998| _substvar_1179_) true (= (ite |UNROLL#9018| #b1 #b0) _substvar_1187_) (= |UNROLL#9019| _substvar_1184_) (= |UNROLL#8926| _substvar_1181_)))
(assert |UNROLL#8491|)
(push 1)
(define-fun |UNROLL#9033| () Bool (or _substvar_1409_ (not (= _substvar_1179_ #b1))))
(assert (not |UNROLL#9033|))
(set-info :status sat)
(check-sat)
(exit)