1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/fuzz09.smtv1.smt2 b/test/regress/regress0/aufbv/fuzz09.smtv1.smt2
new file mode 100644
index 000000000..b9658e097
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz09.smtv1.smt2
@@ -0,0 +1,10 @@
+(set-option :incremental false)
+(set-info :status sat)
+(set-logic QF_AUFBV)
+(declare-fun v0 () (_ BitVec 4))
+(declare-fun v1 () (_ BitVec 6))
+(declare-fun v2 () (_ BitVec 11))
+(declare-fun v3 () (_ BitVec 1))
+(declare-fun v4 () (_ BitVec 10))
+(declare-fun a5 () (Array (_ BitVec 13) (_ BitVec 16)))
+(check-sat-assuming ( (let ((_let_0 (bvsrem ((_ zero_extend 8) (_ bv2 2)) v4))) (let ((_let_1 (bvneg v3))) (let ((_let_2 ((_ zero_extend 15) _let_1))) (let ((_let_3 ((_ zero_extend 2) (bvand ((_ sign_extend 5) v1) v2)))) (let ((_let_4 (store (store a5 ((_ zero_extend 2) v2) _let_2) _let_3 ((_ sign_extend 14) (_ bv2 2))))) (let ((_let_5 (select _let_4 ((_ zero_extend 9) v0)))) (let ((_let_6 (select (store (store a5 ((_ zero_extend 2) v2) _let_2) ((_ zero_extend 7) v1) ((_ sign_extend 14) (_ bv2 2))) ((_ sign_extend 12) _let_1)))) (let ((_let_7 ((_ sign_extend 6) v4))) (let ((_let_8 (ite (bvsge _let_0 ((_ zero_extend 8) (_ bv2 2))) (_ bv1 1) (_ bv0 1)))) (let ((_let_9 (bvnor _let_2 (select (store a5 ((_ zero_extend 2) v2) _let_2) ((_ zero_extend 12) _let_1))))) (let ((_let_10 ((_ zero_extend 15) _let_8))) (let ((_let_11 (bvand _let_9 _let_10))) (let ((_let_12 (bvsdiv ((_ sign_extend 2) v0) v1))) (let ((_let_13 (ite (bvsle ((_ zero_extend 9) (_ bv2 2)) (bvand ((_ sign_extend 5) v1) v2)) (_ bv1 1) (_ bv0 1)))) (let ((_let_14 (bvxnor _let_6 _let_6))) (let ((_let_15 (bvcomp _let_5 _let_14))) (let ((_let_16 ((_ sign_extend 15) v3))) (let ((_let_17 (ite (bvsge (select (store _let_4 _let_3 _let_6) ((_ sign_extend 12) v3)) _let_16) (_ bv1 1) (_ bv0 1)))) (let ((_let_18 (ite (bvult ((_ zero_extend 1) v4) (bvand ((_ sign_extend 5) v1) v2)) (_ bv1 1) (_ bv0 1)))) (let ((_let_19 ((_ zero_extend 5) _let_13))) (let ((_let_20 ((_ zero_extend 15) _let_13))) (let ((_let_21 ((_ zero_extend 6) v4))) (let ((_let_22 ((_ sign_extend 15) _let_15))) (let ((_let_23 ((_ sign_extend 15) _let_1))) (let ((_let_24 (ite (bvult v1 _let_19) (bvugt ((_ sign_extend 15) _let_13) _let_5) (bvsle _let_0 ((_ zero_extend 8) (_ bv2 2)))))) (let ((_let_25 (or (ite (=> (bvsle _let_0 ((_ sign_extend 4) v1)) (bvuge _let_11 _let_5)) (not (bvsge _let_6 ((_ sign_extend 15) _let_13))) (and (bvsle _let_5 ((_ sign_extend 5) (bvand ((_ sign_extend 5) v1) v2))) (bvugt (select (store a5 ((_ zero_extend 2) v2) _let_2) ((_ zero_extend 12) _let_1)) (bvsdiv ((_ zero_extend 5) (bvnand v2 ((_ sign_extend 7) v0))) _let_9)))) (bvult _let_9 ((_ zero_extend 5) (bvnand ((_ zero_extend 10) _let_8) v2)))))) (and (and (and (and (and (and (xor (not (ite (=> (bvult ((_ zero_extend 14) (_ bv2 2)) (select (store _let_4 _let_3 _let_6) ((_ sign_extend 12) v3))) (and (=> (and (bvsgt v1 ((_ zero_extend 4) (_ bv2 2))) (= (bvsdiv ((_ zero_extend 5) (bvnand v2 ((_ sign_extend 7) v0))) _let_9) _let_22)) (bvsle (_ bv2 2) ((_ sign_extend 1) _let_18))) (not (not (or (and (bvsgt (bvsdiv ((_ zero_extend 5) (bvnand v2 ((_ sign_extend 7) v0))) _let_9) ((_ zero_extend 5) (bvand ((_ sign_extend 5) v1) v2))) (bvsge ((_ zero_extend 1) _let_1) (_ bv2 2))) (bvsge _let_22 _let_9)))))) (not (or (or (not (bvugt _let_14 (select (store _let_4 _let_3 _let_6) ((_ sign_extend 12) v3)))) (ite (bvsle _let_5 ((_ zero_extend 15) v3)) (distinct ((_ sign_extend 10) _let_17) (bvnand ((_ zero_extend 10) _let_8) v2)) (bvslt v4 ((_ sign_extend 4) _let_12)))) (not (or (distinct ((_ zero_extend 15) _let_15) _let_5) (=> (xor (bvsle ((_ sign_extend 10) v3) (bvand ((_ sign_extend 5) v1) v2)) (bvuge ((_ zero_extend 6) _let_0) (bvsdiv ((_ zero_extend 5) (bvnand v2 ((_ sign_extend 7) v0))) _let_9))) (and (bvsge (_ bv2 2) ((_ sign_extend 1) _let_17)) (bvult ((_ zero_extend 1) v4) v2))))))) (or (ite _let_24 _let_24 (= (and (bvslt ((_ sign_extend 10) v1) (select (store a5 ((_ zero_extend 2) v2) _let_2) ((_ zero_extend 12) _let_1))) (bvult _let_6 ((_ sign_extend 5) (bvnand ((_ zero_extend 10) _let_8) v2)))) (bvsge _let_10 _let_9))) (and (= _let_14 _let_20) (not (distinct ((_ sign_extend 5) (bvnand v2 ((_ sign_extend 7) v0))) (select (store _let_4 _let_3 _let_6) ((_ sign_extend 12) v3)))))))) (ite (=> (or (= (bvslt ((_ sign_extend 10) _let_12) _let_9) (bvult _let_14 (select (store a5 ((_ zero_extend 2) v2) _let_2) ((_ zero_extend 12) _let_1)))) (bvuge _let_15 _let_17)) (ite (= (ite (or (= (bvsge (bvand ((_ sign_extend 5) v1) v2) ((_ zero_extend 10) v3)) (bvsge ((_ sign_extend 14) (_ bv2 2)) _let_9)) (bvslt ((_ zero_extend 10) _let_1) (bvand ((_ sign_extend 5) v1) v2))) (bvugt v4 ((_ sign_extend 9) _let_17)) (= (bvugt _let_12 _let_19) (bvuge _let_7 _let_11))) (bvuge v2 ((_ zero_extend 10) _let_8))) _let_25 _let_25)) (= (and (xor (and (= _let_23 _let_11) (bvslt ((_ sign_extend 15) _let_17) _let_9)) (= _let_0 ((_ zero_extend 8) (_ bv2 2)))) (bvslt _let_13 v3)) (= _let_20 _let_6)) (ite (and (ite (xor (bvslt _let_9 _let_10) (xor (bvugt _let_21 _let_14) (bvsle _let_5 ((_ zero_extend 15) _let_18)))) (and (= (bvsge _let_9 _let_5) (bvslt _let_5 _let_7)) (bvule _let_0 ((_ zero_extend 9) _let_1))) (not (bvsge v0 ((_ sign_extend 3) _let_8)))) (ite (or (xor (bvule v4 ((_ sign_extend 9) _let_18)) (bvugt _let_1 _let_17)) (bvslt ((_ sign_extend 14) (_ bv2 2)) (select (store _let_4 _let_3 _let_6) ((_ sign_extend 12) v3)))) (= v4 ((_ zero_extend 6) v0)) (bvslt _let_5 _let_23))) (xor (xor (bvsle ((_ zero_extend 10) v1) _let_14) (bvule ((_ zero_extend 5) _let_8) _let_12)) (xor (bvsge _let_0 _let_0) (bvsle _let_14 (select (store a5 ((_ zero_extend 2) v2) _let_2) ((_ zero_extend 12) _let_1))))) (and (distinct ((_ sign_extend 9) v3) _let_0) (and (or (and (bvsle ((_ zero_extend 5) _let_17) v1) (bvule _let_21 _let_5)) (not (distinct _let_1 _let_17))) (bvsle _let_16 _let_6)))))) (not (= _let_9 (_ bv0 16)))) (not (= _let_9 (bvnot (_ bv0 16))))) (not (= v1 (_ bv0 6)))) (not (= v1 (bvnot (_ bv0 6))))) (not (= v4 (_ bv0 10)))) (not (= v4 (bvnot (_ bv0 10))))))))))))))))))))))))))))))) ))