path: root/test/regress/regress0/aufbv/fuzz15.smtv1.smt2

(set-option :incremental false)
(set-info :status sat)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 12))
(declare-fun a1 () (Array (_ BitVec 10) (_ BitVec 2)))
(check-sat-assuming ( (let ((_let_0 (bvand (_ bv62635 16) (_ bv62635 16)))) (let ((_let_1 (bvnand v0 v0))) (let ((_let_2 (select (store a1 ((_ extract 9 0) v0) ((_ extract 5 4) _let_0)) ((_ extract 10 1) v0)))) (let ((_let_3 (select (store (store a1 ((_ extract 9 0) v0) ((_ extract 5 4) _let_0)) ((_ extract 10 1) _let_1) ((_ extract 10 9) _let_1)) ((_ extract 14 5) _let_0)))) (let ((_let_4 (select (store a1 ((_ extract 9 0) v0) ((_ extract 5 4) _let_0)) ((_ extract 9 0) _let_1)))) (let ((_let_5 (bvnot v0))) (let ((_let_6 ((_ zero_extend 10) (select (store (store a1 ((_ extract 9 0) v0) ((_ extract 5 4) _let_0)) ((_ extract 10 1) _let_1) ((_ extract 10 9) _let_1)) ((_ sign_extend 8) _let_3))))) (let ((_let_7 (bvsub (_ bv62635 16) ((_ sign_extend 14) _let_3)))) (let ((_let_8 (bvsmod ((_ sign_extend 10) _let_3) _let_6))) (let ((_let_9 (bvurem _let_7 _let_7))) (let ((_let_10 (bvadd ((_ sign_extend 14) _let_2) _let_0))) (let ((_let_11 ((_ sign_extend 3) _let_6))) (let ((_let_12 ((_ zero_extend 11) (ite (= _let_8 _let_5) (_ bv1 1) (_ bv0 1))))) (let ((_let_13 (bvurem _let_12 _let_5))) (let ((_let_14 ((_ sign_extend 8) _let_4))) (let ((_let_15 (bvxnor ((_ zero_extend 4) _let_1) _let_7))) (let ((_let_16 ((_ sign_extend 4) _let_1))) (let ((_let_17 ((_ sign_extend 4) _let_8))) (let ((_let_18 ((_ sign_extend 10) _let_2))) (let ((_let_19 ((_ sign_extend 14) (select (store (store a1 ((_ extract 9 0) v0) ((_ extract 5 4) _let_0)) ((_ extract 10 1) _let_1) ((_ extract 10 9) _let_1)) ((_ sign_extend 8) _let_3))))) (and (and (and (and (=> (ite (and (bvsge _let_15 _let_17) (or (bvsgt (_ bv62635 16) _let_7) (bvsge _let_10 _let_16))) (not (= (=> (bvule _let_18 _let_5) (distinct _let_18 _let_5)) (xor (bvsle _let_10 _let_19) (bvslt _let_1 _let_1)))) (=> (=> (and (bvsle _let_8 _let_8) (bvult (_ bv62635 16) ((_ zero_extend 4) v0))) (not (bvslt ((_ sign_extend 14) _let_3) (_ bv62635 16)))) (=> (bvugt ((_ zero_extend 14) (select (store (store a1 ((_ extract 9 0) v0) ((_ extract 5 4) _let_0)) ((_ extract 10 1) _let_1) ((_ extract 10 9) _let_1)) ((_ sign_extend 8) _let_3))) (_ bv62635 16)) (or (=> (ite (=> (distinct _let_15 _let_0) (bvsgt (_ bv62635 16) _let_16)) (distinct _let_12 _let_13) (bvult v0 _let_13)) (= (bvsgt _let_9 ((_ sign_extend 6) _let_14)) (and (bvsge _let_13 _let_12) (=> (bvule ((_ sign_extend 5) _let_14) _let_11) (distinct ((_ zero_extend 14) (ite (= _let_8 _let_5) (_ bv1 1) (_ bv0 1))) _let_11))))) (distinct ((_ zero_extend 13) _let_2) _let_11))))) (xor (= (xor (not (bvsle _let_12 v0)) (bvule _let_6 ((_ zero_extend 10) _let_4))) (ite (= _let_13 _let_5) (and (not (bvult _let_3 _let_2)) (= (ite (= (_ bv62635 16) _let_7) (bvsgt ((_ sign_extend 2) _let_14) _let_6) (ite (bvsgt (_ bv62635 16) _let_17) (or (bvuge ((_ sign_extend 4) _let_5) _let_15) (bvult _let_15 ((_ sign_extend 4) v0))) (bvugt _let_19 _let_9))) (bvsgt _let_3 (select (store (store a1 ((_ extract 9 0) v0) ((_ extract 5 4) _let_0)) ((_ extract 10 1) _let_1) ((_ extract 10 9) _let_1)) ((_ sign_extend 8) _let_3))))) (=> (bvult _let_6 v0) (=> (distinct _let_15 ((_ zero_extend 4) _let_5)) (bvslt ((_ zero_extend 10) _let_3) _let_5))))) (not (bvult ((_ sign_extend 14) _let_4) _let_7)))) (not (= _let_6 (_ bv0 12)))) (not (= _let_6 (bvnot (_ bv0 12))))) (not (= _let_7 (_ bv0 16)))) (not (= _let_5 (_ bv0 12)))))))))))))))))))))))) ))