(set-option :incremental false)
(set-info :status sat)
(set-logic QF_BV)
(declare-fun v5 () (_ BitVec 4))
(declare-fun v0 () (_ BitVec 4))
(declare-fun v8 () (_ BitVec 4))
(declare-fun v3 () (_ BitVec 4))
(declare-fun v2 () (_ BitVec 4))
(declare-fun v6 () (_ BitVec 4))
(declare-fun v1 () (_ BitVec 4))
(check-sat-assuming ( (let ((_let_0 (bvlshr v1 (bvand (_ bv4 4) v3)))) (let ((_let_1 (ite (bvugt _let_0 ((_ zero_extend 3) (ite (bvslt (_ bv4 4) v2) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (let ((_let_2 ((_ zero_extend 3) (ite (bvsle (_ bv0 4) v1) (_ bv1 1) (_ bv0 1))))) (let ((_let_3 (ite (bvuge v1 v6) (_ bv1 1) (_ bv0 1)))) (let ((_let_4 (ite (= (_ bv1 1) _let_3) (_ bv1 4) (_ bv0 4)))) (let ((_let_5 (bvshl (_ bv4 4) v1))) (let ((_let_6 (bvnot v5))) (let ((_let_7 (bvadd (_ bv1 4) (_ bv1 4)))) (and (bvsge ((_ zero_extend 3) (ite (bvule (ite (= (_ bv1 1) ((_ extract 1 1) v2)) (_ bv4 4) (bvsub (bvadd v1 v6) v6)) v2) (_ bv1 1) (_ bv0 1))) (_ bv1 4)) (or false (bvugt (_ bv1 4) ((_ sign_extend 3) (ite (bvsge (_ bv0 4) ((_ zero_extend 3) _let_1)) (_ bv1 1) (_ bv0 1)))) (bvslt ((_ zero_extend 3) (ite (bvslt (_ bv0 4) _let_2) (_ bv1 1) (_ bv0 1))) (_ bv1 4))) (or false (bvule ((_ zero_extend 3) (ite (bvule ((_ sign_extend 3) (ite (bvuge v0 v6) (_ bv1 1) (_ bv0 1))) (_ bv0 4)) (_ bv1 1) (_ bv0 1))) (_ bv0 4)) (not (bvsge _let_4 (_ bv0 4)))) (bvule _let_5 (_ bv0 4)) (= (_ bv1 1) (bvlshr (_ bv1 1) (ite (bvult v0 ((_ sign_extend 3) _let_3)) (_ bv1 1) (_ bv0 1)))) (or false (bvugt ((_ zero_extend 3) (ite (bvuge (_ bv0 4) _let_5) (_ bv1 1) (_ bv0 1))) (_ bv0 4)) (distinct (_ bv1 1) (ite (bvslt v6 (_ bv0 4)) (_ bv1 1) (_ bv0 1)))) (or false (= v1 ((_ zero_extend 3) (ite (bvsgt v3 _let_2) (_ bv1 1) (_ bv0 1)))) (bvule v6 _let_6)) (or false (bvule (ite (bvule v0 v6) (_ bv1 1) (_ bv0 1)) ((_ extract 2 2) _let_4)) (bvsle (_ bv0 4) (bvand (_ bv4 4) v3))) (or false (not (bvsge (_ bv0 4) (bvshl _let_0 _let_7))) (not (bvuge (_ bv0 4) (bvand (_ bv4 4) _let_6)))) (bvslt _let_1 (ite (bvuge v6 ((_ sign_extend 3) (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (not (bvsle _let_7 (bvxnor (_ bv0 4) (bvxnor (_ bv0 4) (bvand v1 v6))))) (distinct (_ bv0 4) (ite (= (_ bv1 1) (bvcomp v2 v3)) v8 ((_ zero_extend 3) (bvcomp v0 v5))))))))))))) ))