(set-option :incremental false)
(set-info :status sat)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 6))
(declare-fun v1 () (_ BitVec 16))
(declare-fun v2 () (_ BitVec 1))
(declare-fun a3 () (Array (_ BitVec 1) (_ BitVec 16)))
(declare-fun a4 () (Array (_ BitVec 16) (_ BitVec 1)))
(check-sat-assuming ( (let ((_let_0 (ite (bvult v0 ((_ sign_extend 5) v2)) (_ bv1 1) (_ bv0 1)))) (let ((_let_1 ((_ sign_extend 0) v1))) (let ((_let_2 (select a3 ((_ extract 0 0) (_ bv6 4))))) (let ((_let_3 (select (store (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ sign_extend 15) _let_0) ((_ extract 4 4) v1)) (select a3 ((_ extract 4 4) v0))))) (let ((_let_4 (select (store (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ sign_extend 15) _let_0) ((_ extract 4 4) v1)) _let_2))) (let ((_let_5 ((_ sign_extend 15) _let_4))) (let ((_let_6 (bvadd _let_5 v1))) (let ((_let_7 (bvlshr _let_2 ((_ sign_extend 12) (_ bv6 4))))) (let ((_let_8 (bvsdiv ((_ zero_extend 15) (select (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 15) _let_0))) (select a3 ((_ extract 4 4) v0))))) (let ((_let_9 ((_ rotate_right 0) _let_0))) (let ((_let_10 (ite (bvugt _let_1 _let_5) (_ bv1 1) (_ bv0 1)))) (let ((_let_11 ((_ sign_extend 15) v2))) (let ((_let_12 (bvsdiv _let_11 _let_8))) (let ((_let_13 ((_ zero_extend 15) (bvlshr _let_3 (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1)))))) (let ((_let_14 (= v1 _let_1))) (let ((_let_15 (or (bvult _let_7 _let_6) (xor (bvsgt _let_3 _let_4) (bvugt ((_ zero_extend 15) _let_4) _let_2))))) (let ((_let_16 (= (and (bvuge v1 _let_1) (not (bvugt v0 ((_ zero_extend 2) (_ bv6 4))))) (bvule _let_12 ((_ sign_extend 15) (bvlshr _let_3 (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1)))))))) (let ((_let_17 (xor (and (= _let_7 v1) (bvslt ((_ sign_extend 10) v0) v1)) (bvsle _let_11 _let_7)))) (let ((_let_18 (=> (xor (bvult _let_10 v2) (bvsge ((_ sign_extend 15) _let_9) _let_1)) (xor (bvult _let_10 v2) (bvsge ((_ sign_extend 15) _let_9) _let_1))))) (let ((_let_19 (bvnot (_ bv0 16)))) (and (and (and (and (or (= (= (and (or _let_18 _let_18) (xor (= (or _let_15 _let_15) (or (or (bvsle ((_ sign_extend 15) (select (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 15) _let_0))) v1) (distinct _let_9 _let_9)) (=> (bvsle _let_13 (select a3 ((_ extract 4 4) v0))) (bvsgt v0 ((_ zero_extend 5) _let_3))))) (ite (xor (bvsle (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1)) v2) (ite (bvsle (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1)) (bvlshr _let_3 (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1)))) (distinct (select a3 ((_ extract 4 4) v0)) ((_ sign_extend 10) v0)) (xor (distinct _let_2 _let_12) (bvult _let_4 _let_4)))) (and (=> (or (and (= (= (select (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 15) _let_0)) _let_3) (= (bvsle _let_2 _let_6) (bvugt _let_2 _let_8))) (and (xor (bvslt _let_12 ((_ zero_extend 15) (select (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 15) _let_0)))) (bvult ((_ zero_extend 5) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) v0)) (bvult ((_ zero_extend 15) _let_10) _let_1))) (bvult _let_10 (select (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 15) _let_0)))) (and (bvugt _let_4 (select (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 15) _let_0))) (bvuge _let_4 _let_0))) (=> (bvsle _let_10 v2) (not (or _let_14 _let_14)))) (not (bvuge v0 ((_ zero_extend 5) v2)))))) (ite (bvsgt ((_ zero_extend 3) _let_9) (_ bv6 4)) (= (bvsle _let_1 _let_11) (bvult _let_0 (bvlshr _let_3 (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))))) (bvule _let_0 (bvlshr _let_3 (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1)))))) (xor (and (or (or (ite (distinct (select a3 ((_ extract 4 4) v0)) _let_8) _let_16 _let_16) (bvsgt _let_9 (select (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 15) _let_0)))) (distinct ((_ zero_extend 15) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) _let_2)) (not (bvule _let_12 ((_ zero_extend 10) (bvxnor ((_ zero_extend 5) _let_4) v0))))) (xor (not (xor (bvule (bvlshr _let_3 (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) _let_4) (bvsle (_ bv6 4) ((_ zero_extend 3) _let_0)))) (bvsle _let_7 ((_ zero_extend 15) (select (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 15) _let_0))))))) (or (or _let_17 _let_17) (xor (xor (xor (bvsle ((_ sign_extend 15) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) _let_2) (ite (bvugt _let_13 _let_8) (bvule _let_1 _let_2) (ite (bvsge (_ bv6 4) (_ bv6 4)) (bvuge _let_6 _let_12) (= ((_ zero_extend 15) _let_3) v1)))) (bvslt _let_13 _let_1)) (and (bvult ((_ sign_extend 5) (select (store a4 ((_ sign_extend 15) _let_0) (ite (bvslt (_ bv6 4) ((_ zero_extend 3) _let_0)) (_ bv1 1) (_ bv0 1))) ((_ zero_extend 15) _let_0))) v0) (= v1 ((_ zero_extend 10) v0)))))) (not (= (select a3 ((_ extract 4 4) v0)) (_ bv0 16)))) (not (= (select a3 ((_ extract 4 4) v0)) _let_19))) (not (= _let_8 (_ bv0 16)))) (not (= _let_8 _let_19))))))))))))))))))))))) ))