bug fixes to models, array rewriter with previously failing testcases

1 files changed, 90 insertions, 0 deletions

diff --git a/test/regress/regress0/aufbv/fuzz13.smt b/test/regress/regress0/aufbv/fuzz13.smt
new file mode 100644
index 000000000..d8c0b8480
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz13.smt
@@ -0,0 +1,90 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:status sat
+:extrafuns ((v0 BitVec[9]))
+:extrafuns ((v1 BitVec[14]))
+:extrafuns ((a2 Array[2:5]))
+:extrafuns ((a3 Array[8:5]))
+:formula
+(let (?e4 bv712[10])
+(let (?e5 (ite (bvslt ?e4 ?e4) bv1[1] bv0[1]))
+(let (?e6 (ite (= bv1[1] (extract[2:2] v1)) (sign_extend[5] v0) v1))
+(let (?e7 (store a2 (sign_extend[1] ?e5) (extract[12:8] ?e6)))
+(let (?e8 (store ?e7 (zero_extend[1] ?e5) (extract[6:2] v1)))
+(let (?e9 (select ?e8 (extract[12:11] v1)))
+(let (?e10 (select a2 (extract[2:1] ?e4)))
+(let (?e11 (store ?e8 (zero_extend[1] ?e5) ?e10))
+(let (?e12 (select ?e11 (extract[1:0] ?e10)))
+(let (?e13 (select a2 (extract[3:2] ?e9)))
+(let (?e14 (ite (bvsge (zero_extend[4] ?e10) v0) bv1[1] bv0[1]))
+(let (?e15 (bvnand ?e4 (zero_extend[5] ?e13)))
+(let (?e16 (ite (bvule ?e12 ?e12) bv1[1] bv0[1]))
+(let (?e17 (extract[0:0] ?e5))
+(let (?e18 (zero_extend[0] ?e6))
+(let (?e19 (bvsdiv (zero_extend[9] ?e12) v1))
+(let (?e20 (bvsdiv (zero_extend[9] ?e9) ?e6))
+(flet ($e21 (bvugt v1 (zero_extend[9] ?e12)))
+(flet ($e22 (bvuge ?e9 (sign_extend[4] ?e14)))
+(flet ($e23 (bvslt ?e6 (sign_extend[9] ?e10)))
+(flet ($e24 (bvugt ?e19 v1))
+(flet ($e25 (bvult (sign_extend[4] ?e12) v0))
+(flet ($e26 (= (sign_extend[4] ?e15) v1))
+(flet ($e27 (= ?e19 (sign_extend[9] ?e12)))
+(flet ($e28 (bvsge (zero_extend[9] ?e9) ?e6))
+(flet ($e29 (bvuge ?e13 (zero_extend[4] ?e5)))
+(flet ($e30 (distinct (zero_extend[4] ?e14) ?e9))
+(flet ($e31 (bvsle (zero_extend[4] ?e14) ?e12))
+(flet ($e32 (bvslt ?e10 ?e12))
+(flet ($e33 (distinct ?e6 ?e18))
+(flet ($e34 (bvsge (sign_extend[4] ?e12) v0))
+(flet ($e35 (bvsge ?e6 (zero_extend[5] v0)))
+(flet ($e36 (distinct v0 (sign_extend[4] ?e13)))
+(flet ($e37 (= ?e18 (sign_extend[5] v0)))
+(flet ($e38 (bvugt ?e16 ?e5))
+(flet ($e39 (bvslt ?e9 (sign_extend[4] ?e16)))
+(flet ($e40 (distinct (zero_extend[9] ?e13) ?e19))
+(flet ($e41 (bvsle ?e19 (zero_extend[13] ?e5)))
+(flet ($e42 (bvslt (zero_extend[4] ?e12) v0))
+(flet ($e43 (bvugt ?e14 ?e17))
+(flet ($e44 (bvsle (sign_extend[4] ?e14) ?e13))
+(flet ($e45 (bvugt (zero_extend[4] ?e14) ?e12))
+(flet ($e46 (bvsge ?e19 ?e6))
+(flet ($e47 (bvsle ?e10 (zero_extend[4] ?e14)))
+(flet ($e48 (bvsle ?e20 (zero_extend[4] ?e4)))
+(flet ($e49 (and $e22 $e30))
+(flet ($e50 (or $e38 $e29))
+(flet ($e51 (xor $e41 $e34))
+(flet ($e52 (iff $e21 $e48))
+(flet ($e53 (iff $e46 $e23))
+(flet ($e54 (iff $e33 $e44))
+(flet ($e55 (and $e24 $e43))
+(flet ($e56 (implies $e32 $e31))
+(flet ($e57 (or $e56 $e47))
+(flet ($e58 (xor $e50 $e40))
+(flet ($e59 (or $e57 $e45))
+(flet ($e60 (iff $e42 $e59))
+(flet ($e61 (or $e35 $e36))
+(flet ($e62 (if_then_else $e51 $e60 $e25))
+(flet ($e63 (or $e55 $e54))
+(flet ($e64 (xor $e53 $e39))
+(flet ($e65 (and $e63 $e63))
+(flet ($e66 (or $e61 $e28))
+(flet ($e67 (and $e27 $e27))
+(flet ($e68 (or $e26 $e26))
+(flet ($e69 (or $e65 $e49))
+(flet ($e70 (xor $e58 $e62))
+(flet ($e71 (implies $e68 $e37))
+(flet ($e72 (if_then_else $e52 $e52 $e70))
+(flet ($e73 (implies $e66 $e67))
+(flet ($e74 (xor $e64 $e71))
+(flet ($e75 (and $e73 $e73))
+(flet ($e76 (implies $e72 $e69))
+(flet ($e77 (xor $e76 $e75))
+(flet ($e78 (iff $e77 $e74))
+(flet ($e79 (and $e78 (not (= v1 bv0[14]))))
+(flet ($e80 (and $e79 (not (= v1 (bvnot bv0[14])))))
+(flet ($e81 (and $e80 (not (= ?e6 bv0[14]))))
+(flet ($e82 (and $e81 (not (= ?e6 (bvnot bv0[14])))))
+$e82
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+