bug fixes to models, array rewriter with previously failing testcases

6 files changed, 369 insertions, 1 deletions

diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index 1a698b180..c67ce5b00 100644
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -44,6 +44,7 @@ TESTS =	\
 	fuzz10.smt \
 	fuzz11.smt \
 	fuzz12.smt \
+	fuzz13.smt \
 	fifo32bc06k08.delta01.smt \
 	rewrite_bug.smt \
 	array_rewrite_bug.smt
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
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index 362209579..ed810eaeb 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -15,7 +15,10 @@ endif
 TESTS =	\
         bug330.smt2 \
 	bug336.smt2 \
-	fuzz01.delta01.smt
+	fuzz01.delta01.smt \
+	fuzz02.smt \
+	fuzz03.smt \
+	fuzz04.smt
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/auflia/fuzz02.smt b/test/regress/regress0/auflia/fuzz02.smt
new file mode 100644
index 000000000..7f34226e7
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz02.smt
@@ -0,0 +1,244 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:status sat
+:extrafuns ((f0 Int Int))
+:extrafuns ((f1 Array Array))
+:extrapreds ((p0 Int Int Int))
+:extrapreds ((p1 Array Array Array))
+:extrafuns ((v0 Int))
+:extrafuns ((v1 Int))
+:extrafuns ((v2 Array))
+:extrafuns ((v3 Array))
+:formula
+(let (?e4 1)
+(let (?e5 (+ v0 v0))
+(let (?e6 (f0 v0))
+(let (?e7 (ite (p0 ?e6 v1 ?e5) 1 0))
+(let (?e8 (* v0 ?e4))
+(let (?e9 (select v3 ?e6))
+(let (?e10 (select v3 ?e5))
+(let (?e11 (f1 v3))
+(let (?e12 (f1 ?e11))
+(let (?e13 (f1 ?e12))
+(let (?e14 (f1 v2))
+(flet ($e15 (p1 v3 v3 v3))
+(flet ($e16 (p1 ?e11 ?e11 ?e13))
+(flet ($e17 (p1 ?e14 ?e13 ?e12))
+(flet ($e18 (p1 v2 v3 ?e11))
+(flet ($e19 (p0 v1 ?e9 v0))
+(flet ($e20 (p0 ?e8 v1 ?e7))
+(flet ($e21 (> v0 ?e6))
+(flet ($e22 (< ?e5 ?e10))
+(let (?e23 (ite $e20 ?e12 ?e12))
+(let (?e24 (ite $e21 ?e23 v3))
+(let (?e25 (ite $e22 ?e13 ?e12))
+(let (?e26 (ite $e18 v2 ?e24))
+(let (?e27 (ite $e15 ?e11 ?e26))
+(let (?e28 (ite $e22 ?e14 ?e26))
+(let (?e29 (ite $e16 ?e13 ?e23))
+(let (?e30 (ite $e17 ?e11 ?e28))
+(let (?e31 (ite $e19 ?e13 ?e11))
+(let (?e32 (ite $e21 v0 ?e7))
+(let (?e33 (ite $e20 ?e8 v1))
+(let (?e34 (ite $e20 ?e32 ?e32))
+(let (?e35 (ite $e16 v1 ?e8))
+(let (?e36 (ite $e17 ?e6 ?e7))
+(let (?e37 (ite $e19 ?e32 ?e7))
+(let (?e38 (ite $e21 ?e9 ?e8))
+(let (?e39 (ite $e15 ?e10 ?e37))
+(let (?e40 (ite $e19 ?e7 ?e6))
+(let (?e41 (ite $e22 ?e5 ?e8))
+(let (?e42 (ite $e18 ?e32 ?e8))
+(let (?e43 (select ?e13 ?e35))
+(let (?e44 (select ?e26 ?e37))
+(let (?e45 (f1 ?e26))
+(let (?e46 (f1 ?e12))
+(let (?e47 (f1 ?e25))
+(let (?e48 (f1 ?e25))
+(let (?e49 (f1 ?e24))
+(let (?e50 (f1 ?e14))
+(let (?e51 (f1 ?e23))
+(let (?e52 (f1 ?e27))
+(let (?e53 (f1 ?e30))
+(let (?e54 (f1 ?e29))
+(let (?e55 (f1 ?e31))
+(let (?e56 (f1 v3))
+(let (?e57 (f1 ?e50))
+(let (?e58 (f1 ?e13))
+(let (?e59 (f1 ?e11))
+(let (?e60 (f1 ?e12))
+(let (?e61 (f1 ?e28))
+(let (?e62 (f1 ?e49))
+(let (?e63 (f1 v2))
+(let (?e64 (f0 ?e36))
+(let (?e65 (+ v0 ?e36))
+(let (?e66 (- v1 ?e35))
+(let (?e67 (f0 ?e65))
+(let (?e68 (f0 ?e32))
+(let (?e69 (f0 ?e6))
+(let (?e70 (- ?e35 ?e68))
+(let (?e71 (* ?e4 ?e40))
+(let (?e72 (~ ?e42))
+(let (?e73 (- ?e38 ?e37))
+(let (?e74 (~ ?e39))
+(let (?e75 (ite (p0 ?e64 ?e34 ?e70) 1 0))
+(let (?e76 (- ?e10 ?e5))
+(let (?e77 (* ?e41 ?e4))
+(let (?e78 (ite (p0 ?e73 ?e7 ?e34) 1 0))
+(let (?e79 (~ ?e10))
+(let (?e80 (- ?e42 ?e64))
+(let (?e81 (* ?e10 (~ ?e4)))
+(let (?e82 (+ ?e9 ?e69))
+(let (?e83 (- ?e34 ?e39))
+(let (?e84 (~ ?e33))
+(let (?e85 (+ ?e43 ?e33))
+(let (?e86 (- ?e37 ?e37))
+(let (?e87 (ite (p0 ?e5 ?e64 ?e83) 1 0))
+(let (?e88 (f0 ?e74))
+(let (?e89 (ite (p0 ?e88 ?e9 ?e73) 1 0))
+(let (?e90 (+ ?e88 ?e80))
+(let (?e91 (- ?e8 ?e8))
+(let (?e92 (~ ?e44))
+(flet ($e93 (p1 ?e52 ?e59 ?e30))
+(flet ($e94 (p1 ?e61 ?e29 ?e46))
+(flet ($e95 (p1 ?e51 ?e50 ?e63))
+(flet ($e96 (p1 ?e13 ?e63 ?e23))
+(flet ($e97 (p1 ?e57 ?e25 ?e57))
+(flet ($e98 (p1 v2 ?e58 ?e31))
+(flet ($e99 (p1 ?e14 ?e28 ?e14))
+(flet ($e100 (p1 ?e62 ?e57 ?e30))
+(flet ($e101 (p1 ?e53 ?e12 ?e62))
+(flet ($e102 (p1 ?e49 ?e12 ?e52))
+(flet ($e103 (p1 ?e46 ?e49 ?e14))
+(flet ($e104 (p1 ?e57 v2 ?e31))
+(flet ($e105 (p1 ?e24 ?e55 ?e14))
+(flet ($e106 (p1 ?e53 ?e59 ?e30))
+(flet ($e107 (p1 v3 ?e11 ?e30))
+(flet ($e108 (p1 ?e56 ?e59 ?e60))
+(flet ($e109 (p1 ?e62 ?e23 ?e55))
+(flet ($e110 (p1 ?e29 ?e59 ?e51))
+(flet ($e111 (p1 ?e30 ?e28 ?e59))
+(flet ($e112 (p1 v2 ?e54 ?e13))
+(flet ($e113 (p1 ?e14 ?e50 ?e48))
+(flet ($e114 (p1 ?e26 ?e60 ?e30))
+(flet ($e115 (p1 ?e27 ?e12 ?e47))
+(flet ($e116 (p1 ?e45 ?e53 ?e62))
+(flet ($e117 (<= ?e91 ?e85))
+(flet ($e118 (>= ?e40 ?e89))
+(flet ($e119 (distinct ?e76 ?e77))
+(flet ($e120 (>= ?e91 ?e5))
+(flet ($e121 (= ?e84 ?e68))
+(flet ($e122 (p0 ?e41 v1 ?e36))
+(flet ($e123 (= ?e77 ?e69))
+(flet ($e124 (> ?e38 ?e10))
+(flet ($e125 (p0 v1 ?e77 ?e5))
+(flet ($e126 (= ?e64 ?e41))
+(flet ($e127 (>= ?e81 ?e40))
+(flet ($e128 (< ?e67 ?e39))
+(flet ($e129 (distinct ?e78 ?e65))
+(flet ($e130 (<= ?e34 ?e33))
+(flet ($e131 (<= ?e72 ?e76))
+(flet ($e132 (> ?e87 ?e88))
+(flet ($e133 (>= ?e92 ?e8))
+(flet ($e134 (>= ?e86 ?e36))
+(flet ($e135 (> ?e32 ?e33))
+(flet ($e136 (distinct ?e90 ?e6))
+(flet ($e137 (< ?e88 ?e35))
+(flet ($e138 (p0 ?e9 ?e38 ?e78))
+(flet ($e139 (> ?e80 ?e32))
+(flet ($e140 (p0 ?e79 ?e91 ?e88))
+(flet ($e141 (p0 ?e75 ?e10 ?e74))
+(flet ($e142 (>= ?e34 ?e39))
+(flet ($e143 (p0 ?e66 ?e67 ?e66))
+(flet ($e144 (= ?e90 ?e39))
+(flet ($e145 (< ?e37 ?e79))
+(flet ($e146 (distinct ?e44 ?e78))
+(flet ($e147 (< ?e83 v0))
+(flet ($e148 (>= ?e7 ?e69))
+(flet ($e149 (>= ?e73 ?e10))
+(flet ($e150 (p0 ?e71 ?e90 ?e65))
+(flet ($e151 (p0 ?e36 ?e33 ?e33))
+(flet ($e152 (> ?e82 ?e80))
+(flet ($e153 (distinct ?e79 ?e10))
+(flet ($e154 (p0 ?e42 ?e64 v0))
+(flet ($e155 (< ?e70 ?e86))
+(flet ($e156 (<= ?e43 ?e7))
+(flet ($e157 (or $e16 $e139))
+(flet ($e158 (if_then_else $e103 $e93 $e141))
+(flet ($e159 (not $e132))
+(flet ($e160 (or $e111 $e100))
+(flet ($e161 (iff $e160 $e134))
+(flet ($e162 (and $e19 $e133))
+(flet ($e163 (and $e146 $e128))
+(flet ($e164 (and $e157 $e156))
+(flet ($e165 (xor $e140 $e155))
+(flet ($e166 (implies $e113 $e153))
+(flet ($e167 (iff $e164 $e102))
+(flet ($e168 (implies $e121 $e116))
+(flet ($e169 (if_then_else $e142 $e119 $e104))
+(flet ($e170 (implies $e129 $e99))
+(flet ($e171 (or $e135 $e161))
+(flet ($e172 (or $e126 $e15))
+(flet ($e173 (implies $e158 $e137))
+(flet ($e174 (iff $e166 $e117))
+(flet ($e175 (iff $e105 $e174))
+(flet ($e176 (not $e125))
+(flet ($e177 (iff $e120 $e171))
+(flet ($e178 (xor $e168 $e149))
+(flet ($e179 (and $e96 $e96))
+(flet ($e180 (and $e130 $e143))
+(flet ($e181 (and $e108 $e20))
+(flet ($e182 (if_then_else $e173 $e159 $e167))
+(flet ($e183 (xor $e118 $e107))
+(flet ($e184 (implies $e98 $e169))
+(flet ($e185 (and $e177 $e136))
+(flet ($e186 (not $e185))
+(flet ($e187 (and $e170 $e138))
+(flet ($e188 (iff $e109 $e147))
+(flet ($e189 (or $e188 $e145))
+(flet ($e190 (implies $e152 $e94))
+(flet ($e191 (if_then_else $e97 $e181 $e163))
+(flet ($e192 (iff $e115 $e190))
+(flet ($e193 (if_then_else $e183 $e172 $e17))
+(flet ($e194 (not $e127))
+(flet ($e195 (iff $e179 $e101))
+(flet ($e196 (iff $e186 $e154))
+(flet ($e197 (if_then_else $e178 $e176 $e150))
+(flet ($e198 (xor $e122 $e124))
+(flet ($e199 (not $e182))
+(flet ($e200 (and $e112 $e197))
+(flet ($e201 (iff $e151 $e184))
+(flet ($e202 (or $e106 $e192))
+(flet ($e203 (iff $e162 $e95))
+(flet ($e204 (and $e199 $e199))
+(flet ($e205 (if_then_else $e131 $e187 $e131))
+(flet ($e206 (xor $e144 $e201))
+(flet ($e207 (and $e18 $e202))
+(flet ($e208 (and $e193 $e22))
+(flet ($e209 (or $e123 $e203))
+(flet ($e210 (not $e196))
+(flet ($e211 (and $e209 $e200))
+(flet ($e212 (xor $e208 $e114))
+(flet ($e213 (xor $e212 $e175))
+(flet ($e214 (and $e148 $e206))
+(flet ($e215 (or $e198 $e210))
+(flet ($e216 (or $e213 $e215))
+(flet ($e217 (xor $e189 $e194))
+(flet ($e218 (and $e214 $e204))
+(flet ($e219 (and $e211 $e21))
+(flet ($e220 (and $e165 $e191))
+(flet ($e221 (xor $e180 $e180))
+(flet ($e222 (and $e218 $e205))
+(flet ($e223 (iff $e195 $e219))
+(flet ($e224 (not $e221))
+(flet ($e225 (iff $e222 $e220))
+(flet ($e226 (implies $e225 $e223))
+(flet ($e227 (not $e207))
+(flet ($e228 (if_then_else $e226 $e226 $e216))
+(flet ($e229 (iff $e217 $e110))
+(flet ($e230 (not $e229))
+(flet ($e231 (if_then_else $e224 $e230 $e227))
+(flet ($e232 (or $e231 $e228))
+$e232
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/auflia/fuzz03.smt b/test/regress/regress0/auflia/fuzz03.smt
new file mode 100644
index 000000000..151250a1f
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz03.smt
@@ -0,0 +1,15 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:extrapreds ((p1 Array Array Array))
+:extrafuns ((v1 Array))
+:extrafuns ((f1 Array Array Array Array))
+:status sat
+:formula
+(let (?n1 0)
+(let (?n2 (store v1 ?n1 ?n1))
+(let (?n3 (f1 v1 v1 ?n2))
+(let (?n4 (f1 v1 ?n2 v1))
+(let (?n5 (f1 v1 ?n4 ?n2))
+(flet ($n6 (p1 ?n3 ?n5 v1))
+$n6
+)))))))
diff --git a/test/regress/regress0/auflia/fuzz04.smt b/test/regress/regress0/auflia/fuzz04.smt
new file mode 100644
index 000000000..7523aae28
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz04.smt
@@ -0,0 +1,15 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:extrapreds ((p1 Array Array))
+:extrafuns ((f1 Array Array Array Array))
+:extrafuns ((v3 Array))
+:status sat
+:formula
+(let (?n1 (f1 v3 v3 v3))
+(let (?n2 0)
+(let (?n3 (store v3 ?n2 ?n2))
+(let (?n4 (f1 v3 v3 ?n3))
+(let (?n5 (f1 v3 ?n4 v3))
+(flet ($n6 (p1 ?n1 ?n5))
+$n6
+)))))))