(set-option :incremental false)
(set-info :status sat)
(set-logic QF_BV)
(declare-fun v3 () (_ BitVec 4))
(declare-fun v0 () (_ BitVec 4))
(declare-fun v1 () (_ BitVec 4))
(declare-fun v2 () (_ BitVec 4))
(declare-fun v4 () (_ BitVec 4))
(check-sat-assuming ( (let ((_let_0 (bvnot v0))) (let ((_let_1 (bvlshr v1 _let_0))) (let ((_let_2 (bvneg _let_1))) (let ((_let_3 (= (_ bv0 4) _let_2))) (let ((_let_4 (bvnot v2))) (let ((_let_5 (bvxnor _let_4 ((_ zero_extend 3) (bvcomp (_ bv12 4) v0))))) (let ((_let_6 (ite (bvsge v1 (_ bv0 4)) (_ bv1 1) (_ bv0 1)))) (let ((_let_7 (bvlshr _let_1 v3))) (and (not (bvuge (_ bv12 4) v2)) (or false _let_3 (not _let_3)) (or false (distinct v2 _let_5) (not (bvsge _let_1 (ite (= (_ bv1 1) (ite (bvsgt v0 _let_4) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 3) _let_6) _let_4)))) (not (bvsle ((_ sign_extend 3) (ite (bvule (_ bv12 4) _let_2) (_ bv1 1) (_ bv0 1))) _let_5)) (bvugt _let_1 (bvxor v0 v4)) (or false (distinct _let_6 (ite (bvslt (bvneg _let_4) v4) (_ bv1 1) (_ bv0 1))) (bvslt _let_7 _let_2)) (or false (bvsle _let_0 _let_4) (bvsle (_ bv0 4) _let_7))))))))))) ))