(set-option :incremental false)
(set-info :status sat)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 6))
(declare-fun v1 () (_ BitVec 2))
(declare-fun v2 () (_ BitVec 13))
(declare-fun v3 () (_ BitVec 9))
(declare-fun a4 () (Array (_ BitVec 5) (_ BitVec 15)))
(check-sat-assuming ( (let ((_let_0 (bvand v3 v3))) (let ((_let_1 ((_ sign_extend 2) (_ bv2 3)))) (let ((_let_2 (select (store a4 ((_ extract 4 0) (bvashr ((_ zero_extend 7) v0) v2)) ((_ sign_extend 12) (_ bv2 3))) ((_ zero_extend 2) (_ bv2 3))))) (let ((_let_3 (ite (bvsge ((_ zero_extend 7) v1) _let_0) (_ bv1 1) (_ bv0 1)))) (let ((_let_4 ((_ sign_extend 4) (bvxor ((_ sign_extend 7) v1) _let_0)))) (let ((_let_5 (bvcomp (bvashr ((_ zero_extend 7) v0) v2) _let_4))) (let ((_let_6 ((_ zero_extend 2) v2))) (let ((_let_7 (ite (= (_ bv1 1) ((_ extract 4 4) _let_0)) _let_6 _let_2))) (let ((_let_8 (ite (bvuge (bvashr ((_ zero_extend 7) v0) v2) (bvashr ((_ zero_extend 7) v0) v2)) (_ bv1 1) (_ bv0 1)))) (let ((_let_9 ((_ repeat 1) _let_1))) (let ((_let_10 (bvnand v0 ((_ sign_extend 1) _let_9)))) (let ((_let_11 (ite (or (ite (bvsgt _let_0 _let_0) (bvsgt ((_ sign_extend 6) v3) _let_2) (= v1 ((_ sign_extend 1) _let_5))) (bvule (bvashr ((_ zero_extend 7) v0) v2) ((_ zero_extend 4) _let_0))) (or (ite (bvsgt _let_0 _let_0) (bvsgt ((_ sign_extend 6) v3) _let_2) (= v1 ((_ sign_extend 1) _let_5))) (bvule (bvashr ((_ zero_extend 7) v0) v2) ((_ zero_extend 4) _let_0))) (or (and (bvsge v2 ((_ sign_extend 7) _let_10)) (bvule _let_6 _let_2)) (or (bvsgt _let_7 ((_ zero_extend 14) _let_8)) (not (xor (bvslt ((_ sign_extend 12) _let_3) (bvashr ((_ zero_extend 7) v0) v2)) (bvule (bvnot v3) ((_ sign_extend 8) _let_5))))))))) (or (and _let_11 _let_11) (not (ite (xor (not (or (bvule _let_4 (bvashr ((_ zero_extend 7) v0) v2)) (= ((_ sign_extend 10) (_ bv2 3)) v2))) (ite (bvuge _let_7 ((_ sign_extend 9) _let_10)) (= _let_2 _let_6) (bvult ((_ zero_extend 3) v1) _let_9))) (bvslt ((_ sign_extend 8) _let_8) (bvor ((_ zero_extend 6) (_ bv2 3)) _let_0)) (xor (=> (distinct ((_ zero_extend 2) _let_3) (_ bv2 3)) (bvule ((_ sign_extend 5) _let_8) v0)) (distinct v3 ((_ sign_extend 4) _let_1)))))))))))))))))) ))