(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(set-info :status unsat)
(declare-fun E_26193 ()(_ BitVec 8))
(declare-fun E_26215 ()(_ BitVec 8))
(declare-fun E_26214 ()(_ BitVec 1))
(declare-fun E_26211 ()(_ BitVec 1))
(declare-fun E_26210 ()(_ BitVec 8))
(declare-fun E_26209 ()(_ BitVec 8))
(declare-fun E_26212 ()(_ BitVec 8))
(declare-fun E_26205 ()(_ BitVec 8))
(declare-fun E_26204 ()(_ BitVec 24))
(declare-fun E_26206 ()(_ BitVec 32))
(declare-fun E_26207 ()(_ BitVec 8))
(declare-fun E_26203 ()(_ BitVec 4))
(declare-fun E_26208 ()(_ BitVec 8))
(declare-fun E_26213 ()(_ BitVec 8))
(declare-fun E_26200 ()(_ BitVec 8))
(declare-fun E_26201 ()(_ BitVec 8))
(declare-fun E_26196 ()(_ BitVec 8))
(declare-fun E_26195 ()(_ BitVec 24))
(declare-fun E_26197 ()(_ BitVec 32))
(declare-fun E_26198 ()(_ BitVec 8))
(declare-fun E_26194 ()(_ BitVec 4))
(declare-fun E_26199 ()(_ BitVec 8))
(declare-fun E_26202 ()(_ BitVec 8))
(declare-fun E_26192 ()(_ BitVec 8))
(declare-fun E_26189 ()(_ BitVec 1))
(declare-fun E_26188 ()(_ BitVec 4))
(declare-fun E_26190 ()(_ BitVec 5))
(declare-fun E_26191 ()(_ BitVec 5))
(assert  (=  (bvnot   E_26214)  E_26211))
(assert  (=  (ite  (=  (_ bv1 1)  E_26211)  E_26209  E_26210)  E_26212))
(assert  (=  (concat  E_26204  E_26205)  E_26206))
(assert  (=  ((_ extract 7 0) E_26206)  E_26207))
(assert  (=  (ite  (=  (_ bv1 1)  E_26211) ((_ zero_extend 4) E_26203)  E_26207)  E_26208))
(assert  (=  (bvsub   E_26212  E_26208)  E_26213))
(assert  (=  (ite  (=  (_ bv1 1)  E_26214)  E_26209  E_26200)  E_26201))
(assert  (=  (concat  E_26195  E_26196)  E_26197))
(assert  (=  ((_ extract 7 0) E_26197)  E_26198))
(assert  (=  (ite  (=  (_ bv1 1)  E_26214) ((_ zero_extend 4) E_26194)  E_26198)  E_26199))
(assert  (=  (bvadd   E_26201  E_26199)  E_26202))
(assert  (=  (ite  (=  (_ bv1 1)  E_26214)  E_26202  E_26213)  E_26215))
(assert  (=  (bvadd   E_26209 ((_ zero_extend 7) E_26211))  E_26192))
(assert  (=   #b1  E_26189))
(assert  (=  (ite  (=  (_ bv1 1)  E_26214)  E_26194  E_26203)  E_26188))
(assert  (=  (bvsub  ((_ sign_extend 4) E_26189) ((_ zero_extend 1) E_26188))  E_26190))
(assert  (=  (ite  (=  (_ bv1 1)  E_26214) ((_ zero_extend 1) E_26194)  E_26190)  E_26191))
(assert  (=  ((_ extract 7 0)(bvadd  ((_ zero_extend 1) E_26192) ((_ sign_extend 4) E_26191)))  E_26193))
(assert  (=  (bvcomp   E_26193  E_26215) (_ bv0 1)))
(check-sat)
(exit)