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