(set-option :incremental false)
(set-info :status sat)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 12))
(declare-fun v1 () (_ BitVec 11))
(declare-fun a2 () (Array (_ BitVec 1) (_ BitVec 14)))
(declare-fun a3 () (Array (_ BitVec 1) (_ BitVec 6)))
(check-sat-assuming ( (let ((_let_0 (select a3 ((_ extract 4 4) (bvor ((_ sign_extend 1) v1) v0))))) (let ((_let_1 ((_ extract 5 5) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0))))) (let ((_let_2 ((_ zero_extend 9) (select (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 3 3) (bvsmod ((_ sign_extend 4) (_ bv80 7)) v1)))))) (let ((_let_3 ((_ zero_extend 0) (_ bv80 7)))) (let ((_let_4 (ite (bvuge ((_ sign_extend 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0))) _let_2) (_ bv1 1) (_ bv0 1)))) (let ((_let_5 ((_ repeat 1) v1))) (let ((_let_6 (bvor ((_ zero_extend 5) _let_0) v1))) (let ((_let_7 (bvurem ((_ zero_extend 9) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 5 5) (_ bv80 7)) ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 11 11) (bvor ((_ sign_extend 1) v1) v0)))) _let_2))) (let ((_let_8 (bvsdiv ((_ sign_extend 4) (bvsmod ((_ sign_extend 4) (_ bv80 7)) v1)) _let_7))) (let ((_let_9 ((_ sign_extend 5) (select (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 3 3) (bvsmod ((_ sign_extend 4) (_ bv80 7)) v1)))))) (let ((_let_10 (bvsge ((_ sign_extend 11) (ite (bvsle ((_ sign_extend 6) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1 ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1)) (bvor ((_ sign_extend 1) v1) v0)) (_ bv1 1) (_ bv0 1))) v0))) (let ((_let_11 (bvult _let_8 ((_ sign_extend 14) (ite (bvslt v0 (bvor ((_ sign_extend 1) v1) v0)) (_ bv1 1) (_ bv0 1)))))) (let ((_let_12 (bvult ((_ sign_extend 4) _let_6) (bvxor _let_2 ((_ zero_extend 3) (bvor ((_ sign_extend 1) v1) v0)))))) (let ((_let_13 (xor (= (distinct ((_ sign_extend 8) _let_3) _let_8) (or (bvule (bvor ((_ sign_extend 1) v1) v0) ((_ sign_extend 1) (bvsmod ((_ sign_extend 4) (_ bv80 7)) v1))) (ite (bvule ((_ sign_extend 3) (bvor ((_ sign_extend 1) v1) v0)) _let_8) (bvuge ((_ zero_extend 6) (select (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 3 3) (bvsmod ((_ sign_extend 4) (_ bv80 7)) v1)))) (bvor ((_ sign_extend 1) v1) v0)) (bvuge _let_2 ((_ zero_extend 4) (bvsmod ((_ sign_extend 4) (_ bv80 7)) v1)))))) (bvsgt _let_7 ((_ zero_extend 14) (ite (bvsle ((_ sign_extend 6) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1 ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1)) (bvor ((_ sign_extend 1) v1) v0)) (_ bv1 1) (_ bv0 1))))))) (let ((_let_14 (not (=> (= (bvult (bvxor _let_2 ((_ zero_extend 3) (bvor ((_ sign_extend 1) v1) v0))) ((_ zero_extend 4) v1)) (bvsge (_ bv80 7) ((_ sign_extend 6) (ite (bvslt v0 (bvor ((_ sign_extend 1) v1) v0)) (_ bv1 1) (_ bv0 1))))) (bvult ((_ zero_extend 5) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1 ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1)) (bvsmod ((_ sign_extend 4) (_ bv80 7)) v1)))))) (let ((_let_15 (and (not (bvsge (_ bv80 7) ((_ zero_extend 1) (bvashr (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 5 5) (_ bv80 7)) ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 11 11) (bvor ((_ sign_extend 1) v1) v0))) _let_0)))) (not (bvsge (_ bv80 7) ((_ zero_extend 1) (bvashr (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 5 5) (_ bv80 7)) ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 11 11) (bvor ((_ sign_extend 1) v1) v0))) _let_0))))))) (and (and (and (and (and (or (and (= (not (= (xor (bvult ((_ sign_extend 11) (ite (bvsle ((_ sign_extend 6) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1 ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1)) (bvor ((_ sign_extend 1) v1) v0)) (_ bv1 1) (_ bv0 1))) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0))) (bvult (_ bv80 7) ((_ sign_extend 6) ((_ rotate_right 0) _let_4)))) (not (not (bvult ((_ zero_extend 14) _let_4) _let_2))))) (and (not (not (not (and _let_10 _let_10)))) (= _let_15 _let_15))) (ite (ite (xor (xor (and (xor _let_12 _let_12) (bvslt ((_ sign_extend 10) (ite (bvsle ((_ sign_extend 6) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1 ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1)) (bvor ((_ sign_extend 1) v1) v0)) (_ bv1 1) (_ bv0 1))) v1)) (ite (or (bvult ((_ sign_extend 5) (ite (bvslt v0 (bvor ((_ sign_extend 1) v1) v0)) (_ bv1 1) (_ bv0 1))) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 5 5) (_ bv80 7)) ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 11 11) (bvor ((_ sign_extend 1) v1) v0)))) (bvsle _let_5 ((_ zero_extend 5) (select (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 3 3) (bvsmod ((_ sign_extend 4) (_ bv80 7)) v1)))))) (bvsge _let_7 (bvxor _let_2 ((_ zero_extend 3) (bvor ((_ sign_extend 1) v1) v0)))) (bvugt _let_6 ((_ sign_extend 5) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1 ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1))))) (= _let_11 _let_11)) (ite (bvsgt ((_ zero_extend 6) (ite (bvslt v0 (bvor ((_ sign_extend 1) v1) v0)) (_ bv1 1) (_ bv0 1))) _let_3) (bvsgt _let_2 ((_ zero_extend 3) (bvor ((_ sign_extend 1) v1) v0))) (bvuge (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1 ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1) ((_ sign_extend 5) (ite (bvsle ((_ sign_extend 6) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1 ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) _let_1)) (bvor ((_ sign_extend 1) v1) v0)) (_ bv1 1) (_ bv0 1))))) (or (and (distinct _let_9 _let_5) (or (bvule _let_8 ((_ sign_extend 3) v0)) (and (bvsgt (_ bv80 7) ((_ sign_extend 1) _let_0)) (not (= ((_ zero_extend 8) (_ bv80 7)) _let_7))))) (or (not (bvuge _let_8 ((_ zero_extend 9) (select (store (store a3 ((_ extract 7 7) v0) ((_ extract 5 0) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 5 5) (_ bv80 7)) ((_ extract 8 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0)))) ((_ extract 11 11) (bvor ((_ sign_extend 1) v1) v0)))))) (distinct ((_ zero_extend 4) _let_5) _let_7)))) (and _let_13 _let_13) (ite (not (bvuge v1 _let_9)) (not (bvsle _let_7 ((_ zero_extend 3) ((_ rotate_right 8) (bvor ((_ sign_extend 1) v1) v0))))) (xor (bvsge _let_3 ((_ zero_extend 6) _let_4)) (bvult v0 ((_ sign_extend 1) v1)))))) (and _let_14 _let_14)) (not (= _let_7 (_ bv0 15)))) (not (= _let_7 (bvnot (_ bv0 15))))) (not (= v1 (_ bv0 11)))) (not (= v1 (bvnot (_ bv0 11))))) (not (= _let_2 (_ bv0 15)))))))))))))))))))) ))