array benchmarks

author: Morgan Deters <mdeters@gmail.com> 2011-07-11 16:38:38 +0000
committer: Morgan Deters <mdeters@gmail.com> 2011-07-11 16:38:38 +0000
commit: 2ae8fae8c1e1de22c2324e5c63c5d7fd73a4582e (patch)
tree: a2aeb46410f1b9c9e06226864e700639a6d25f45
parent: e72fdcf6333d575e9c737a6274aa627dc9c54b47 (diff)
12 files changed, 2819 insertions, 1 deletions
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 8fdeda04a..2e302f1ee 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -10,7 +10,18 @@ TESTS =	\
 	arrays3.smt2 \
 	arrays4.smt2
 
-EXTRA_DIST = $(TESTS)
+EXTRA_DIST = $(TESTS) \
+	incorrect1.smt \
+	incorrect2.smt \
+	incorrect3.smt \
+	incorrect4.smt \
+	incorrect5.smt \
+	incorrect6.smt \
+	incorrect7.smt \
+	incorrect8.smt \
+	incorrect9.smt \
+	incorrect10.smt \
+	incorrect11.smt
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
diff --git a/test/regress/regress0/arrays/incorrect1.smt b/test/regress/regress0/arrays/incorrect1.smt
new file mode 100644
index 000000000..03b743373
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect1.smt
@@ -0,0 +1,132 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Index))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Index))
+:extrafuns ((v4 Element))
+:formula
+(flet ($e5 (distinct v0 v0))
+(flet ($e6 (= v3 v2))
+(flet ($e7 (= v1 v2))
+(flet ($e8 (distinct v4 v4))
+(let (?e9 (ite $e6 v0 v0))
+(let (?e10 (ite $e8 ?e9 v0))
+(let (?e11 (ite $e8 ?e9 ?e9))
+(let (?e12 (ite $e7 v0 ?e11))
+(let (?e13 (ite $e5 ?e10 ?e11))
+(let (?e14 (ite $e5 v3 v1))
+(let (?e15 (ite $e8 v2 v2))
+(let (?e16 (ite $e6 v3 v1))
+(let (?e17 (ite $e6 ?e15 ?e15))
+(let (?e18 (ite $e8 ?e17 ?e16))
+(let (?e19 (ite $e8 ?e15 ?e15))
+(let (?e20 (ite $e6 v3 ?e19))
+(let (?e21 (ite $e6 ?e15 ?e18))
+(let (?e22 (ite $e6 v1 ?e20))
+(let (?e23 (ite $e7 v3 ?e15))
+(let (?e24 (ite $e8 v4 v4))
+(let (?e25 (ite $e5 v4 v4))
+(let (?e26 (ite $e6 ?e25 ?e25))
+(let (?e27 (ite $e7 v4 ?e25))
+(let (?e28 (select ?e12 ?e18))
+(flet ($e29 (distinct ?e12 ?e9))
+(flet ($e30 (distinct v0 ?e12))
+(flet ($e31 (distinct ?e9 v0))
+(flet ($e32 (= ?e11 ?e9))
+(flet ($e33 (= ?e11 ?e10))
+(flet ($e34 (= ?e10 v0))
+(flet ($e35 (= ?e11 ?e10))
+(flet ($e36 (= v0 ?e9))
+(flet ($e37 (distinct ?e11 ?e12))
+(flet ($e38 (distinct ?e11 ?e9))
+(flet ($e39 (distinct ?e10 ?e11))
+(flet ($e40 (distinct ?e11 ?e13))
+(flet ($e41 (= ?e14 ?e21))
+(flet ($e42 (distinct ?e19 ?e17))
+(flet ($e43 (= ?e22 ?e21))
+(flet ($e44 (distinct ?e14 ?e18))
+(flet ($e45 (distinct v1 ?e21))
+(flet ($e46 (distinct ?e15 v3))
+(flet ($e47 (= v3 ?e19))
+(flet ($e48 (= ?e21 ?e22))
+(flet ($e49 (distinct ?e16 ?e21))
+(flet ($e50 (distinct ?e18 ?e14))
+(flet ($e51 (= v2 v2))
+(flet ($e52 (= ?e15 ?e22))
+(flet ($e53 (distinct ?e18 ?e21))
+(flet ($e54 (= v1 ?e19))
+(flet ($e55 (distinct ?e19 ?e16))
+(flet ($e56 (= ?e21 v2))
+(flet ($e57 (distinct v2 ?e22))
+(flet ($e58 (distinct ?e19 ?e21))
+(flet ($e59 (= v2 ?e19))
+(flet ($e60 (distinct ?e20 v1))
+(flet ($e61 (distinct ?e19 ?e21))
+(flet ($e62 (= ?e19 ?e16))
+(flet ($e63 (distinct ?e19 ?e19))
+(flet ($e64 (distinct ?e16 v1))
+(flet ($e65 (distinct v2 ?e20))
+(flet ($e66 (distinct ?e18 ?e23))
+(flet ($e67 (distinct ?e25 v4))
+(flet ($e68 (= ?e27 ?e27))
+(flet ($e69 (distinct ?e28 ?e27))
+(flet ($e70 (distinct ?e26 ?e26))
+(flet ($e71 (= ?e28 v4))
+(flet ($e72 (= ?e27 ?e24))
+(flet ($e73 (if_then_else $e29 $e38 $e34))
+(flet ($e74 (iff $e57 $e57))
+(flet ($e75 (iff $e71 $e42))
+(flet ($e76 (xor $e61 $e58))
+(flet ($e77 (and $e39 $e30))
+(flet ($e78 (implies $e63 $e36))
+(flet ($e79 (and $e41 $e52))
+(flet ($e80 (not $e70))
+(flet ($e81 (implies $e8 $e33))
+(flet ($e82 (or $e56 $e65))
+(flet ($e83 (or $e78 $e47))
+(flet ($e84 (if_then_else $e77 $e73 $e77))
+(flet ($e85 (or $e45 $e54))
+(flet ($e86 (or $e80 $e43))
+(flet ($e87 (iff $e6 $e32))
+(flet ($e88 (xor $e44 $e40))
+(flet ($e89 (iff $e66 $e55))
+(flet ($e90 (and $e87 $e84))
+(flet ($e91 (not $e67))
+(flet ($e92 (xor $e79 $e31))
+(flet ($e93 (or $e75 $e72))
+(flet ($e94 (and $e51 $e90))
+(flet ($e95 (and $e60 $e35))
+(flet ($e96 (xor $e68 $e82))
+(flet ($e97 (and $e88 $e89))
+(flet ($e98 (and $e59 $e96))
+(flet ($e99 (and $e93 $e92))
+(flet ($e100 (if_then_else $e86 $e76 $e37))
+(flet ($e101 (if_then_else $e81 $e64 $e97))
+(flet ($e102 (or $e5 $e100))
+(flet ($e103 (if_then_else $e48 $e85 $e99))
+(flet ($e104 (if_then_else $e95 $e69 $e94))
+(flet ($e105 (iff $e50 $e98))
+(flet ($e106 (xor $e62 $e83))
+(flet ($e107 (implies $e104 $e7))
+(flet ($e108 (if_then_else $e103 $e102 $e53))
+(flet ($e109 (iff $e105 $e105))
+(flet ($e110 (implies $e74 $e46))
+(flet ($e111 (not $e106))
+(flet ($e112 (xor $e109 $e101))
+(flet ($e113 (or $e111 $e91))
+(flet ($e114 (if_then_else $e107 $e108 $e108))
+(flet ($e115 (iff $e112 $e113))
+(flet ($e116 (iff $e115 $e115))
+(flet ($e117 (and $e110 $e116))
+(flet ($e118 (and $e114 $e114))
+(flet ($e119 (not $e49))
+(flet ($e120 (or $e118 $e118))
+(flet ($e121 (not $e119))
+(flet ($e122 (and $e117 $e121))
+(flet ($e123 (not $e122))
+(flet ($e124 (and $e120 $e123))
+$e124
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect10.smt b/test/regress/regress0/arrays/incorrect10.smt
new file mode 100644
index 000000000..402fcc128
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect10.smt
@@ -0,0 +1,275 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Index))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Element))
+:formula
+(let (?e4 (store v0 v1 v3))
+(let (?e5 (store ?e4 v2 v3))
+(let (?e6 (select ?e5 v1))
+(let (?e7 (select ?e4 v1))
+(let (?e8 (select ?e4 v1))
+(let (?e9 (store ?e4 v2 ?e8))
+(let (?e10 (select ?e9 v1))
+(let (?e11 (select ?e9 v1))
+(flet ($e12 (= v0 v0))
+(flet ($e13 (distinct ?e5 v0))
+(flet ($e14 (= ?e5 ?e9))
+(flet ($e15 (= v0 v0))
+(flet ($e16 (= ?e5 ?e4))
+(flet ($e17 (= v2 v1))
+(flet ($e18 (= ?e10 ?e11))
+(flet ($e19 (= v3 ?e6))
+(flet ($e20 (= ?e6 ?e8))
+(flet ($e21 (distinct ?e6 ?e11))
+(flet ($e22 (= ?e11 ?e10))
+(flet ($e23 (= ?e7 ?e6))
+(let (?e24 (ite $e18 ?e4 ?e4))
+(let (?e25 (ite $e16 ?e5 ?e24))
+(let (?e26 (ite $e14 v0 ?e4))
+(let (?e27 (ite $e17 ?e9 ?e26))
+(let (?e28 (ite $e22 v0 v0))
+(let (?e29 (ite $e20 ?e28 ?e28))
+(let (?e30 (ite $e21 ?e27 ?e9))
+(let (?e31 (ite $e14 ?e27 ?e4))
+(let (?e32 (ite $e15 ?e27 ?e25))
+(let (?e33 (ite $e13 ?e28 ?e4))
+(let (?e34 (ite $e12 ?e33 ?e27))
+(let (?e35 (ite $e23 ?e25 ?e9))
+(let (?e36 (ite $e14 ?e9 ?e9))
+(let (?e37 (ite $e15 ?e26 ?e5))
+(let (?e38 (ite $e19 ?e26 ?e5))
+(let (?e39 (ite $e15 v1 v2))
+(let (?e40 (ite $e16 v2 ?e39))
+(let (?e41 (ite $e18 ?e40 v1))
+(let (?e42 (ite $e21 ?e39 v2))
+(let (?e43 (ite $e17 v1 ?e39))
+(let (?e44 (ite $e13 v1 v2))
+(let (?e45 (ite $e22 ?e40 ?e42))
+(let (?e46 (ite $e23 ?e41 v2))
+(let (?e47 (ite $e12 ?e41 ?e39))
+(let (?e48 (ite $e19 ?e47 ?e39))
+(let (?e49 (ite $e18 v1 v2))
+(let (?e50 (ite $e14 ?e43 ?e49))
+(let (?e51 (ite $e20 ?e49 ?e46))
+(let (?e52 (ite $e16 v3 v3))
+(let (?e53 (ite $e17 ?e10 v3))
+(let (?e54 (ite $e12 ?e6 ?e8))
+(let (?e55 (ite $e12 ?e11 ?e10))
+(let (?e56 (ite $e13 v3 ?e10))
+(let (?e57 (ite $e15 ?e7 ?e54))
+(let (?e58 (ite $e19 ?e10 ?e55))
+(let (?e59 (ite $e18 ?e52 ?e7))
+(let (?e60 (ite $e23 ?e56 ?e8))
+(let (?e61 (ite $e14 ?e57 ?e59))
+(let (?e62 (ite $e12 ?e55 v3))
+(let (?e63 (ite $e22 ?e52 ?e11))
+(let (?e64 (ite $e13 ?e61 v3))
+(let (?e65 (ite $e20 ?e6 ?e63))
+(let (?e66 (ite $e21 ?e11 ?e63))
+(let (?e67 (store ?e28 ?e41 ?e66))
+(let (?e68 (store v0 ?e42 ?e8))
+(let (?e69 (select ?e27 ?e43))
+(let (?e70 (select ?e35 ?e40))
+(let (?e71 (select ?e28 ?e44))
+(let (?e72 (store ?e25 ?e39 ?e65))
+(let (?e73 (select ?e67 ?e45))
+(let (?e74 (store ?e25 v1 ?e66))
+(let (?e75 (select ?e34 ?e48))
+(flet ($e76 (= ?e37 ?e33))
+(flet ($e77 (distinct ?e34 ?e34))
+(flet ($e78 (= ?e32 ?e30))
+(flet ($e79 (distinct ?e31 ?e74))
+(flet ($e80 (= ?e33 ?e26))
+(flet ($e81 (= ?e31 ?e36))
+(flet ($e82 (distinct ?e34 ?e9))
+(flet ($e83 (distinct ?e9 ?e67))
+(flet ($e84 (= ?e28 ?e27))
+(flet ($e85 (distinct ?e33 ?e33))
+(flet ($e86 (= v0 ?e68))
+(flet ($e87 (distinct ?e29 ?e27))
+(flet ($e88 (distinct ?e72 ?e4))
+(flet ($e89 (distinct ?e37 ?e5))
+(flet ($e90 (= ?e67 ?e38))
+(flet ($e91 (distinct ?e27 ?e67))
+(flet ($e92 (distinct ?e30 ?e25))
+(flet ($e93 (distinct ?e33 ?e38))
+(flet ($e94 (= ?e30 ?e25))
+(flet ($e95 (distinct ?e5 ?e37))
+(flet ($e96 (distinct ?e37 ?e35))
+(flet ($e97 (distinct ?e38 ?e29))
+(flet ($e98 (distinct ?e4 ?e4))
+(flet ($e99 (distinct ?e25 ?e26))
+(flet ($e100 (= ?e32 ?e24))
+(flet ($e101 (= ?e40 ?e46))
+(flet ($e102 (distinct ?e51 ?e47))
+(flet ($e103 (= ?e51 ?e47))
+(flet ($e104 (= ?e46 ?e51))
+(flet ($e105 (= ?e41 ?e41))
+(flet ($e106 (distinct ?e43 ?e41))
+(flet ($e107 (distinct ?e49 ?e42))
+(flet ($e108 (distinct ?e44 ?e46))
+(flet ($e109 (distinct ?e45 ?e49))
+(flet ($e110 (= ?e50 ?e43))
+(flet ($e111 (= ?e51 ?e39))
+(flet ($e112 (= ?e45 ?e47))
+(flet ($e113 (= ?e41 v2))
+(flet ($e114 (= ?e51 ?e50))
+(flet ($e115 (distinct ?e45 ?e46))
+(flet ($e116 (distinct v2 ?e47))
+(flet ($e117 (= ?e45 ?e44))
+(flet ($e118 (distinct ?e41 ?e51))
+(flet ($e119 (= ?e46 ?e49))
+(flet ($e120 (distinct ?e50 ?e41))
+(flet ($e121 (= ?e50 ?e49))
+(flet ($e122 (distinct ?e50 ?e50))
+(flet ($e123 (distinct ?e41 ?e48))
+(flet ($e124 (distinct ?e46 ?e46))
+(flet ($e125 (= ?e39 v1))
+(flet ($e126 (distinct ?e6 ?e71))
+(flet ($e127 (= ?e58 ?e61))
+(flet ($e128 (= ?e7 ?e58))
+(flet ($e129 (distinct ?e66 ?e71))
+(flet ($e130 (= ?e7 ?e63))
+(flet ($e131 (= ?e53 ?e59))
+(flet ($e132 (distinct ?e63 ?e55))
+(flet ($e133 (= ?e66 ?e7))
+(flet ($e134 (distinct ?e60 ?e53))
+(flet ($e135 (distinct ?e52 ?e65))
+(flet ($e136 (distinct ?e11 ?e11))
+(flet ($e137 (= ?e54 ?e57))
+(flet ($e138 (= ?e73 v3))
+(flet ($e139 (= ?e70 ?e66))
+(flet ($e140 (distinct ?e59 ?e61))
+(flet ($e141 (distinct ?e7 ?e54))
+(flet ($e142 (= ?e70 ?e73))
+(flet ($e143 (distinct v3 ?e10))
+(flet ($e144 (= ?e7 ?e58))
+(flet ($e145 (= ?e57 ?e69))
+(flet ($e146 (distinct ?e52 ?e58))
+(flet ($e147 (distinct ?e55 ?e62))
+(flet ($e148 (= ?e10 ?e66))
+(flet ($e149 (distinct ?e70 ?e75))
+(flet ($e150 (= v3 ?e60))
+(flet ($e151 (= ?e7 ?e52))
+(flet ($e152 (distinct ?e73 ?e64))
+(flet ($e153 (= ?e56 ?e57))
+(flet ($e154 (distinct ?e52 ?e75))
+(flet ($e155 (distinct ?e66 ?e69))
+(flet ($e156 (= ?e56 ?e63))
+(flet ($e157 (= ?e11 ?e10))
+(flet ($e158 (= ?e69 ?e65))
+(flet ($e159 (distinct ?e52 ?e7))
+(flet ($e160 (= ?e53 ?e8))
+(flet ($e161 (implies $e83 $e151))
+(flet ($e162 (and $e156 $e109))
+(flet ($e163 (not $e133))
+(flet ($e164 (implies $e100 $e143))
+(flet ($e165 (iff $e114 $e162))
+(flet ($e166 (or $e76 $e152))
+(flet ($e167 (and $e12 $e93))
+(flet ($e168 (xor $e164 $e78))
+(flet ($e169 (and $e15 $e106))
+(flet ($e170 (not $e111))
+(flet ($e171 (xor $e18 $e135))
+(flet ($e172 (not $e14))
+(flet ($e173 (iff $e125 $e20))
+(flet ($e174 (iff $e84 $e142))
+(flet ($e175 (if_then_else $e129 $e150 $e153))
+(flet ($e176 (iff $e80 $e118))
+(flet ($e177 (xor $e99 $e103))
+(flet ($e178 (or $e97 $e91))
+(flet ($e179 (if_then_else $e127 $e77 $e172))
+(flet ($e180 (and $e169 $e101))
+(flet ($e181 (or $e147 $e90))
+(flet ($e182 (implies $e181 $e157))
+(flet ($e183 (or $e94 $e119))
+(flet ($e184 (and $e120 $e174))
+(flet ($e185 (iff $e23 $e177))
+(flet ($e186 (or $e86 $e85))
+(flet ($e187 (implies $e132 $e16))
+(flet ($e188 (if_then_else $e187 $e186 $e21))
+(flet ($e189 (or $e92 $e92))
+(flet ($e190 (xor $e113 $e128))
+(flet ($e191 (iff $e179 $e171))
+(flet ($e192 (not $e104))
+(flet ($e193 (and $e137 $e107))
+(flet ($e194 (or $e170 $e176))
+(flet ($e195 (or $e134 $e188))
+(flet ($e196 (and $e112 $e116))
+(flet ($e197 (if_then_else $e122 $e163 $e17))
+(flet ($e198 (if_then_else $e102 $e87 $e13))
+(flet ($e199 (or $e184 $e197))
+(flet ($e200 (implies $e189 $e196))
+(flet ($e201 (and $e191 $e79))
+(flet ($e202 (iff $e145 $e124))
+(flet ($e203 (if_then_else $e139 $e199 $e182))
+(flet ($e204 (iff $e146 $e141))
+(flet ($e205 (iff $e98 $e175))
+(flet ($e206 (or $e190 $e148))
+(flet ($e207 (and $e159 $e185))
+(flet ($e208 (xor $e144 $e165))
+(flet ($e209 (if_then_else $e202 $e167 $e19))
+(flet ($e210 (or $e208 $e180))
+(flet ($e211 (or $e89 $e203))
+(flet ($e212 (not $e198))
+(flet ($e213 (iff $e210 $e211))
+(flet ($e214 (implies $e205 $e81))
+(flet ($e215 (not $e192))
+(flet ($e216 (or $e110 $e213))
+(flet ($e217 (implies $e96 $e154))
+(flet ($e218 (not $e155))
+(flet ($e219 (xor $e136 $e105))
+(flet ($e220 (iff $e217 $e130))
+(flet ($e221 (or $e138 $e126))
+(flet ($e222 (not $e178))
+(flet ($e223 (if_then_else $e215 $e82 $e140))
+(flet ($e224 (not $e221))
+(flet ($e225 (implies $e204 $e220))
+(flet ($e226 (xor $e168 $e209))
+(flet ($e227 (or $e95 $e214))
+(flet ($e228 (implies $e218 $e218))
+(flet ($e229 (not $e225))
+(flet ($e230 (not $e229))
+(flet ($e231 (implies $e222 $e228))
+(flet ($e232 (and $e226 $e121))
+(flet ($e233 (iff $e206 $e108))
+(flet ($e234 (and $e230 $e166))
+(flet ($e235 (implies $e231 $e232))
+(flet ($e236 (not $e88))
+(flet ($e237 (not $e201))
+(flet ($e238 (if_then_else $e237 $e236 $e173))
+(flet ($e239 (and $e235 $e193))
+(flet ($e240 (xor $e239 $e238))
+(flet ($e241 (implies $e123 $e219))
+(flet ($e242 (if_then_else $e234 $e212 $e149))
+(flet ($e243 (or $e115 $e242))
+(flet ($e244 (and $e200 $e183))
+(flet ($e245 (implies $e207 $e233))
+(flet ($e246 (iff $e22 $e241))
+(flet ($e247 (implies $e194 $e240))
+(flet ($e248 (implies $e223 $e131))
+(flet ($e249 (or $e227 $e158))
+(flet ($e250 (and $e160 $e224))
+(flet ($e251 (or $e250 $e243))
+(flet ($e252 (or $e117 $e117))
+(flet ($e253 (and $e195 $e248))
+(flet ($e254 (xor $e253 $e249))
+(flet ($e255 (implies $e246 $e254))
+(flet ($e256 (iff $e251 $e161))
+(flet ($e257 (xor $e216 $e245))
+(flet ($e258 (xor $e255 $e256))
+(flet ($e259 (iff $e244 $e257))
+(flet ($e260 (if_then_else $e247 $e259 $e247))
+(flet ($e261 (xor $e258 $e252))
+(flet ($e262 (not $e260))
+(flet ($e263 (or $e262 $e262))
+(flet ($e264 (iff $e263 $e263))
+(flet ($e265 (and $e261 $e261))
+(flet ($e266 (implies $e264 $e264))
+(flet ($e267 (and $e265 $e266))
+$e267
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect11.smt b/test/regress/regress0/arrays/incorrect11.smt
new file mode 100644
index 000000000..0815e98e4
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect11.smt
@@ -0,0 +1,96 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Index))
+:extrafuns ((v2 Element))
+:extrafuns ((v3 Element))
+:extrafuns ((v4 Element))
+:formula
+(flet ($e5 (distinct v0 v0))
+(flet ($e6 (distinct v1 v1))
+(flet ($e7 (= v2 v3))
+(flet ($e8 (distinct v2 v4))
+(let (?e9 (ite $e7 v0 v0))
+(let (?e10 (ite $e5 v0 v0))
+(let (?e11 (ite $e8 v0 ?e9))
+(let (?e12 (ite $e8 ?e9 ?e9))
+(let (?e13 (ite $e6 ?e10 v0))
+(let (?e14 (ite $e8 v1 v1))
+(let (?e15 (ite $e5 ?e14 v1))
+(let (?e16 (ite $e7 v1 ?e15))
+(let (?e17 (ite $e6 ?e14 ?e15))
+(let (?e18 (ite $e7 v4 v2))
+(let (?e19 (ite $e5 v3 v3))
+(let (?e20 (ite $e8 ?e18 ?e18))
+(let (?e21 (ite $e6 v3 v3))
+(let (?e22 (select ?e13 v1))
+(flet ($e23 (distinct ?e9 ?e9))
+(flet ($e24 (= v0 ?e10))
+(flet ($e25 (distinct ?e9 ?e12))
+(flet ($e26 (= ?e11 v0))
+(flet ($e27 (distinct ?e13 ?e11))
+(flet ($e28 (distinct ?e14 v1))
+(flet ($e29 (= ?e15 ?e16))
+(flet ($e30 (= ?e16 v1))
+(flet ($e31 (distinct v1 ?e15))
+(flet ($e32 (= ?e17 v1))
+(flet ($e33 (= ?e21 ?e18))
+(flet ($e34 (distinct v3 v3))
+(flet ($e35 (= ?e21 ?e20))
+(flet ($e36 (distinct ?e18 v4))
+(flet ($e37 (distinct v2 v4))
+(flet ($e38 (= ?e20 ?e21))
+(flet ($e39 (= v3 v2))
+(flet ($e40 (distinct v3 ?e19))
+(flet ($e41 (distinct v4 ?e18))
+(flet ($e42 (= v3 v3))
+(flet ($e43 (= ?e21 ?e21))
+(flet ($e44 (distinct v2 ?e18))
+(flet ($e45 (distinct v2 v2))
+(flet ($e46 (distinct v3 v3))
+(flet ($e47 (= ?e19 v3))
+(flet ($e48 (= v4 v4))
+(flet ($e49 (= ?e19 v2))
+(flet ($e50 (= ?e20 ?e18))
+(flet ($e51 (distinct ?e22 ?e22))
+(flet ($e52 (or $e42 $e31))
+(flet ($e53 (xor $e39 $e35))
+(flet ($e54 (and $e51 $e30))
+(flet ($e55 (or $e43 $e54))
+(flet ($e56 (xor $e26 $e33))
+(flet ($e57 (not $e41))
+(flet ($e58 (implies $e32 $e50))
+(flet ($e59 (not $e24))
+(flet ($e60 (if_then_else $e53 $e7 $e27))
+(flet ($e61 (and $e48 $e38))
+(flet ($e62 (and $e61 $e52))
+(flet ($e63 (xor $e25 $e58))
+(flet ($e64 (and $e49 $e8))
+(flet ($e65 (xor $e62 $e34))
+(flet ($e66 (iff $e29 $e37))
+(flet ($e67 (if_then_else $e65 $e65 $e65))
+(flet ($e68 (xor $e46 $e55))
+(flet ($e69 (xor $e66 $e56))
+(flet ($e70 (or $e40 $e69))
+(flet ($e71 (xor $e36 $e6))
+(flet ($e72 (iff $e59 $e68))
+(flet ($e73 (and $e64 $e64))
+(flet ($e74 (iff $e57 $e63))
+(flet ($e75 (xor $e67 $e5))
+(flet ($e76 (or $e60 $e60))
+(flet ($e77 (and $e47 $e71))
+(flet ($e78 (xor $e23 $e76))
+(flet ($e79 (xor $e74 $e74))
+(flet ($e80 (and $e28 $e45))
+(flet ($e81 (if_then_else $e75 $e70 $e79))
+(flet ($e82 (if_then_else $e78 $e44 $e77))
+(flet ($e83 (or $e73 $e73))
+(flet ($e84 (iff $e72 $e80))
+(flet ($e85 (not $e82))
+(flet ($e86 (if_then_else $e81 $e81 $e85))
+(flet ($e87 (iff $e86 $e84))
+(flet ($e88 (and $e87 $e83))
+$e88
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect2.smt b/test/regress/regress0/arrays/incorrect2.smt
new file mode 100644
index 000000000..2172bbc68
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect2.smt
@@ -0,0 +1,350 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Index))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Index))
+:extrafuns ((v4 Index))
+:extrafuns ((v5 Element))
+:formula
+(flet ($e6 (= v0 v0))
+(flet ($e7 (= v4 v2))
+(flet ($e8 (distinct v3 v2))
+(flet ($e9 (= v3 v3))
+(flet ($e10 (= v2 v3))
+(flet ($e11 (distinct v2 v2))
+(flet ($e12 (distinct v4 v3))
+(flet ($e13 (distinct v4 v2))
+(flet ($e14 (distinct v4 v4))
+(flet ($e15 (distinct v3 v2))
+(flet ($e16 (= v2 v3))
+(flet ($e17 (distinct v1 v2))
+(flet ($e18 (= v5 v5))
+(let (?e19 (ite $e15 v0 v0))
+(let (?e20 (ite $e7 v0 ?e19))
+(let (?e21 (ite $e16 ?e19 ?e19))
+(let (?e22 (ite $e14 ?e19 ?e21))
+(let (?e23 (ite $e9 ?e20 ?e21))
+(let (?e24 (ite $e17 ?e23 ?e23))
+(let (?e25 (ite $e6 ?e19 ?e19))
+(let (?e26 (ite $e9 ?e22 ?e22))
+(let (?e27 (ite $e13 ?e21 ?e19))
+(let (?e28 (ite $e8 ?e21 ?e23))
+(let (?e29 (ite $e18 ?e23 ?e21))
+(let (?e30 (ite $e15 ?e26 ?e19))
+(let (?e31 (ite $e12 ?e19 ?e19))
+(let (?e32 (ite $e14 ?e21 v0))
+(let (?e33 (ite $e10 ?e21 ?e23))
+(let (?e34 (ite $e11 ?e29 ?e27))
+(let (?e35 (ite $e11 v3 v4))
+(let (?e36 (ite $e10 ?e35 v4))
+(let (?e37 (ite $e14 v1 v2))
+(let (?e38 (ite $e17 v3 ?e37))
+(let (?e39 (ite $e16 ?e35 v4))
+(let (?e40 (ite $e10 ?e36 v1))
+(let (?e41 (ite $e18 ?e38 v2))
+(let (?e42 (ite $e16 ?e38 ?e37))
+(let (?e43 (ite $e15 ?e41 v4))
+(let (?e44 (ite $e9 ?e36 ?e35))
+(let (?e45 (ite $e13 ?e36 v1))
+(let (?e46 (ite $e7 ?e36 v2))
+(let (?e47 (ite $e6 ?e43 ?e41))
+(let (?e48 (ite $e8 ?e47 ?e38))
+(let (?e49 (ite $e12 ?e46 v3))
+(let (?e50 (ite $e11 v5 v5))
+(let (?e51 (ite $e16 v5 v5))
+(let (?e52 (ite $e14 ?e51 ?e50))
+(let (?e53 (ite $e12 ?e50 ?e51))
+(let (?e54 (ite $e17 ?e52 v5))
+(let (?e55 (ite $e6 ?e51 ?e53))
+(let (?e56 (ite $e7 v5 ?e51))
+(let (?e57 (ite $e15 ?e51 ?e56))
+(let (?e58 (ite $e13 ?e51 v5))
+(let (?e59 (ite $e17 ?e55 ?e50))
+(let (?e60 (ite $e6 v5 ?e56))
+(let (?e61 (ite $e8 ?e56 ?e58))
+(let (?e62 (ite $e15 ?e59 ?e52))
+(let (?e63 (ite $e14 ?e50 ?e52))
+(let (?e64 (ite $e6 ?e55 ?e54))
+(let (?e65 (ite $e16 ?e54 ?e60))
+(let (?e66 (ite $e9 ?e65 ?e58))
+(let (?e67 (ite $e12 ?e57 ?e62))
+(let (?e68 (ite $e18 ?e51 ?e58))
+(let (?e69 (ite $e10 ?e54 ?e58))
+(let (?e70 (select ?e29 ?e40))
+(flet ($e71 (= ?e23 ?e28))
+(flet ($e72 (= ?e23 ?e26))
+(flet ($e73 (distinct ?e21 ?e19))
+(flet ($e74 (distinct ?e19 ?e32))
+(flet ($e75 (distinct ?e24 ?e26))
+(flet ($e76 (distinct ?e26 ?e30))
+(flet ($e77 (distinct v0 ?e26))
+(flet ($e78 (distinct ?e33 ?e22))
+(flet ($e79 (= ?e34 ?e28))
+(flet ($e80 (= ?e19 ?e32))
+(flet ($e81 (distinct ?e24 ?e30))
+(flet ($e82 (distinct ?e34 ?e23))
+(flet ($e83 (= ?e21 ?e27))
+(flet ($e84 (= v0 ?e21))
+(flet ($e85 (distinct ?e27 ?e21))
+(flet ($e86 (= ?e21 ?e30))
+(flet ($e87 (= ?e26 ?e34))
+(flet ($e88 (= ?e27 ?e33))
+(flet ($e89 (distinct ?e24 ?e26))
+(flet ($e90 (= ?e24 ?e19))
+(flet ($e91 (= ?e33 ?e21))
+(flet ($e92 (= ?e24 ?e33))
+(flet ($e93 (= ?e34 ?e33))
+(flet ($e94 (= ?e33 v0))
+(flet ($e95 (= ?e29 ?e26))
+(flet ($e96 (= ?e25 ?e31))
+(flet ($e97 (distinct ?e19 ?e31))
+(flet ($e98 (= ?e19 ?e29))
+(flet ($e99 (distinct ?e31 ?e31))
+(flet ($e100 (= ?e27 ?e27))
+(flet ($e101 (distinct ?e27 v0))
+(flet ($e102 (distinct ?e23 ?e29))
+(flet ($e103 (distinct ?e27 ?e29))
+(flet ($e104 (= ?e31 ?e29))
+(flet ($e105 (= ?e25 ?e26))
+(flet ($e106 (= ?e26 ?e31))
+(flet ($e107 (= ?e28 ?e33))
+(flet ($e108 (distinct v0 ?e27))
+(flet ($e109 (distinct ?e30 ?e23))
+(flet ($e110 (distinct ?e34 ?e30))
+(flet ($e111 (= ?e30 ?e31))
+(flet ($e112 (= ?e27 ?e32))
+(flet ($e113 (= ?e24 ?e27))
+(flet ($e114 (distinct ?e31 ?e26))
+(flet ($e115 (distinct ?e23 ?e30))
+(flet ($e116 (distinct v0 ?e34))
+(flet ($e117 (= ?e30 ?e21))
+(flet ($e118 (= v0 ?e34))
+(flet ($e119 (= ?e27 ?e26))
+(flet ($e120 (= ?e26 v0))
+(flet ($e121 (distinct ?e26 ?e34))
+(flet ($e122 (= ?e31 ?e33))
+(flet ($e123 (distinct ?e28 ?e21))
+(flet ($e124 (= ?e22 ?e34))
+(flet ($e125 (distinct ?e21 v0))
+(flet ($e126 (distinct ?e34 ?e29))
+(flet ($e127 (= ?e28 ?e30))
+(flet ($e128 (= ?e20 ?e26))
+(flet ($e129 (distinct ?e36 ?e36))
+(flet ($e130 (= v2 ?e41))
+(flet ($e131 (distinct ?e39 ?e38))
+(flet ($e132 (distinct v1 v3))
+(flet ($e133 (= ?e48 ?e38))
+(flet ($e134 (= ?e43 ?e44))
+(flet ($e135 (= ?e41 v4))
+(flet ($e136 (= ?e45 ?e47))
+(flet ($e137 (distinct ?e36 ?e48))
+(flet ($e138 (= ?e47 ?e46))
+(flet ($e139 (= v2 ?e40))
+(flet ($e140 (= ?e45 ?e44))
+(flet ($e141 (= ?e35 v1))
+(flet ($e142 (= v4 v4))
+(flet ($e143 (= ?e42 ?e35))
+(flet ($e144 (= v1 ?e41))
+(flet ($e145 (= ?e47 ?e40))
+(flet ($e146 (= ?e47 v1))
+(flet ($e147 (distinct ?e41 ?e44))
+(flet ($e148 (= ?e35 ?e35))
+(flet ($e149 (distinct ?e35 v1))
+(flet ($e150 (= ?e40 ?e44))
+(flet ($e151 (= ?e45 v2))
+(flet ($e152 (= v2 ?e35))
+(flet ($e153 (distinct ?e38 v3))
+(flet ($e154 (distinct ?e45 ?e38))
+(flet ($e155 (distinct v4 ?e48))
+(flet ($e156 (= ?e49 ?e46))
+(flet ($e157 (distinct ?e40 ?e44))
+(flet ($e158 (= ?e42 ?e46))
+(flet ($e159 (= ?e39 ?e39))
+(flet ($e160 (distinct ?e44 ?e41))
+(flet ($e161 (= ?e48 v2))
+(flet ($e162 (distinct ?e49 ?e46))
+(flet ($e163 (= ?e39 ?e44))
+(flet ($e164 (distinct ?e41 ?e40))
+(flet ($e165 (distinct ?e46 ?e46))
+(flet ($e166 (distinct v3 ?e37))
+(flet ($e167 (= ?e51 ?e53))
+(flet ($e168 (= ?e59 ?e53))
+(flet ($e169 (= ?e67 ?e59))
+(flet ($e170 (distinct ?e55 ?e64))
+(flet ($e171 (distinct ?e58 ?e52))
+(flet ($e172 (= ?e52 ?e52))
+(flet ($e173 (distinct ?e69 ?e61))
+(flet ($e174 (distinct ?e67 ?e56))
+(flet ($e175 (= ?e62 ?e62))
+(flet ($e176 (distinct ?e50 ?e52))
+(flet ($e177 (= ?e52 ?e60))
+(flet ($e178 (distinct ?e68 ?e58))
+(flet ($e179 (= ?e62 ?e50))
+(flet ($e180 (distinct v5 ?e62))
+(flet ($e181 (distinct ?e53 ?e57))
+(flet ($e182 (= ?e63 ?e50))
+(flet ($e183 (= ?e62 ?e56))
+(flet ($e184 (= ?e54 ?e61))
+(flet ($e185 (distinct ?e69 ?e59))
+(flet ($e186 (= ?e65 ?e52))
+(flet ($e187 (distinct ?e64 ?e63))
+(flet ($e188 (= ?e63 ?e66))
+(flet ($e189 (distinct ?e64 ?e67))
+(flet ($e190 (= v5 v5))
+(flet ($e191 (distinct ?e52 ?e60))
+(flet ($e192 (distinct ?e51 ?e70))
+(flet ($e193 (xor $e181 $e149))
+(flet ($e194 (xor $e188 $e96))
+(flet ($e195 (implies $e179 $e73))
+(flet ($e196 (iff $e83 $e91))
+(flet ($e197 (or $e105 $e123))
+(flet ($e198 (and $e121 $e172))
+(flet ($e199 (not $e147))
+(flet ($e200 (iff $e189 $e117))
+(flet ($e201 (or $e155 $e108))
+(flet ($e202 (iff $e144 $e175))
+(flet ($e203 (or $e107 $e201))
+(flet ($e204 (and $e8 $e168))
+(flet ($e205 (iff $e90 $e171))
+(flet ($e206 (or $e157 $e10))
+(flet ($e207 (xor $e92 $e82))
+(flet ($e208 (xor $e180 $e148))
+(flet ($e209 (iff $e191 $e124))
+(flet ($e210 (xor $e110 $e152))
+(flet ($e211 (implies $e102 $e18))
+(flet ($e212 (not $e139))
+(flet ($e213 (implies $e205 $e203))
+(flet ($e214 (not $e209))
+(flet ($e215 (xor $e94 $e192))
+(flet ($e216 (or $e122 $e6))
+(flet ($e217 (and $e145 $e113))
+(flet ($e218 (implies $e161 $e88))
+(flet ($e219 (xor $e202 $e199))
+(flet ($e220 (xor $e135 $e213))
+(flet ($e221 (not $e100))
+(flet ($e222 (not $e87))
+(flet ($e223 (and $e127 $e208))
+(flet ($e224 (implies $e166 $e212))
+(flet ($e225 (not $e115))
+(flet ($e226 (not $e15))
+(flet ($e227 (or $e170 $e120))
+(flet ($e228 (not $e101))
+(flet ($e229 (implies $e156 $e162))
+(flet ($e230 (iff $e125 $e75))
+(flet ($e231 (xor $e223 $e81))
+(flet ($e232 (implies $e174 $e160))
+(flet ($e233 (implies $e97 $e200))
+(flet ($e234 (if_then_else $e103 $e134 $e176))
+(flet ($e235 (and $e133 $e89))
+(flet ($e236 (not $e17))
+(flet ($e237 (implies $e225 $e98))
+(flet ($e238 (or $e130 $e104))
+(flet ($e239 (not $e169))
+(flet ($e240 (implies $e118 $e16))
+(flet ($e241 (iff $e237 $e190))
+(flet ($e242 (not $e227))
+(flet ($e243 (and $e154 $e217))
+(flet ($e244 (if_then_else $e137 $e76 $e236))
+(flet ($e245 (not $e153))
+(flet ($e246 (and $e138 $e93))
+(flet ($e247 (not $e197))
+(flet ($e248 (xor $e141 $e210))
+(flet ($e249 (iff $e140 $e246))
+(flet ($e250 (or $e187 $e72))
+(flet ($e251 (implies $e228 $e14))
+(flet ($e252 (if_then_else $e193 $e11 $e85))
+(flet ($e253 (iff $e158 $e80))
+(flet ($e254 (or $e167 $e86))
+(flet ($e255 (not $e243))
+(flet ($e256 (or $e79 $e7))
+(flet ($e257 (implies $e109 $e9))
+(flet ($e258 (xor $e177 $e126))
+(flet ($e259 (xor $e254 $e13))
+(flet ($e260 (or $e226 $e250))
+(flet ($e261 (not $e95))
+(flet ($e262 (iff $e99 $e234))
+(flet ($e263 (implies $e260 $e242))
+(flet ($e264 (implies $e173 $e233))
+(flet ($e265 (if_then_else $e218 $e214 $e12))
+(flet ($e266 (and $e221 $e248))
+(flet ($e267 (or $e106 $e206))
+(flet ($e268 (iff $e263 $e245))
+(flet ($e269 (if_then_else $e262 $e216 $e266))
+(flet ($e270 (and $e257 $e247))
+(flet ($e271 (if_then_else $e198 $e270 $e132))
+(flet ($e272 (xor $e230 $e204))
+(flet ($e273 (not $e235))
+(flet ($e274 (and $e143 $e220))
+(flet ($e275 (and $e128 $e142))
+(flet ($e276 (and $e114 $e74))
+(flet ($e277 (if_then_else $e252 $e195 $e146))
+(flet ($e278 (xor $e277 $e275))
+(flet ($e279 (implies $e232 $e259))
+(flet ($e280 (xor $e264 $e164))
+(flet ($e281 (or $e112 $e159))
+(flet ($e282 (xor $e240 $e78))
+(flet ($e283 (or $e231 $e258))
+(flet ($e284 (if_then_else $e77 $e136 $e71))
+(flet ($e285 (implies $e279 $e251))
+(flet ($e286 (or $e241 $e238))
+(flet ($e287 (and $e274 $e244))
+(flet ($e288 (or $e185 $e196))
+(flet ($e289 (and $e84 $e267))
+(flet ($e290 (and $e219 $e215))
+(flet ($e291 (or $e268 $e278))
+(flet ($e292 (if_then_else $e186 $e119 $e256))
+(flet ($e293 (iff $e253 $e289))
+(flet ($e294 (not $e151))
+(flet ($e295 (implies $e239 $e294))
+(flet ($e296 (iff $e207 $e290))
+(flet ($e297 (if_then_else $e291 $e182 $e283))
+(flet ($e298 (iff $e131 $e150))
+(flet ($e299 (if_then_else $e184 $e269 $e288))
+(flet ($e300 (xor $e249 $e229))
+(flet ($e301 (not $e272))
+(flet ($e302 (if_then_else $e281 $e261 $e129))
+(flet ($e303 (or $e296 $e183))
+(flet ($e304 (not $e299))
+(flet ($e305 (and $e222 $e178))
+(flet ($e306 (implies $e224 $e255))
+(flet ($e307 (not $e302))
+(flet ($e308 (xor $e271 $e285))
+(flet ($e309 (and $e301 $e305))
+(flet ($e310 (or $e297 $e116))
+(flet ($e311 (and $e287 $e295))
+(flet ($e312 (if_then_else $e310 $e282 $e303))
+(flet ($e313 (and $e304 $e312))
+(flet ($e314 (implies $e211 $e286))
+(flet ($e315 (implies $e273 $e307))
+(flet ($e316 (xor $e165 $e292))
+(flet ($e317 (iff $e306 $e300))
+(flet ($e318 (implies $e313 $e314))
+(flet ($e319 (and $e298 $e194))
+(flet ($e320 (not $e308))
+(flet ($e321 (not $e311))
+(flet ($e322 (not $e321))
+(flet ($e323 (not $e319))
+(flet ($e324 (implies $e280 $e276))
+(flet ($e325 (or $e111 $e323))
+(flet ($e326 (and $e315 $e315))
+(flet ($e327 (iff $e265 $e316))
+(flet ($e328 (iff $e325 $e324))
+(flet ($e329 (implies $e163 $e284))
+(flet ($e330 (not $e320))
+(flet ($e331 (and $e293 $e330))
+(flet ($e332 (or $e326 $e318))
+(flet ($e333 (implies $e328 $e328))
+(flet ($e334 (iff $e309 $e309))
+(flet ($e335 (iff $e334 $e332))
+(flet ($e336 (not $e322))
+(flet ($e337 (and $e331 $e333))
+(flet ($e338 (or $e327 $e337))
+(flet ($e339 (implies $e329 $e317))
+(flet ($e340 (iff $e338 $e335))
+(flet ($e341 (implies $e339 $e340))
+(flet ($e342 (xor $e336 $e341))
+$e342
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect3.smt b/test/regress/regress0/arrays/incorrect3.smt
new file mode 100644
index 000000000..f8184783d
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect3.smt
@@ -0,0 +1,446 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Index))
+:extrafuns ((v2 Element))
+:extrafuns ((v3 Element))
+:extrafuns ((v4 Element))
+:extrafuns ((v5 Element))
+:extrafuns ((v6 Element))
+:formula
+(let (?e7 (store v0 v1 v2))
+(let (?e8 (select ?e7 v1))
+(let (?e9 (select ?e7 v1))
+(flet ($e10 (distinct v0 v0))
+(flet ($e11 (= ?e7 v0))
+(flet ($e12 (distinct v1 v1))
+(flet ($e13 (distinct v4 ?e9))
+(flet ($e14 (distinct v2 v6))
+(flet ($e15 (= ?e9 ?e9))
+(flet ($e16 (distinct v2 v5))
+(flet ($e17 (= v6 v5))
+(flet ($e18 (= v3 v3))
+(flet ($e19 (= v2 v2))
+(flet ($e20 (distinct v2 v2))
+(flet ($e21 (distinct v3 v4))
+(flet ($e22 (distinct v4 ?e9))
+(flet ($e23 (distinct v4 v5))
+(flet ($e24 (= ?e9 v3))
+(flet ($e25 (= v3 ?e8))
+(let (?e26 (ite $e21 v0 v0))
+(let (?e27 (ite $e20 ?e7 v0))
+(let (?e28 (ite $e13 ?e26 v0))
+(let (?e29 (ite $e22 ?e7 ?e7))
+(let (?e30 (ite $e17 ?e29 ?e29))
+(let (?e31 (ite $e16 ?e28 ?e28))
+(let (?e32 (ite $e18 ?e29 ?e30))
+(let (?e33 (ite $e11 ?e28 ?e29))
+(let (?e34 (ite $e15 ?e29 ?e31))
+(let (?e35 (ite $e21 ?e30 ?e26))
+(let (?e36 (ite $e11 ?e32 ?e30))
+(let (?e37 (ite $e14 ?e35 ?e34))
+(let (?e38 (ite $e17 ?e7 ?e28))
+(let (?e39 (ite $e19 ?e7 ?e7))
+(let (?e40 (ite $e23 ?e32 v0))
+(let (?e41 (ite $e12 ?e26 ?e29))
+(let (?e42 (ite $e10 ?e36 ?e27))
+(let (?e43 (ite $e10 v0 ?e7))
+(let (?e44 (ite $e16 ?e41 ?e43))
+(let (?e45 (ite $e11 ?e41 ?e43))
+(let (?e46 (ite $e24 ?e33 ?e32))
+(let (?e47 (ite $e17 ?e38 v0))
+(let (?e48 (ite $e25 ?e27 ?e28))
+(let (?e49 (ite $e20 v1 v1))
+(let (?e50 (ite $e16 v1 ?e49))
+(let (?e51 (ite $e12 ?e50 v1))
+(let (?e52 (ite $e16 ?e51 ?e51))
+(let (?e53 (ite $e19 ?e51 ?e52))
+(let (?e54 (ite $e11 v1 v1))
+(let (?e55 (ite $e14 ?e49 ?e50))
+(let (?e56 (ite $e19 ?e52 ?e52))
+(let (?e57 (ite $e14 ?e51 ?e54))
+(let (?e58 (ite $e20 v1 ?e53))
+(let (?e59 (ite $e15 ?e50 ?e53))
+(let (?e60 (ite $e17 ?e55 ?e49))
+(let (?e61 (ite $e10 ?e60 ?e50))
+(let (?e62 (ite $e23 ?e57 ?e52))
+(let (?e63 (ite $e23 ?e62 ?e61))
+(let (?e64 (ite $e13 ?e51 ?e57))
+(let (?e65 (ite $e21 ?e55 ?e63))
+(let (?e66 (ite $e25 ?e51 ?e56))
+(let (?e67 (ite $e24 ?e50 ?e55))
+(let (?e68 (ite $e14 ?e66 ?e66))
+(let (?e69 (ite $e19 ?e52 ?e67))
+(let (?e70 (ite $e11 ?e53 ?e54))
+(let (?e71 (ite $e18 ?e56 ?e69))
+(let (?e72 (ite $e22 ?e55 ?e52))
+(let (?e73 (ite $e16 v6 v5))
+(let (?e74 (ite $e12 v4 v3))
+(let (?e75 (ite $e25 v6 v3))
+(let (?e76 (ite $e17 v5 v6))
+(let (?e77 (ite $e20 ?e8 v2))
+(let (?e78 (ite $e24 v5 ?e9))
+(let (?e79 (ite $e23 v3 v5))
+(let (?e80 (ite $e13 ?e8 ?e77))
+(let (?e81 (ite $e23 v5 ?e75))
+(let (?e82 (ite $e21 v4 v5))
+(let (?e83 (ite $e19 v5 v5))
+(let (?e84 (ite $e12 v4 ?e78))
+(let (?e85 (ite $e11 ?e76 v4))
+(let (?e86 (ite $e20 ?e77 ?e82))
+(let (?e87 (ite $e12 v5 ?e75))
+(let (?e88 (ite $e18 ?e76 ?e84))
+(let (?e89 (ite $e16 ?e76 ?e75))
+(let (?e90 (ite $e17 ?e77 ?e85))
+(let (?e91 (ite $e17 ?e77 v4))
+(let (?e92 (ite $e10 ?e91 ?e78))
+(let (?e93 (ite $e18 v2 ?e73))
+(let (?e94 (ite $e12 v3 ?e93))
+(let (?e95 (ite $e15 ?e74 ?e73))
+(let (?e96 (ite $e22 ?e95 v2))
+(let (?e97 (ite $e25 v6 v5))
+(let (?e98 (ite $e14 ?e97 v3))
+(let (?e99 (store ?e45 ?e61 ?e74))
+(let (?e100 (select ?e44 ?e60))
+(let (?e101 (select ?e46 ?e57))
+(let (?e102 (store ?e37 ?e67 ?e79))
+(let (?e103 (select ?e33 ?e61))
+(flet ($e104 (= ?e48 ?e43))
+(flet ($e105 (distinct ?e40 ?e35))
+(flet ($e106 (distinct ?e32 ?e44))
+(flet ($e107 (distinct v0 ?e42))
+(flet ($e108 (= ?e32 ?e38))
+(flet ($e109 (distinct ?e41 ?e28))
+(flet ($e110 (distinct ?e34 ?e31))
+(flet ($e111 (= ?e26 v0))
+(flet ($e112 (distinct ?e31 ?e46))
+(flet ($e113 (distinct ?e48 ?e42))
+(flet ($e114 (distinct ?e44 ?e29))
+(flet ($e115 (distinct ?e31 ?e102))
+(flet ($e116 (distinct ?e37 ?e102))
+(flet ($e117 (= ?e38 ?e27))
+(flet ($e118 (distinct ?e46 ?e46))
+(flet ($e119 (distinct ?e26 ?e48))
+(flet ($e120 (= ?e38 ?e33))
+(flet ($e121 (distinct ?e31 ?e48))
+(flet ($e122 (= ?e7 ?e40))
+(flet ($e123 (= ?e27 ?e41))
+(flet ($e124 (distinct ?e39 ?e36))
+(flet ($e125 (distinct ?e36 ?e37))
+(flet ($e126 (distinct ?e44 ?e41))
+(flet ($e127 (= ?e40 ?e34))
+(flet ($e128 (distinct ?e27 ?e43))
+(flet ($e129 (distinct ?e43 ?e32))
+(flet ($e130 (distinct ?e46 ?e44))
+(flet ($e131 (= ?e37 ?e32))
+(flet ($e132 (= ?e99 ?e43))
+(flet ($e133 (distinct ?e42 ?e102))
+(flet ($e134 (distinct ?e30 ?e99))
+(flet ($e135 (distinct ?e27 ?e48))
+(flet ($e136 (= ?e34 ?e41))
+(flet ($e137 (= ?e31 ?e48))
+(flet ($e138 (distinct ?e48 ?e40))
+(flet ($e139 (= ?e46 ?e43))
+(flet ($e140 (distinct ?e32 ?e42))
+(flet ($e141 (distinct ?e42 ?e102))
+(flet ($e142 (= ?e36 ?e27))
+(flet ($e143 (distinct ?e28 ?e45))
+(flet ($e144 (= ?e43 ?e36))
+(flet ($e145 (= ?e32 ?e40))
+(flet ($e146 (= ?e31 ?e28))
+(flet ($e147 (distinct ?e47 ?e102))
+(flet ($e148 (= ?e58 ?e71))
+(flet ($e149 (distinct ?e49 ?e50))
+(flet ($e150 (distinct ?e71 ?e70))
+(flet ($e151 (= ?e57 ?e59))
+(flet ($e152 (distinct ?e66 ?e67))
+(flet ($e153 (distinct ?e56 ?e69))
+(flet ($e154 (distinct ?e62 ?e57))
+(flet ($e155 (distinct ?e67 ?e61))
+(flet ($e156 (distinct ?e63 ?e55))
+(flet ($e157 (distinct ?e63 ?e69))
+(flet ($e158 (= ?e63 ?e64))
+(flet ($e159 (= ?e50 ?e68))
+(flet ($e160 (= ?e72 ?e63))
+(flet ($e161 (distinct ?e59 ?e57))
+(flet ($e162 (distinct ?e61 ?e58))
+(flet ($e163 (distinct ?e53 ?e71))
+(flet ($e164 (distinct ?e57 ?e66))
+(flet ($e165 (= ?e60 ?e64))
+(flet ($e166 (distinct ?e65 ?e54))
+(flet ($e167 (distinct ?e63 ?e72))
+(flet ($e168 (distinct ?e68 ?e66))
+(flet ($e169 (= ?e66 v1))
+(flet ($e170 (distinct ?e65 ?e59))
+(flet ($e171 (= ?e61 v1))
+(flet ($e172 (= v1 ?e53))
+(flet ($e173 (= ?e60 ?e57))
+(flet ($e174 (= ?e54 ?e49))
+(flet ($e175 (distinct ?e53 ?e54))
+(flet ($e176 (= ?e63 ?e70))
+(flet ($e177 (distinct ?e58 ?e60))
+(flet ($e178 (= ?e54 ?e59))
+(flet ($e179 (distinct ?e60 ?e67))
+(flet ($e180 (distinct ?e54 ?e59))
+(flet ($e181 (= ?e71 ?e72))
+(flet ($e182 (= ?e71 ?e66))
+(flet ($e183 (= ?e66 ?e54))
+(flet ($e184 (distinct ?e56 ?e66))
+(flet ($e185 (distinct ?e59 ?e72))
+(flet ($e186 (= ?e50 ?e50))
+(flet ($e187 (= ?e55 ?e63))
+(flet ($e188 (= ?e58 ?e51))
+(flet ($e189 (= ?e67 ?e72))
+(flet ($e190 (distinct ?e66 ?e71))
+(flet ($e191 (distinct ?e66 ?e68))
+(flet ($e192 (= ?e55 ?e56))
+(flet ($e193 (distinct ?e49 ?e63))
+(flet ($e194 (= ?e61 ?e53))
+(flet ($e195 (distinct ?e57 v1))
+(flet ($e196 (distinct ?e66 ?e68))
+(flet ($e197 (distinct ?e60 ?e71))
+(flet ($e198 (= ?e52 ?e53))
+(flet ($e199 (distinct v2 v5))
+(flet ($e200 (= ?e82 ?e84))
+(flet ($e201 (= ?e94 ?e76))
+(flet ($e202 (distinct ?e9 v6))
+(flet ($e203 (= v2 ?e92))
+(flet ($e204 (= ?e83 ?e88))
+(flet ($e205 (= ?e79 ?e81))
+(flet ($e206 (= ?e93 ?e95))
+(flet ($e207 (= ?e86 ?e73))
+(flet ($e208 (= ?e96 v2))
+(flet ($e209 (distinct ?e84 ?e88))
+(flet ($e210 (distinct ?e93 v5))
+(flet ($e211 (distinct v6 ?e92))
+(flet ($e212 (distinct ?e86 ?e96))
+(flet ($e213 (distinct ?e8 ?e86))
+(flet ($e214 (distinct v5 ?e103))
+(flet ($e215 (= ?e77 ?e9))
+(flet ($e216 (= ?e93 ?e75))
+(flet ($e217 (= v6 ?e79))
+(flet ($e218 (= v3 ?e75))
+(flet ($e219 (= ?e79 ?e75))
+(flet ($e220 (= ?e91 ?e92))
+(flet ($e221 (distinct ?e93 ?e78))
+(flet ($e222 (= ?e98 ?e77))
+(flet ($e223 (= ?e76 ?e98))
+(flet ($e224 (distinct ?e88 ?e94))
+(flet ($e225 (distinct ?e9 ?e74))
+(flet ($e226 (distinct ?e79 ?e91))
+(flet ($e227 (= ?e75 v6))
+(flet ($e228 (distinct ?e86 ?e90))
+(flet ($e229 (distinct ?e101 ?e86))
+(flet ($e230 (= ?e93 v5))
+(flet ($e231 (distinct ?e84 ?e94))
+(flet ($e232 (distinct v2 ?e83))
+(flet ($e233 (distinct ?e85 ?e9))
+(flet ($e234 (distinct ?e87 ?e81))
+(flet ($e235 (distinct v5 ?e77))
+(flet ($e236 (= ?e96 ?e87))
+(flet ($e237 (distinct ?e87 ?e100))
+(flet ($e238 (= ?e73 ?e80))
+(flet ($e239 (= v4 ?e87))
+(flet ($e240 (= ?e73 ?e86))
+(flet ($e241 (distinct v2 ?e90))
+(flet ($e242 (distinct ?e74 ?e9))
+(flet ($e243 (= ?e95 ?e8))
+(flet ($e244 (= v2 v6))
+(flet ($e245 (= ?e97 ?e88))
+(flet ($e246 (distinct ?e74 ?e73))
+(flet ($e247 (distinct ?e94 ?e76))
+(flet ($e248 (= ?e103 ?e85))
+(flet ($e249 (= ?e84 ?e85))
+(flet ($e250 (= ?e73 ?e77))
+(flet ($e251 (= ?e73 v6))
+(flet ($e252 (distinct v4 ?e84))
+(flet ($e253 (distinct ?e98 ?e101))
+(flet ($e254 (distinct ?e87 ?e81))
+(flet ($e255 (= ?e94 ?e77))
+(flet ($e256 (= ?e73 v5))
+(flet ($e257 (distinct ?e81 ?e101))
+(flet ($e258 (distinct ?e103 ?e73))
+(flet ($e259 (distinct ?e92 ?e89))
+(flet ($e260 (and $e120 $e210))
+(flet ($e261 (and $e127 $e173))
+(flet ($e262 (iff $e174 $e249))
+(flet ($e263 (if_then_else $e114 $e240 $e185))
+(flet ($e264 (implies $e198 $e156))
+(flet ($e265 (or $e203 $e263))
+(flet ($e266 (and $e255 $e204))
+(flet ($e267 (implies $e243 $e209))
+(flet ($e268 (if_then_else $e222 $e112 $e199))
+(flet ($e269 (or $e145 $e257))
+(flet ($e270 (if_then_else $e10 $e134 $e136))
+(flet ($e271 (or $e264 $e131))
+(flet ($e272 (iff $e218 $e226))
+(flet ($e273 (xor $e152 $e195))
+(flet ($e274 (xor $e262 $e13))
+(flet ($e275 (if_then_else $e177 $e108 $e12))
+(flet ($e276 (not $e247))
+(flet ($e277 (implies $e180 $e275))
+(flet ($e278 (not $e196))
+(flet ($e279 (and $e242 $e151))
+(flet ($e280 (xor $e273 $e148))
+(flet ($e281 (or $e212 $e235))
+(flet ($e282 (if_then_else $e172 $e201 $e25))
+(flet ($e283 (not $e14))
+(flet ($e284 (if_then_else $e267 $e168 $e146))
+(flet ($e285 (and $e219 $e16))
+(flet ($e286 (xor $e272 $e105))
+(flet ($e287 (xor $e21 $e141))
+(flet ($e288 (xor $e160 $e266))
+(flet ($e289 (xor $e208 $e245))
+(flet ($e290 (or $e116 $e135))
+(flet ($e291 (xor $e202 $e225))
+(flet ($e292 (iff $e133 $e268))
+(flet ($e293 (xor $e179 $e278))
+(flet ($e294 (iff $e110 $e287))
+(flet ($e295 (not $e241))
+(flet ($e296 (and $e163 $e106))
+(flet ($e297 (xor $e265 $e122))
+(flet ($e298 (not $e295))
+(flet ($e299 (iff $e164 $e290))
+(flet ($e300 (and $e244 $e143))
+(flet ($e301 (xor $e238 $e189))
+(flet ($e302 (if_then_else $e15 $e284 $e260))
+(flet ($e303 (or $e259 $e297))
+(flet ($e304 (and $e197 $e190))
+(flet ($e305 (iff $e250 $e296))
+(flet ($e306 (implies $e153 $e118))
+(flet ($e307 (or $e288 $e270))
+(flet ($e308 (if_then_else $e298 $e221 $e253))
+(flet ($e309 (if_then_else $e111 $e23 $e170))
+(flet ($e310 (implies $e159 $e228))
+(flet ($e311 (not $e138))
+(flet ($e312 (or $e167 $e11))
+(flet ($e313 (xor $e279 $e289))
+(flet ($e314 (xor $e206 $e227))
+(flet ($e315 (or $e312 $e157))
+(flet ($e316 (xor $e261 $e313))
+(flet ($e317 (implies $e314 $e183))
+(flet ($e318 (or $e317 $e165))
+(flet ($e319 (implies $e22 $e175))
+(flet ($e320 (if_then_else $e213 $e293 $e293))
+(flet ($e321 (iff $e280 $e299))
+(flet ($e322 (not $e169))
+(flet ($e323 (or $e234 $e117))
+(flet ($e324 (not $e150))
+(flet ($e325 (if_then_else $e223 $e258 $e184))
+(flet ($e326 (xor $e237 $e178))
+(flet ($e327 (or $e307 $e19))
+(flet ($e328 (if_then_else $e303 $e192 $e274))
+(flet ($e329 (xor $e230 $e316))
+(flet ($e330 (implies $e239 $e24))
+(flet ($e331 (and $e324 $e154))
+(flet ($e332 (implies $e246 $e132))
+(flet ($e333 (implies $e121 $e128))
+(flet ($e334 (xor $e181 $e107))
+(flet ($e335 (xor $e322 $e321))
+(flet ($e336 (iff $e200 $e139))
+(flet ($e337 (and $e325 $e147))
+(flet ($e338 (iff $e220 $e166))
+(flet ($e339 (implies $e276 $e326))
+(flet ($e340 (if_then_else $e20 $e104 $e254))
+(flet ($e341 (not $e292))
+(flet ($e342 (implies $e306 $e335))
+(flet ($e343 (implies $e294 $e229))
+(flet ($e344 (or $e328 $e186))
+(flet ($e345 (if_then_else $e162 $e333 $e256))
+(flet ($e346 (iff $e125 $e217))
+(flet ($e347 (and $e345 $e336))
+(flet ($e348 (or $e271 $e251))
+(flet ($e349 (implies $e144 $e342))
+(flet ($e350 (if_then_else $e302 $e308 $e302))
+(flet ($e351 (xor $e182 $e347))
+(flet ($e352 (if_then_else $e18 $e188 $e343))
+(flet ($e353 (iff $e126 $e349))
+(flet ($e354 (or $e233 $e320))
+(flet ($e355 (implies $e215 $e341))
+(flet ($e356 (not $e211))
+(flet ($e357 (not $e344))
+(flet ($e358 (or $e334 $e309))
+(flet ($e359 (or $e315 $e337))
+(flet ($e360 (if_then_else $e277 $e155 $e283))
+(flet ($e361 (not $e339))
+(flet ($e362 (not $e232))
+(flet ($e363 (or $e123 $e142))
+(flet ($e364 (not $e363))
+(flet ($e365 (not $e353))
+(flet ($e366 (and $e124 $e231))
+(flet ($e367 (not $e161))
+(flet ($e368 (or $e364 $e137))
+(flet ($e369 (iff $e367 $e109))
+(flet ($e370 (xor $e360 $e310))
+(flet ($e371 (not $e362))
+(flet ($e372 (and $e357 $e331))
+(flet ($e373 (and $e252 $e207))
+(flet ($e374 (if_then_else $e140 $e140 $e115))
+(flet ($e375 (or $e291 $e214))
+(flet ($e376 (not $e351))
+(flet ($e377 (iff $e311 $e236))
+(flet ($e378 (if_then_else $e372 $e248 $e361))
+(flet ($e379 (xor $e374 $e350))
+(flet ($e380 (and $e216 $e370))
+(flet ($e381 (implies $e301 $e224))
+(flet ($e382 (iff $e379 $e130))
+(flet ($e383 (iff $e158 $e354))
+(flet ($e384 (not $e346))
+(flet ($e385 (or $e171 $e338))
+(flet ($e386 (xor $e191 $e378))
+(flet ($e387 (iff $e282 $e330))
+(flet ($e388 (and $e281 $e281))
+(flet ($e389 (implies $e387 $e318))
+(flet ($e390 (implies $e176 $e359))
+(flet ($e391 (and $e358 $e366))
+(flet ($e392 (implies $e365 $e371))
+(flet ($e393 (and $e383 $e340))
+(flet ($e394 (or $e390 $e369))
+(flet ($e395 (not $e389))
+(flet ($e396 (not $e323))
+(flet ($e397 (and $e394 $e193))
+(flet ($e398 (implies $e391 $e368))
+(flet ($e399 (iff $e395 $e398))
+(flet ($e400 (and $e392 $e129))
+(flet ($e401 (or $e17 $e399))
+(flet ($e402 (implies $e396 $e396))
+(flet ($e403 (iff $e401 $e386))
+(flet ($e404 (implies $e376 $e319))
+(flet ($e405 (if_then_else $e269 $e205 $e194))
+(flet ($e406 (and $e380 $e332))
+(flet ($e407 (xor $e402 $e403))
+(flet ($e408 (if_then_else $e329 $e113 $e382))
+(flet ($e409 (and $e286 $e187))
+(flet ($e410 (implies $e393 $e300))
+(flet ($e411 (implies $e388 $e355))
+(flet ($e412 (implies $e409 $e352))
+(flet ($e413 (implies $e397 $e405))
+(flet ($e414 (xor $e373 $e400))
+(flet ($e415 (not $e285))
+(flet ($e416 (not $e119))
+(flet ($e417 (not $e305))
+(flet ($e418 (xor $e348 $e408))
+(flet ($e419 (if_then_else $e149 $e304 $e415))
+(flet ($e420 (if_then_else $e407 $e377 $e419))
+(flet ($e421 (xor $e381 $e385))
+(flet ($e422 (not $e420))
+(flet ($e423 (iff $e422 $e411))
+(flet ($e424 (or $e375 $e404))
+(flet ($e425 (xor $e414 $e384))
+(flet ($e426 (implies $e327 $e406))
+(flet ($e427 (implies $e424 $e412))
+(flet ($e428 (implies $e421 $e417))
+(flet ($e429 (and $e427 $e413))
+(flet ($e430 (or $e410 $e356))
+(flet ($e431 (if_then_else $e429 $e425 $e418))
+(flet ($e432 (xor $e430 $e430))
+(flet ($e433 (iff $e431 $e426))
+(flet ($e434 (and $e432 $e423))
+(flet ($e435 (xor $e434 $e428))
+(flet ($e436 (xor $e433 $e433))
+(flet ($e437 (and $e416 $e435))
+(flet ($e438 (implies $e437 $e436))
+$e438
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect4.smt b/test/regress/regress0/arrays/incorrect4.smt
new file mode 100644
index 000000000..62f28834a
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect4.smt
@@ -0,0 +1,170 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Index))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Index))
+:extrafuns ((v4 Element))
+:extrafuns ((v5 Element))
+:extrafuns ((v6 Element))
+:formula
+(flet ($e7 (= v0 v0))
+(flet ($e8 (= v2 v2))
+(flet ($e9 (= v1 v2))
+(flet ($e10 (distinct v1 v2))
+(flet ($e11 (distinct v3 v2))
+(flet ($e12 (distinct v5 v5))
+(flet ($e13 (= v6 v4))
+(let (?e14 (ite $e9 v0 v0))
+(let (?e15 (ite $e7 v0 v0))
+(let (?e16 (ite $e11 ?e14 ?e15))
+(let (?e17 (ite $e8 ?e15 ?e15))
+(let (?e18 (ite $e10 ?e16 v0))
+(let (?e19 (ite $e9 ?e14 ?e15))
+(let (?e20 (ite $e12 ?e17 ?e19))
+(let (?e21 (ite $e8 ?e20 ?e16))
+(let (?e22 (ite $e13 ?e20 ?e16))
+(let (?e23 (ite $e10 v3 v1))
+(let (?e24 (ite $e13 v2 v3))
+(let (?e25 (ite $e11 v2 ?e23))
+(let (?e26 (ite $e12 v2 ?e23))
+(let (?e27 (ite $e8 ?e25 ?e23))
+(let (?e28 (ite $e7 v3 ?e26))
+(let (?e29 (ite $e9 ?e28 v1))
+(let (?e30 (ite $e8 v5 v5))
+(let (?e31 (ite $e10 v4 ?e30))
+(let (?e32 (ite $e11 v6 ?e30))
+(let (?e33 (ite $e7 ?e31 v4))
+(let (?e34 (ite $e10 ?e30 ?e32))
+(let (?e35 (ite $e9 v5 ?e32))
+(let (?e36 (ite $e12 ?e30 v4))
+(let (?e37 (ite $e11 v6 v4))
+(let (?e38 (ite $e12 ?e32 ?e33))
+(let (?e39 (ite $e8 v4 v6))
+(let (?e40 (ite $e13 ?e32 ?e33))
+(let (?e41 (store ?e17 v2 ?e33))
+(let (?e42 (select ?e41 v2))
+(flet ($e43 (= ?e17 ?e22))
+(flet ($e44 (distinct v0 ?e20))
+(flet ($e45 (= ?e14 ?e22))
+(flet ($e46 (= ?e17 ?e17))
+(flet ($e47 (distinct ?e21 ?e17))
+(flet ($e48 (= ?e41 ?e14))
+(flet ($e49 (distinct ?e19 ?e14))
+(flet ($e50 (= ?e14 ?e22))
+(flet ($e51 (= ?e20 ?e21))
+(flet ($e52 (= ?e14 ?e21))
+(flet ($e53 (= ?e19 ?e20))
+(flet ($e54 (= ?e22 ?e20))
+(flet ($e55 (= ?e15 ?e17))
+(flet ($e56 (= ?e16 ?e19))
+(flet ($e57 (= ?e16 ?e15))
+(flet ($e58 (distinct ?e41 ?e41))
+(flet ($e59 (distinct ?e20 ?e21))
+(flet ($e60 (distinct ?e17 ?e14))
+(flet ($e61 (distinct ?e15 ?e22))
+(flet ($e62 (distinct ?e22 ?e22))
+(flet ($e63 (= ?e18 v0))
+(flet ($e64 (= ?e27 ?e28))
+(flet ($e65 (distinct ?e23 v2))
+(flet ($e66 (= ?e23 ?e25))
+(flet ($e67 (distinct ?e24 ?e24))
+(flet ($e68 (distinct ?e28 ?e28))
+(flet ($e69 (= v1 ?e24))
+(flet ($e70 (= ?e29 ?e28))
+(flet ($e71 (distinct v3 ?e26))
+(flet ($e72 (distinct ?e36 ?e33))
+(flet ($e73 (distinct ?e30 v4))
+(flet ($e74 (= ?e39 ?e39))
+(flet ($e75 (= v4 ?e30))
+(flet ($e76 (= ?e33 ?e38))
+(flet ($e77 (= ?e34 ?e40))
+(flet ($e78 (= ?e36 ?e42))
+(flet ($e79 (distinct v4 ?e34))
+(flet ($e80 (distinct ?e30 ?e37))
+(flet ($e81 (= v6 ?e37))
+(flet ($e82 (= v5 ?e39))
+(flet ($e83 (distinct ?e35 ?e30))
+(flet ($e84 (distinct ?e39 ?e38))
+(flet ($e85 (distinct ?e32 ?e30))
+(flet ($e86 (= ?e42 ?e33))
+(flet ($e87 (distinct ?e36 v5))
+(flet ($e88 (distinct ?e30 ?e36))
+(flet ($e89 (= ?e42 v4))
+(flet ($e90 (distinct ?e42 ?e30))
+(flet ($e91 (distinct ?e36 v5))
+(flet ($e92 (= ?e34 ?e38))
+(flet ($e93 (distinct ?e42 v6))
+(flet ($e94 (distinct ?e37 ?e32))
+(flet ($e95 (distinct v6 ?e39))
+(flet ($e96 (= ?e35 ?e37))
+(flet ($e97 (= ?e42 ?e31))
+(flet ($e98 (implies $e89 $e93))
+(flet ($e99 (xor $e10 $e77))
+(flet ($e100 (or $e8 $e71))
+(flet ($e101 (iff $e7 $e43))
+(flet ($e102 (or $e46 $e54))
+(flet ($e103 (and $e78 $e50))
+(flet ($e104 (if_then_else $e67 $e58 $e82))
+(flet ($e105 (not $e85))
+(flet ($e106 (implies $e105 $e9))
+(flet ($e107 (xor $e83 $e66))
+(flet ($e108 (if_then_else $e53 $e57 $e107))
+(flet ($e109 (if_then_else $e97 $e13 $e106))
+(flet ($e110 (and $e60 $e79))
+(flet ($e111 (not $e99))
+(flet ($e112 (implies $e47 $e104))
+(flet ($e113 (and $e73 $e109))
+(flet ($e114 (or $e68 $e11))
+(flet ($e115 (xor $e44 $e96))
+(flet ($e116 (iff $e75 $e102))
+(flet ($e117 (if_then_else $e90 $e86 $e94))
+(flet ($e118 (xor $e62 $e70))
+(flet ($e119 (not $e113))
+(flet ($e120 (iff $e103 $e115))
+(flet ($e121 (or $e98 $e80))
+(flet ($e122 (not $e49))
+(flet ($e123 (or $e48 $e101))
+(flet ($e124 (xor $e108 $e123))
+(flet ($e125 (xor $e91 $e118))
+(flet ($e126 (xor $e56 $e84))
+(flet ($e127 (if_then_else $e110 $e114 $e117))
+(flet ($e128 (iff $e87 $e88))
+(flet ($e129 (implies $e95 $e127))
+(flet ($e130 (and $e52 $e116))
+(flet ($e131 (not $e69))
+(flet ($e132 (iff $e112 $e130))
+(flet ($e133 (or $e128 $e72))
+(flet ($e134 (if_then_else $e133 $e74 $e124))
+(flet ($e135 (implies $e55 $e51))
+(flet ($e136 (and $e126 $e61))
+(flet ($e137 (xor $e65 $e81))
+(flet ($e138 (or $e122 $e111))
+(flet ($e139 (or $e121 $e138))
+(flet ($e140 (implies $e119 $e136))
+(flet ($e141 (not $e140))
+(flet ($e142 (if_then_else $e12 $e59 $e132))
+(flet ($e143 (or $e142 $e129))
+(flet ($e144 (and $e45 $e63))
+(flet ($e145 (if_then_else $e76 $e141 $e131))
+(flet ($e146 (implies $e145 $e137))
+(flet ($e147 (if_then_else $e139 $e139 $e146))
+(flet ($e148 (xor $e144 $e147))
+(flet ($e149 (not $e120))
+(flet ($e150 (iff $e125 $e92))
+(flet ($e151 (or $e135 $e135))
+(flet ($e152 (or $e151 $e100))
+(flet ($e153 (implies $e149 $e152))
+(flet ($e154 (not $e134))
+(flet ($e155 (xor $e154 $e150))
+(flet ($e156 (if_then_else $e64 $e155 $e64))
+(flet ($e157 (or $e153 $e153))
+(flet ($e158 (not $e143))
+(flet ($e159 (and $e148 $e157))
+(flet ($e160 (xor $e159 $e159))
+(flet ($e161 (and $e156 $e158))
+(flet ($e162 (xor $e160 $e161))
+$e162
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect5.smt b/test/regress/regress0/arrays/incorrect5.smt
new file mode 100644
index 000000000..a9c8d854c
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect5.smt
@@ -0,0 +1,313 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Index))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Index))
+:extrafuns ((v4 Element))
+:formula
+(let (?e5 (store v0 v3 v4))
+(let (?e6 (select v0 v2))
+(let (?e7 (select ?e5 v2))
+(flet ($e8 (= v0 ?e5))
+(flet ($e9 (distinct v2 v1))
+(flet ($e10 (= v3 v2))
+(flet ($e11 (distinct ?e7 ?e7))
+(flet ($e12 (distinct ?e7 ?e7))
+(flet ($e13 (= ?e7 v4))
+(flet ($e14 (distinct ?e6 v4))
+(let (?e15 (ite $e12 ?e5 ?e5))
+(let (?e16 (ite $e13 ?e15 ?e5))
+(let (?e17 (ite $e13 ?e16 ?e5))
+(let (?e18 (ite $e11 ?e15 v0))
+(let (?e19 (ite $e8 ?e5 ?e18))
+(let (?e20 (ite $e10 ?e5 ?e15))
+(let (?e21 (ite $e9 ?e17 ?e5))
+(let (?e22 (ite $e10 ?e16 ?e15))
+(let (?e23 (ite $e14 ?e5 ?e16))
+(let (?e24 (ite $e14 v3 v3))
+(let (?e25 (ite $e10 v2 v1))
+(let (?e26 (ite $e13 ?e25 v1))
+(let (?e27 (ite $e11 v3 ?e24))
+(let (?e28 (ite $e12 ?e24 ?e27))
+(let (?e29 (ite $e9 v1 ?e28))
+(let (?e30 (ite $e12 ?e28 ?e28))
+(let (?e31 (ite $e11 ?e30 ?e25))
+(let (?e32 (ite $e12 v2 ?e27))
+(let (?e33 (ite $e8 ?e25 v2))
+(let (?e34 (ite $e8 ?e7 v4))
+(let (?e35 (ite $e12 ?e6 ?e6))
+(let (?e36 (ite $e11 ?e34 ?e35))
+(let (?e37 (ite $e14 ?e6 ?e6))
+(let (?e38 (ite $e10 v4 ?e34))
+(let (?e39 (ite $e13 ?e6 ?e37))
+(let (?e40 (ite $e10 ?e36 ?e36))
+(let (?e41 (ite $e14 v4 ?e37))
+(let (?e42 (ite $e13 ?e41 ?e37))
+(let (?e43 (ite $e9 ?e36 ?e6))
+(let (?e44 (store ?e16 ?e32 ?e37))
+(let (?e45 (select ?e15 v2))
+(let (?e46 (select ?e18 ?e33))
+(let (?e47 (store ?e44 ?e28 ?e39))
+(let (?e48 (select ?e20 v2))
+(flet ($e49 (distinct ?e44 ?e21))
+(flet ($e50 (= ?e18 ?e18))
+(flet ($e51 (distinct ?e44 ?e15))
+(flet ($e52 (distinct ?e21 ?e19))
+(flet ($e53 (= ?e47 v0))
+(flet ($e54 (distinct v0 ?e17))
+(flet ($e55 (= ?e21 ?e21))
+(flet ($e56 (= ?e19 ?e23))
+(flet ($e57 (= ?e44 ?e5))
+(flet ($e58 (= ?e17 ?e21))
+(flet ($e59 (= ?e44 ?e23))
+(flet ($e60 (distinct ?e47 ?e19))
+(flet ($e61 (distinct ?e5 ?e20))
+(flet ($e62 (distinct ?e20 ?e19))
+(flet ($e63 (= v0 ?e16))
+(flet ($e64 (distinct ?e16 ?e5))
+(flet ($e65 (distinct ?e44 ?e17))
+(flet ($e66 (= ?e5 ?e5))
+(flet ($e67 (distinct ?e47 ?e5))
+(flet ($e68 (distinct ?e19 ?e5))
+(flet ($e69 (distinct ?e18 ?e16))
+(flet ($e70 (= ?e18 ?e22))
+(flet ($e71 (distinct ?e29 v1))
+(flet ($e72 (distinct ?e26 ?e26))
+(flet ($e73 (distinct ?e27 ?e26))
+(flet ($e74 (distinct v3 ?e31))
+(flet ($e75 (= ?e25 ?e28))
+(flet ($e76 (= ?e32 v2))
+(flet ($e77 (= v1 ?e26))
+(flet ($e78 (= ?e32 ?e29))
+(flet ($e79 (distinct ?e24 ?e29))
+(flet ($e80 (= v2 ?e32))
+(flet ($e81 (= v2 ?e24))
+(flet ($e82 (distinct ?e32 ?e25))
+(flet ($e83 (= ?e31 v3))
+(flet ($e84 (= ?e29 ?e29))
+(flet ($e85 (distinct v3 v1))
+(flet ($e86 (= ?e28 ?e27))
+(flet ($e87 (distinct ?e27 ?e26))
+(flet ($e88 (distinct ?e26 ?e26))
+(flet ($e89 (distinct ?e29 v3))
+(flet ($e90 (= ?e26 ?e32))
+(flet ($e91 (= ?e30 v1))
+(flet ($e92 (= ?e31 ?e25))
+(flet ($e93 (= ?e32 v1))
+(flet ($e94 (distinct ?e26 ?e31))
+(flet ($e95 (distinct ?e29 ?e26))
+(flet ($e96 (= v3 v3))
+(flet ($e97 (= v2 ?e29))
+(flet ($e98 (distinct v3 v2))
+(flet ($e99 (= ?e29 v2))
+(flet ($e100 (distinct v1 v3))
+(flet ($e101 (= v2 ?e29))
+(flet ($e102 (distinct ?e24 ?e28))
+(flet ($e103 (= ?e31 ?e30))
+(flet ($e104 (distinct ?e32 ?e33))
+(flet ($e105 (= ?e34 v4))
+(flet ($e106 (= ?e43 ?e45))
+(flet ($e107 (= ?e48 ?e48))
+(flet ($e108 (= ?e46 ?e34))
+(flet ($e109 (= ?e40 ?e40))
+(flet ($e110 (= ?e35 ?e7))
+(flet ($e111 (distinct ?e37 ?e37))
+(flet ($e112 (= ?e34 ?e7))
+(flet ($e113 (= ?e37 ?e6))
+(flet ($e114 (= ?e48 ?e41))
+(flet ($e115 (distinct ?e6 ?e48))
+(flet ($e116 (distinct v4 ?e45))
+(flet ($e117 (distinct ?e45 ?e45))
+(flet ($e118 (distinct ?e42 ?e35))
+(flet ($e119 (distinct ?e37 ?e39))
+(flet ($e120 (distinct ?e6 ?e40))
+(flet ($e121 (= ?e34 ?e41))
+(flet ($e122 (distinct ?e37 ?e46))
+(flet ($e123 (= ?e7 ?e34))
+(flet ($e124 (= ?e35 ?e45))
+(flet ($e125 (= ?e40 ?e37))
+(flet ($e126 (= ?e39 ?e38))
+(flet ($e127 (= ?e46 ?e34))
+(flet ($e128 (= ?e42 ?e48))
+(flet ($e129 (= ?e34 ?e37))
+(flet ($e130 (distinct v4 v4))
+(flet ($e131 (= ?e41 ?e40))
+(flet ($e132 (distinct ?e43 ?e38))
+(flet ($e133 (distinct ?e39 ?e45))
+(flet ($e134 (distinct ?e42 v4))
+(flet ($e135 (= ?e48 ?e34))
+(flet ($e136 (distinct ?e38 ?e35))
+(flet ($e137 (= ?e41 ?e45))
+(flet ($e138 (distinct ?e7 ?e35))
+(flet ($e139 (= ?e7 ?e35))
+(flet ($e140 (= ?e46 ?e7))
+(flet ($e141 (distinct ?e45 v4))
+(flet ($e142 (= v4 ?e35))
+(flet ($e143 (= ?e48 ?e43))
+(flet ($e144 (= ?e37 ?e35))
+(flet ($e145 (distinct ?e34 v4))
+(flet ($e146 (distinct ?e35 ?e41))
+(flet ($e147 (= ?e40 ?e34))
+(flet ($e148 (= ?e46 ?e35))
+(flet ($e149 (= ?e43 ?e41))
+(flet ($e150 (= ?e39 ?e43))
+(flet ($e151 (distinct ?e41 ?e46))
+(flet ($e152 (= ?e7 ?e42))
+(flet ($e153 (distinct ?e43 ?e38))
+(flet ($e154 (distinct ?e37 ?e6))
+(flet ($e155 (= ?e7 ?e7))
+(flet ($e156 (distinct ?e43 ?e7))
+(flet ($e157 (= ?e43 ?e39))
+(flet ($e158 (distinct ?e43 ?e42))
+(flet ($e159 (= ?e39 ?e46))
+(flet ($e160 (distinct ?e41 ?e6))
+(flet ($e161 (= ?e7 ?e43))
+(flet ($e162 (= ?e39 ?e40))
+(flet ($e163 (distinct ?e42 v4))
+(flet ($e164 (distinct ?e35 v4))
+(flet ($e165 (= ?e40 ?e46))
+(flet ($e166 (distinct ?e45 ?e36))
+(flet ($e167 (iff $e137 $e129))
+(flet ($e168 (not $e106))
+(flet ($e169 (if_then_else $e86 $e140 $e85))
+(flet ($e170 (if_then_else $e136 $e56 $e69))
+(flet ($e171 (if_then_else $e169 $e79 $e100))
+(flet ($e172 (xor $e145 $e92))
+(flet ($e173 (implies $e64 $e101))
+(flet ($e174 (not $e171))
+(flet ($e175 (xor $e96 $e71))
+(flet ($e176 (and $e75 $e135))
+(flet ($e177 (or $e143 $e91))
+(flet ($e178 (not $e111))
+(flet ($e179 (if_then_else $e175 $e94 $e168))
+(flet ($e180 (not $e110))
+(flet ($e181 (or $e72 $e8))
+(flet ($e182 (not $e130))
+(flet ($e183 (iff $e10 $e88))
+(flet ($e184 (iff $e103 $e165))
+(flet ($e185 (xor $e76 $e13))
+(flet ($e186 (xor $e172 $e116))
+(flet ($e187 (iff $e180 $e102))
+(flet ($e188 (iff $e183 $e126))
+(flet ($e189 (iff $e121 $e186))
+(flet ($e190 (implies $e90 $e139))
+(flet ($e191 (iff $e124 $e58))
+(flet ($e192 (xor $e57 $e80))
+(flet ($e193 (xor $e133 $e164))
+(flet ($e194 (implies $e60 $e179))
+(flet ($e195 (iff $e170 $e87))
+(flet ($e196 (if_then_else $e63 $e107 $e189))
+(flet ($e197 (xor $e125 $e182))
+(flet ($e198 (implies $e55 $e141))
+(flet ($e199 (xor $e148 $e73))
+(flet ($e200 (iff $e195 $e74))
+(flet ($e201 (not $e67))
+(flet ($e202 (implies $e153 $e166))
+(flet ($e203 (iff $e190 $e118))
+(flet ($e204 (iff $e70 $e187))
+(flet ($e205 (implies $e152 $e131))
+(flet ($e206 (xor $e84 $e122))
+(flet ($e207 (or $e108 $e159))
+(flet ($e208 (implies $e12 $e196))
+(flet ($e209 (xor $e193 $e9))
+(flet ($e210 (implies $e146 $e138))
+(flet ($e211 (and $e194 $e147))
+(flet ($e212 (or $e104 $e65))
+(flet ($e213 (or $e54 $e200))
+(flet ($e214 (and $e114 $e157))
+(flet ($e215 (not $e158))
+(flet ($e216 (implies $e61 $e211))
+(flet ($e217 (implies $e109 $e151))
+(flet ($e218 (if_then_else $e199 $e134 $e132))
+(flet ($e219 (iff $e167 $e119))
+(flet ($e220 (and $e49 $e185))
+(flet ($e221 (or $e155 $e113))
+(flet ($e222 (not $e192))
+(flet ($e223 (not $e99))
+(flet ($e224 (if_then_else $e93 $e89 $e81))
+(flet ($e225 (and $e77 $e221))
+(flet ($e226 (if_then_else $e78 $e214 $e178))
+(flet ($e227 (and $e62 $e123))
+(flet ($e228 (and $e154 $e144))
+(flet ($e229 (xor $e14 $e225))
+(flet ($e230 (if_then_else $e163 $e217 $e163))
+(flet ($e231 (not $e230))
+(flet ($e232 (implies $e174 $e11))
+(flet ($e233 (not $e52))
+(flet ($e234 (if_then_else $e160 $e117 $e53))
+(flet ($e235 (not $e105))
+(flet ($e236 (iff $e51 $e177))
+(flet ($e237 (iff $e203 $e176))
+(flet ($e238 (if_then_else $e120 $e233 $e207))
+(flet ($e239 (or $e50 $e59))
+(flet ($e240 (xor $e115 $e181))
+(flet ($e241 (xor $e112 $e68))
+(flet ($e242 (if_then_else $e236 $e97 $e227))
+(flet ($e243 (not $e66))
+(flet ($e244 (not $e98))
+(flet ($e245 (not $e234))
+(flet ($e246 (if_then_else $e238 $e127 $e184))
+(flet ($e247 (not $e215))
+(flet ($e248 (implies $e224 $e209))
+(flet ($e249 (xor $e220 $e229))
+(flet ($e250 (if_then_else $e128 $e128 $e149))
+(flet ($e251 (implies $e208 $e161))
+(flet ($e252 (or $e222 $e240))
+(flet ($e253 (xor $e201 $e218))
+(flet ($e254 (xor $e232 $e251))
+(flet ($e255 (xor $e244 $e250))
+(flet ($e256 (iff $e249 $e212))
+(flet ($e257 (if_then_else $e142 $e255 $e253))
+(flet ($e258 (if_then_else $e256 $e228 $e198))
+(flet ($e259 (xor $e156 $e243))
+(flet ($e260 (implies $e239 $e242))
+(flet ($e261 (or $e257 $e206))
+(flet ($e262 (and $e204 $e150))
+(flet ($e263 (not $e248))
+(flet ($e264 (and $e258 $e202))
+(flet ($e265 (and $e226 $e247))
+(flet ($e266 (implies $e162 $e265))
+(flet ($e267 (if_then_else $e213 $e173 $e213))
+(flet ($e268 (xor $e246 $e267))
+(flet ($e269 (implies $e252 $e262))
+(flet ($e270 (or $e205 $e223))
+(flet ($e271 (not $e188))
+(flet ($e272 (not $e260))
+(flet ($e273 (and $e219 $e263))
+(flet ($e274 (xor $e95 $e259))
+(flet ($e275 (or $e191 $e191))
+(flet ($e276 (or $e197 $e261))
+(flet ($e277 (and $e216 $e254))
+(flet ($e278 (or $e276 $e264))
+(flet ($e279 (iff $e271 $e237))
+(flet ($e280 (iff $e279 $e269))
+(flet ($e281 (xor $e270 $e210))
+(flet ($e282 (and $e281 $e241))
+(flet ($e283 (and $e235 $e235))
+(flet ($e284 (xor $e283 $e283))
+(flet ($e285 (and $e83 $e277))
+(flet ($e286 (iff $e231 $e278))
+(flet ($e287 (implies $e272 $e275))
+(flet ($e288 (not $e273))
+(flet ($e289 (not $e245))
+(flet ($e290 (and $e274 $e282))
+(flet ($e291 (implies $e266 $e280))
+(flet ($e292 (implies $e288 $e287))
+(flet ($e293 (not $e268))
+(flet ($e294 (xor $e293 $e284))
+(flet ($e295 (if_then_else $e82 $e285 $e290))
+(flet ($e296 (or $e291 $e295))
+(flet ($e297 (not $e286))
+(flet ($e298 (implies $e292 $e292))
+(flet ($e299 (and $e294 $e297))
+(flet ($e300 (implies $e299 $e299))
+(flet ($e301 (xor $e298 $e300))
+(flet ($e302 (if_then_else $e301 $e289 $e289))
+(flet ($e303 (not $e296))
+(flet ($e304 (implies $e302 $e302))
+(flet ($e305 (implies $e304 $e303))
+$e305
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect6.smt b/test/regress/regress0/arrays/incorrect6.smt
new file mode 100644
index 000000000..5e9de90aa
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect6.smt
@@ -0,0 +1,265 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Array))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Index))
+:extrafuns ((v4 Element))
+:extrafuns ((v5 Element))
+:extrafuns ((v6 Element))
+:extrafuns ((v7 Element))
+:extrafuns ((v8 Element))
+:formula
+(let (?e9 (select v0 v3))
+(flet ($e10 (= v0 v1))
+(flet ($e11 (distinct v2 v2))
+(flet ($e12 (= v3 v2))
+(flet ($e13 (distinct ?e9 v5))
+(flet ($e14 (= ?e9 v6))
+(flet ($e15 (= ?e9 ?e9))
+(flet ($e16 (= v4 v8))
+(flet ($e17 (= v4 v8))
+(flet ($e18 (= v8 v6))
+(flet ($e19 (= ?e9 v5))
+(flet ($e20 (distinct v7 v5))
+(let (?e21 (ite $e20 v0 v0))
+(let (?e22 (ite $e20 ?e21 ?e21))
+(let (?e23 (ite $e11 v1 v0))
+(let (?e24 (ite $e17 ?e22 ?e22))
+(let (?e25 (ite $e10 ?e22 ?e23))
+(let (?e26 (ite $e17 ?e24 v0))
+(let (?e27 (ite $e16 v0 v1))
+(let (?e28 (ite $e13 v1 ?e22))
+(let (?e29 (ite $e18 ?e26 ?e26))
+(let (?e30 (ite $e12 ?e24 ?e28))
+(let (?e31 (ite $e19 ?e27 ?e28))
+(let (?e32 (ite $e15 ?e29 ?e25))
+(let (?e33 (ite $e14 ?e26 ?e26))
+(let (?e34 (ite $e12 v2 v3))
+(let (?e35 (ite $e13 ?e34 ?e34))
+(let (?e36 (ite $e16 v3 v3))
+(let (?e37 (ite $e10 ?e34 ?e34))
+(let (?e38 (ite $e11 ?e35 v2))
+(let (?e39 (ite $e19 ?e34 ?e37))
+(let (?e40 (ite $e14 ?e35 ?e34))
+(let (?e41 (ite $e20 ?e40 v3))
+(let (?e42 (ite $e17 ?e39 ?e36))
+(let (?e43 (ite $e20 ?e40 v2))
+(let (?e44 (ite $e15 ?e43 v2))
+(let (?e45 (ite $e18 ?e43 v2))
+(let (?e46 (ite $e11 v6 v7))
+(let (?e47 (ite $e19 v5 v6))
+(let (?e48 (ite $e10 v8 v5))
+(let (?e49 (ite $e11 v6 ?e48))
+(let (?e50 (ite $e15 ?e9 ?e49))
+(let (?e51 (ite $e15 v4 v4))
+(let (?e52 (ite $e12 ?e50 ?e47))
+(let (?e53 (ite $e13 v6 ?e51))
+(let (?e54 (ite $e18 ?e49 ?e46))
+(let (?e55 (ite $e20 ?e9 ?e50))
+(let (?e56 (ite $e17 ?e53 ?e52))
+(let (?e57 (ite $e14 ?e47 ?e9))
+(let (?e58 (ite $e16 ?e48 ?e52))
+(let (?e59 (select ?e23 ?e39))
+(flet ($e60 (distinct v1 ?e22))
+(flet ($e61 (= ?e25 ?e25))
+(flet ($e62 (distinct ?e32 ?e27))
+(flet ($e63 (distinct ?e31 ?e25))
+(flet ($e64 (distinct ?e22 ?e28))
+(flet ($e65 (= v1 ?e28))
+(flet ($e66 (distinct ?e25 ?e28))
+(flet ($e67 (= v1 ?e25))
+(flet ($e68 (= ?e30 v0))
+(flet ($e69 (distinct ?e25 ?e23))
+(flet ($e70 (distinct ?e21 ?e24))
+(flet ($e71 (= ?e30 ?e25))
+(flet ($e72 (distinct ?e21 v0))
+(flet ($e73 (distinct v1 ?e29))
+(flet ($e74 (distinct ?e32 ?e31))
+(flet ($e75 (distinct ?e25 ?e23))
+(flet ($e76 (= ?e32 ?e21))
+(flet ($e77 (distinct ?e32 ?e31))
+(flet ($e78 (distinct ?e28 ?e24))
+(flet ($e79 (distinct v1 ?e26))
+(flet ($e80 (distinct v1 ?e23))
+(flet ($e81 (distinct v1 v0))
+(flet ($e82 (= ?e29 v1))
+(flet ($e83 (distinct ?e29 ?e22))
+(flet ($e84 (distinct v0 ?e29))
+(flet ($e85 (= ?e28 ?e27))
+(flet ($e86 (distinct ?e25 ?e21))
+(flet ($e87 (distinct ?e28 ?e25))
+(flet ($e88 (= ?e29 ?e21))
+(flet ($e89 (= ?e31 ?e33))
+(flet ($e90 (distinct ?e45 ?e35))
+(flet ($e91 (= ?e37 v3))
+(flet ($e92 (distinct ?e43 ?e35))
+(flet ($e93 (distinct v2 v3))
+(flet ($e94 (distinct ?e40 ?e45))
+(flet ($e95 (distinct ?e38 v3))
+(flet ($e96 (distinct ?e43 ?e37))
+(flet ($e97 (= ?e36 ?e44))
+(flet ($e98 (= ?e39 ?e36))
+(flet ($e99 (distinct ?e38 ?e44))
+(flet ($e100 (distinct ?e44 ?e34))
+(flet ($e101 (distinct ?e43 ?e40))
+(flet ($e102 (distinct v2 v3))
+(flet ($e103 (= ?e43 ?e41))
+(flet ($e104 (= ?e38 ?e40))
+(flet ($e105 (= v3 ?e37))
+(flet ($e106 (= v2 ?e44))
+(flet ($e107 (distinct ?e34 ?e45))
+(flet ($e108 (distinct ?e39 ?e37))
+(flet ($e109 (= ?e36 ?e38))
+(flet ($e110 (= v3 ?e38))
+(flet ($e111 (= ?e39 v3))
+(flet ($e112 (distinct ?e44 ?e45))
+(flet ($e113 (distinct ?e41 ?e40))
+(flet ($e114 (= ?e38 ?e40))
+(flet ($e115 (distinct ?e44 ?e38))
+(flet ($e116 (distinct ?e37 ?e44))
+(flet ($e117 (distinct ?e34 ?e39))
+(flet ($e118 (distinct ?e37 ?e40))
+(flet ($e119 (distinct ?e37 ?e36))
+(flet ($e120 (distinct ?e45 ?e42))
+(flet ($e121 (distinct ?e58 ?e48))
+(flet ($e122 (distinct ?e9 v7))
+(flet ($e123 (distinct v7 v4))
+(flet ($e124 (= ?e59 ?e59))
+(flet ($e125 (= ?e46 ?e49))
+(flet ($e126 (distinct ?e58 ?e48))
+(flet ($e127 (distinct ?e53 ?e46))
+(flet ($e128 (distinct v4 ?e47))
+(flet ($e129 (distinct v4 v5))
+(flet ($e130 (= v7 ?e49))
+(flet ($e131 (distinct v8 v6))
+(flet ($e132 (= ?e48 ?e51))
+(flet ($e133 (distinct ?e51 ?e47))
+(flet ($e134 (= ?e55 ?e49))
+(flet ($e135 (= ?e54 ?e58))
+(flet ($e136 (distinct ?e47 ?e57))
+(flet ($e137 (= ?e48 v4))
+(flet ($e138 (= ?e48 ?e55))
+(flet ($e139 (distinct v8 ?e48))
+(flet ($e140 (distinct ?e55 v7))
+(flet ($e141 (= v4 v6))
+(flet ($e142 (distinct ?e56 ?e53))
+(flet ($e143 (distinct ?e58 ?e49))
+(flet ($e144 (distinct ?e50 v5))
+(flet ($e145 (distinct ?e58 ?e47))
+(flet ($e146 (distinct v8 ?e56))
+(flet ($e147 (= ?e50 ?e52))
+(flet ($e148 (xor $e19 $e117))
+(flet ($e149 (or $e106 $e64))
+(flet ($e150 (or $e74 $e14))
+(flet ($e151 (or $e127 $e110))
+(flet ($e152 (iff $e140 $e113))
+(flet ($e153 (implies $e71 $e144))
+(flet ($e154 (iff $e142 $e85))
+(flet ($e155 (implies $e13 $e13))
+(flet ($e156 (not $e118))
+(flet ($e157 (if_then_else $e123 $e62 $e95))
+(flet ($e158 (implies $e63 $e101))
+(flet ($e159 (iff $e77 $e125))
+(flet ($e160 (or $e73 $e80))
+(flet ($e161 (if_then_else $e143 $e99 $e107))
+(flet ($e162 (iff $e72 $e102))
+(flet ($e163 (or $e100 $e126))
+(flet ($e164 (or $e91 $e162))
+(flet ($e165 (iff $e11 $e75))
+(flet ($e166 (and $e84 $e158))
+(flet ($e167 (or $e16 $e60))
+(flet ($e168 (implies $e149 $e137))
+(flet ($e169 (not $e109))
+(flet ($e170 (and $e61 $e145))
+(flet ($e171 (and $e121 $e68))
+(flet ($e172 (and $e120 $e124))
+(flet ($e173 (and $e165 $e90))
+(flet ($e174 (implies $e168 $e166))
+(flet ($e175 (or $e174 $e173))
+(flet ($e176 (xor $e114 $e105))
+(flet ($e177 (xor $e97 $e66))
+(flet ($e178 (xor $e128 $e122))
+(flet ($e179 (xor $e167 $e176))
+(flet ($e180 (iff $e177 $e108))
+(flet ($e181 (not $e159))
+(flet ($e182 (iff $e178 $e138))
+(flet ($e183 (or $e98 $e169))
+(flet ($e184 (iff $e87 $e83))
+(flet ($e185 (not $e12))
+(flet ($e186 (and $e78 $e151))
+(flet ($e187 (not $e69))
+(flet ($e188 (xor $e94 $e88))
+(flet ($e189 (and $e81 $e141))
+(flet ($e190 (or $e96 $e184))
+(flet ($e191 (iff $e116 $e103))
+(flet ($e192 (or $e147 $e136))
+(flet ($e193 (if_then_else $e179 $e89 $e139))
+(flet ($e194 (implies $e193 $e134))
+(flet ($e195 (iff $e191 $e10))
+(flet ($e196 (iff $e152 $e190))
+(flet ($e197 (iff $e163 $e161))
+(flet ($e198 (iff $e170 $e129))
+(flet ($e199 (or $e195 $e67))
+(flet ($e200 (not $e164))
+(flet ($e201 (and $e104 $e192))
+(flet ($e202 (iff $e65 $e150))
+(flet ($e203 (xor $e200 $e70))
+(flet ($e204 (and $e183 $e79))
+(flet ($e205 (or $e185 $e172))
+(flet ($e206 (not $e18))
+(flet ($e207 (implies $e181 $e198))
+(flet ($e208 (not $e189))
+(flet ($e209 (xor $e171 $e203))
+(flet ($e210 (not $e201))
+(flet ($e211 (implies $e196 $e206))
+(flet ($e212 (iff $e211 $e182))
+(flet ($e213 (implies $e155 $e132))
+(flet ($e214 (if_then_else $e199 $e205 $e148))
+(flet ($e215 (xor $e154 $e86))
+(flet ($e216 (not $e119))
+(flet ($e217 (implies $e20 $e133))
+(flet ($e218 (if_then_else $e215 $e180 $e15))
+(flet ($e219 (implies $e197 $e112))
+(flet ($e220 (implies $e156 $e115))
+(flet ($e221 (and $e204 $e212))
+(flet ($e222 (if_then_else $e220 $e214 $e209))
+(flet ($e223 (implies $e218 $e213))
+(flet ($e224 (if_then_else $e93 $e221 $e130))
+(flet ($e225 (and $e223 $e222))
+(flet ($e226 (xor $e202 $e17))
+(flet ($e227 (not $e225))
+(flet ($e228 (if_then_else $e208 $e210 $e207))
+(flet ($e229 (or $e135 $e131))
+(flet ($e230 (not $e157))
+(flet ($e231 (and $e216 $e216))
+(flet ($e232 (or $e229 $e82))
+(flet ($e233 (implies $e187 $e160))
+(flet ($e234 (implies $e76 $e219))
+(flet ($e235 (not $e186))
+(flet ($e236 (xor $e230 $e188))
+(flet ($e237 (xor $e146 $e227))
+(flet ($e238 (implies $e235 $e235))
+(flet ($e239 (or $e92 $e232))
+(flet ($e240 (implies $e236 $e228))
+(flet ($e241 (not $e217))
+(flet ($e242 (or $e237 $e238))
+(flet ($e243 (implies $e233 $e241))
+(flet ($e244 (iff $e175 $e224))
+(flet ($e245 (if_then_else $e239 $e242 $e244))
+(flet ($e246 (xor $e153 $e234))
+(flet ($e247 (if_then_else $e194 $e246 $e226))
+(flet ($e248 (implies $e247 $e247))
+(flet ($e249 (or $e240 $e245))
+(flet ($e250 (xor $e248 $e111))
+(flet ($e251 (implies $e249 $e249))
+(flet ($e252 (iff $e243 $e243))
+(flet ($e253 (xor $e251 $e251))
+(flet ($e254 (iff $e253 $e253))
+(flet ($e255 (if_then_else $e250 $e254 $e254))
+(flet ($e256 (iff $e255 $e252))
+(flet ($e257 (xor $e231 $e256))
+$e257
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect7.smt b/test/regress/regress0/arrays/incorrect7.smt
new file mode 100644
index 000000000..4b406f964
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect7.smt
@@ -0,0 +1,80 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Array))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Element))
+:extrafuns ((v4 Element))
+:formula
+(flet ($e5 (distinct v0 v0))
+(flet ($e6 (distinct v0 v1))
+(flet ($e7 (distinct v2 v2))
+(flet ($e8 (distinct v3 v4))
+(let (?e9 (ite $e5 v1 v1))
+(let (?e10 (ite $e7 ?e9 v0))
+(let (?e11 (ite $e6 ?e10 v0))
+(let (?e12 (ite $e8 v1 v0))
+(let (?e13 (ite $e8 v2 v2))
+(let (?e14 (ite $e7 ?e13 ?e13))
+(let (?e15 (ite $e5 ?e13 ?e14))
+(let (?e16 (ite $e7 v2 ?e13))
+(let (?e17 (ite $e6 v2 ?e13))
+(let (?e18 (ite $e7 v3 v4))
+(let (?e19 (ite $e8 ?e18 v3))
+(let (?e20 (ite $e6 v3 v4))
+(let (?e21 (ite $e8 ?e19 v4))
+(let (?e22 (ite $e6 ?e20 ?e18))
+(let (?e23 (ite $e5 ?e22 ?e21))
+(let (?e24 (store ?e9 ?e17 ?e23))
+(let (?e25 (select ?e11 ?e15))
+(flet ($e26 (= ?e11 ?e12))
+(flet ($e27 (= ?e11 ?e11))
+(flet ($e28 (= ?e12 ?e11))
+(flet ($e29 (= v0 ?e9))
+(flet ($e30 (= ?e9 v1))
+(flet ($e31 (distinct ?e10 v1))
+(flet ($e32 (= ?e12 ?e24))
+(flet ($e33 (distinct ?e17 ?e14))
+(flet ($e34 (distinct v2 ?e17))
+(flet ($e35 (= ?e13 v2))
+(flet ($e36 (distinct ?e15 ?e16))
+(flet ($e37 (= v4 ?e22))
+(flet ($e38 (distinct v4 ?e18))
+(flet ($e39 (= ?e22 ?e23))
+(flet ($e40 (= ?e23 ?e20))
+(flet ($e41 (distinct ?e21 ?e22))
+(flet ($e42 (= ?e21 ?e23))
+(flet ($e43 (distinct ?e23 v4))
+(flet ($e44 (distinct v4 v3))
+(flet ($e45 (= ?e21 ?e19))
+(flet ($e46 (= ?e22 ?e22))
+(flet ($e47 (distinct ?e20 ?e25))
+(flet ($e48 (not $e7))
+(flet ($e49 (not $e33))
+(flet ($e50 (iff $e35 $e39))
+(flet ($e51 (xor $e28 $e42))
+(flet ($e52 (xor $e31 $e38))
+(flet ($e53 (implies $e46 $e36))
+(flet ($e54 (or $e50 $e37))
+(flet ($e55 (or $e52 $e5))
+(flet ($e56 (and $e34 $e55))
+(flet ($e57 (iff $e47 $e8))
+(flet ($e58 (implies $e48 $e44))
+(flet ($e59 (iff $e45 $e57))
+(flet ($e60 (iff $e41 $e29))
+(flet ($e61 (if_then_else $e58 $e40 $e27))
+(flet ($e62 (iff $e53 $e59))
+(flet ($e63 (if_then_else $e32 $e26 $e54))
+(flet ($e64 (xor $e51 $e60))
+(flet ($e65 (iff $e62 $e6))
+(flet ($e66 (implies $e64 $e49))
+(flet ($e67 (or $e63 $e65))
+(flet ($e68 (if_then_else $e30 $e66 $e61))
+(flet ($e69 (or $e56 $e68))
+(flet ($e70 (and $e69 $e43))
+(flet ($e71 (iff $e67 $e67))
+(flet ($e72 (and $e70 $e71))
+$e72
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect8.smt b/test/regress/regress0/arrays/incorrect8.smt
new file mode 100644
index 000000000..a118fec1d
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect8.smt
@@ -0,0 +1,491 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Array))
+:extrafuns ((v2 Array))
+:extrafuns ((v3 Index))
+:extrafuns ((v4 Index))
+:extrafuns ((v5 Element))
+:formula
+(let (?e6 (store v1 v4 v5))
+(let (?e7 (store ?e6 v4 v5))
+(let (?e8 (select v0 v3))
+(let (?e9 (select ?e6 v3))
+(let (?e10 (select v0 v3))
+(let (?e11 (store ?e7 v3 ?e8))
+(let (?e12 (select ?e7 v3))
+(let (?e13 (store ?e7 v3 ?e8))
+(let (?e14 (select v1 v3))
+(flet ($e15 (distinct ?e13 ?e13))
+(flet ($e16 (distinct v2 ?e6))
+(flet ($e17 (distinct v1 v2))
+(flet ($e18 (= v2 ?e7))
+(flet ($e19 (= v0 v0))
+(flet ($e20 (distinct ?e13 v2))
+(flet ($e21 (= ?e6 ?e6))
+(flet ($e22 (distinct ?e11 ?e13))
+(flet ($e23 (= v3 v3))
+(flet ($e24 (= v3 v3))
+(flet ($e25 (distinct v3 v3))
+(flet ($e26 (distinct v4 v3))
+(flet ($e27 (distinct ?e9 ?e14))
+(flet ($e28 (= ?e9 v5))
+(flet ($e29 (= ?e12 v5))
+(flet ($e30 (distinct ?e10 ?e10))
+(flet ($e31 (= ?e12 ?e9))
+(flet ($e32 (= ?e10 ?e10))
+(flet ($e33 (= ?e12 v5))
+(flet ($e34 (= ?e8 ?e8))
+(let (?e35 (ite $e24 ?e6 ?e11))
+(let (?e36 (ite $e17 ?e35 ?e6))
+(let (?e37 (ite $e23 v2 v2))
+(let (?e38 (ite $e31 ?e35 ?e36))
+(let (?e39 (ite $e16 ?e36 ?e38))
+(let (?e40 (ite $e15 v2 v2))
+(let (?e41 (ite $e28 ?e7 ?e36))
+(let (?e42 (ite $e22 ?e7 ?e13))
+(let (?e43 (ite $e34 ?e38 v1))
+(let (?e44 (ite $e33 v0 v1))
+(let (?e45 (ite $e21 ?e44 v1))
+(let (?e46 (ite $e18 ?e35 ?e11))
+(let (?e47 (ite $e19 ?e44 ?e43))
+(let (?e48 (ite $e27 ?e37 v1))
+(let (?e49 (ite $e17 v2 ?e48))
+(let (?e50 (ite $e28 ?e37 v2))
+(let (?e51 (ite $e29 ?e42 ?e41))
+(let (?e52 (ite $e23 ?e49 v2))
+(let (?e53 (ite $e16 ?e47 ?e35))
+(let (?e54 (ite $e25 ?e45 ?e41))
+(let (?e55 (ite $e23 ?e41 ?e45))
+(let (?e56 (ite $e32 ?e6 ?e51))
+(let (?e57 (ite $e34 ?e39 v2))
+(let (?e58 (ite $e27 ?e49 ?e13))
+(let (?e59 (ite $e26 ?e55 ?e53))
+(let (?e60 (ite $e22 ?e37 ?e36))
+(let (?e61 (ite $e26 ?e50 ?e46))
+(let (?e62 (ite $e29 ?e47 ?e61))
+(let (?e63 (ite $e16 ?e59 ?e53))
+(let (?e64 (ite $e20 ?e55 ?e56))
+(let (?e65 (ite $e30 ?e42 ?e52))
+(let (?e66 (ite $e21 v3 v3))
+(let (?e67 (ite $e26 v3 v3))
+(let (?e68 (ite $e28 v4 v4))
+(let (?e69 (ite $e33 ?e67 ?e66))
+(let (?e70 (ite $e18 v4 ?e69))
+(let (?e71 (ite $e17 v3 ?e67))
+(let (?e72 (ite $e23 v3 ?e71))
+(let (?e73 (ite $e27 ?e68 ?e67))
+(let (?e74 (ite $e29 v4 ?e73))
+(let (?e75 (ite $e24 ?e70 ?e72))
+(let (?e76 (ite $e32 ?e73 ?e75))
+(let (?e77 (ite $e17 ?e75 v4))
+(let (?e78 (ite $e25 ?e68 ?e72))
+(let (?e79 (ite $e30 v4 ?e77))
+(let (?e80 (ite $e19 v3 ?e70))
+(let (?e81 (ite $e15 ?e66 v3))
+(let (?e82 (ite $e16 ?e72 ?e76))
+(let (?e83 (ite $e21 ?e70 ?e75))
+(let (?e84 (ite $e23 ?e70 ?e66))
+(let (?e85 (ite $e31 ?e81 ?e74))
+(let (?e86 (ite $e22 ?e69 ?e84))
+(let (?e87 (ite $e34 ?e73 v3))
+(let (?e88 (ite $e20 ?e79 ?e67))
+(let (?e89 (ite $e28 ?e12 ?e9))
+(let (?e90 (ite $e17 ?e10 v5))
+(let (?e91 (ite $e21 ?e8 ?e14))
+(let (?e92 (ite $e23 ?e10 v5))
+(let (?e93 (ite $e24 ?e90 ?e9))
+(let (?e94 (ite $e16 ?e90 ?e10))
+(let (?e95 (ite $e32 ?e8 ?e14))
+(let (?e96 (ite $e18 ?e94 ?e92))
+(let (?e97 (ite $e34 ?e8 ?e14))
+(let (?e98 (ite $e25 ?e90 ?e91))
+(let (?e99 (ite $e15 v5 ?e10))
+(let (?e100 (ite $e31 ?e98 ?e94))
+(let (?e101 (ite $e21 ?e90 ?e14))
+(let (?e102 (ite $e20 ?e95 ?e10))
+(let (?e103 (ite $e22 ?e10 ?e92))
+(let (?e104 (ite $e17 ?e97 ?e94))
+(let (?e105 (ite $e27 ?e102 ?e97))
+(let (?e106 (ite $e29 ?e14 ?e8))
+(let (?e107 (ite $e33 ?e105 ?e95))
+(let (?e108 (ite $e19 ?e100 ?e100))
+(let (?e109 (ite $e19 ?e93 v5))
+(let (?e110 (ite $e30 ?e90 ?e95))
+(let (?e111 (ite $e26 ?e93 ?e108))
+(let (?e112 (store v2 ?e67 ?e100))
+(let (?e113 (store ?e57 ?e80 ?e92))
+(let (?e114 (store ?e52 ?e75 ?e97))
+(let (?e115 (select ?e54 ?e87))
+(let (?e116 (select ?e51 v3))
+(let (?e117 (select ?e13 ?e71))
+(let (?e118 (store ?e112 ?e85 ?e93))
+(let (?e119 (select ?e62 ?e75))
+(let (?e120 (store ?e45 ?e81 ?e91))
+(let (?e121 (select ?e56 ?e76))
+(flet ($e122 (= ?e58 ?e56))
+(flet ($e123 (distinct ?e60 ?e49))
+(flet ($e124 (= ?e62 ?e46))
+(flet ($e125 (= ?e54 ?e113))
+(flet ($e126 (= ?e61 ?e47))
+(flet ($e127 (distinct ?e36 ?e113))
+(flet ($e128 (= ?e40 ?e38))
+(flet ($e129 (= ?e62 ?e112))
+(flet ($e130 (distinct ?e56 ?e65))
+(flet ($e131 (distinct ?e35 ?e114))
+(flet ($e132 (= ?e35 ?e63))
+(flet ($e133 (distinct ?e53 ?e114))
+(flet ($e134 (distinct ?e36 ?e6))
+(flet ($e135 (= ?e51 ?e53))
+(flet ($e136 (= ?e118 ?e61))
+(flet ($e137 (= ?e120 ?e37))
+(flet ($e138 (= ?e35 ?e63))
+(flet ($e139 (= ?e13 ?e57))
+(flet ($e140 (= ?e46 ?e65))
+(flet ($e141 (= ?e120 ?e13))
+(flet ($e142 (= ?e45 ?e51))
+(flet ($e143 (distinct v0 ?e64))
+(flet ($e144 (distinct ?e41 ?e56))
+(flet ($e145 (distinct ?e46 ?e38))
+(flet ($e146 (= v0 ?e38))
+(flet ($e147 (= ?e47 v0))
+(flet ($e148 (distinct ?e47 ?e7))
+(flet ($e149 (distinct ?e56 ?e58))
+(flet ($e150 (= ?e58 ?e52))
+(flet ($e151 (distinct ?e11 ?e55))
+(flet ($e152 (distinct ?e60 ?e57))
+(flet ($e153 (= ?e44 ?e120))
+(flet ($e154 (distinct ?e48 ?e40))
+(flet ($e155 (= ?e46 ?e53))
+(flet ($e156 (distinct ?e44 ?e49))
+(flet ($e157 (distinct v0 ?e13))
+(flet ($e158 (distinct ?e51 ?e56))
+(flet ($e159 (distinct ?e62 ?e13))
+(flet ($e160 (= ?e61 ?e47))
+(flet ($e161 (distinct v2 ?e47))
+(flet ($e162 (distinct ?e52 ?e35))
+(flet ($e163 (= ?e43 ?e48))
+(flet ($e164 (= ?e47 ?e113))
+(flet ($e165 (= ?e112 ?e6))
+(flet ($e166 (distinct ?e52 ?e47))
+(flet ($e167 (distinct ?e41 ?e51))
+(flet ($e168 (= ?e45 ?e55))
+(flet ($e169 (distinct ?e48 ?e58))
+(flet ($e170 (= ?e58 ?e112))
+(flet ($e171 (= ?e58 ?e57))
+(flet ($e172 (= ?e11 ?e39))
+(flet ($e173 (distinct ?e114 ?e54))
+(flet ($e174 (= ?e58 ?e52))
+(flet ($e175 (distinct ?e58 ?e65))
+(flet ($e176 (= v0 ?e11))
+(flet ($e177 (distinct ?e118 ?e38))
+(flet ($e178 (distinct v1 ?e48))
+(flet ($e179 (distinct ?e53 ?e59))
+(flet ($e180 (= ?e11 ?e49))
+(flet ($e181 (= ?e120 ?e42))
+(flet ($e182 (= ?e61 ?e45))
+(flet ($e183 (= ?e42 ?e65))
+(flet ($e184 (= ?e58 ?e57))
+(flet ($e185 (distinct ?e46 ?e51))
+(flet ($e186 (= ?e42 ?e113))
+(flet ($e187 (distinct ?e37 ?e64))
+(flet ($e188 (distinct ?e63 ?e37))
+(flet ($e189 (distinct ?e43 v1))
+(flet ($e190 (distinct ?e62 ?e51))
+(flet ($e191 (= ?e50 ?e6))
+(flet ($e192 (distinct ?e73 ?e83))
+(flet ($e193 (distinct ?e83 ?e76))
+(flet ($e194 (distinct ?e81 ?e87))
+(flet ($e195 (= ?e76 ?e78))
+(flet ($e196 (distinct ?e81 ?e84))
+(flet ($e197 (distinct v4 ?e83))
+(flet ($e198 (= ?e73 ?e68))
+(flet ($e199 (= ?e81 ?e76))
+(flet ($e200 (distinct ?e77 ?e70))
+(flet ($e201 (distinct ?e88 ?e84))
+(flet ($e202 (= ?e79 ?e82))
+(flet ($e203 (= ?e69 ?e81))
+(flet ($e204 (= ?e74 ?e78))
+(flet ($e205 (= ?e87 ?e77))
+(flet ($e206 (distinct ?e80 ?e88))
+(flet ($e207 (distinct v4 ?e73))
+(flet ($e208 (distinct ?e84 ?e67))
+(flet ($e209 (= ?e76 ?e87))
+(flet ($e210 (distinct ?e84 ?e67))
+(flet ($e211 (distinct ?e88 ?e77))
+(flet ($e212 (distinct ?e79 ?e88))
+(flet ($e213 (= ?e78 v3))
+(flet ($e214 (distinct ?e84 ?e70))
+(flet ($e215 (= ?e86 ?e85))
+(flet ($e216 (= ?e75 ?e71))
+(flet ($e217 (= ?e76 ?e87))
+(flet ($e218 (distinct ?e85 ?e73))
+(flet ($e219 (= ?e67 ?e71))
+(flet ($e220 (distinct ?e74 ?e80))
+(flet ($e221 (distinct ?e67 ?e82))
+(flet ($e222 (= ?e76 ?e78))
+(flet ($e223 (distinct ?e70 ?e77))
+(flet ($e224 (= ?e81 ?e67))
+(flet ($e225 (= ?e75 ?e78))
+(flet ($e226 (distinct ?e72 ?e67))
+(flet ($e227 (= ?e80 ?e73))
+(flet ($e228 (= ?e71 ?e69))
+(flet ($e229 (distinct ?e87 ?e83))
+(flet ($e230 (distinct v4 ?e86))
+(flet ($e231 (distinct ?e81 ?e67))
+(flet ($e232 (distinct ?e75 ?e84))
+(flet ($e233 (= ?e70 ?e85))
+(flet ($e234 (distinct ?e83 v4))
+(flet ($e235 (distinct ?e80 ?e88))
+(flet ($e236 (= ?e79 ?e68))
+(flet ($e237 (distinct ?e87 ?e66))
+(flet ($e238 (= ?e98 ?e9))
+(flet ($e239 (= ?e106 ?e119))
+(flet ($e240 (= ?e104 ?e115))
+(flet ($e241 (distinct ?e10 ?e99))
+(flet ($e242 (= ?e99 ?e111))
+(flet ($e243 (= ?e89 ?e92))
+(flet ($e244 (= ?e101 v5))
+(flet ($e245 (distinct ?e106 ?e10))
+(flet ($e246 (distinct ?e14 ?e91))
+(flet ($e247 (= ?e111 ?e93))
+(flet ($e248 (distinct ?e9 ?e95))
+(flet ($e249 (distinct ?e10 ?e12))
+(flet ($e250 (= ?e97 ?e115))
+(flet ($e251 (= v5 ?e9))
+(flet ($e252 (= ?e95 ?e117))
+(flet ($e253 (distinct ?e9 ?e94))
+(flet ($e254 (distinct ?e9 ?e93))
+(flet ($e255 (distinct ?e121 ?e9))
+(flet ($e256 (distinct ?e117 ?e89))
+(flet ($e257 (= ?e96 ?e90))
+(flet ($e258 (= ?e108 ?e121))
+(flet ($e259 (distinct ?e14 ?e98))
+(flet ($e260 (distinct ?e95 v5))
+(flet ($e261 (distinct ?e108 ?e105))
+(flet ($e262 (= ?e107 ?e90))
+(flet ($e263 (distinct ?e119 ?e109))
+(flet ($e264 (= ?e107 ?e14))
+(flet ($e265 (distinct ?e109 ?e108))
+(flet ($e266 (distinct ?e117 ?e100))
+(flet ($e267 (= ?e101 ?e102))
+(flet ($e268 (distinct ?e92 ?e12))
+(flet ($e269 (distinct ?e9 ?e109))
+(flet ($e270 (= ?e90 ?e101))
+(flet ($e271 (distinct ?e12 ?e111))
+(flet ($e272 (= ?e106 ?e104))
+(flet ($e273 (= ?e115 ?e93))
+(flet ($e274 (distinct ?e104 ?e108))
+(flet ($e275 (distinct ?e8 ?e100))
+(flet ($e276 (distinct ?e97 ?e10))
+(flet ($e277 (distinct ?e100 ?e111))
+(flet ($e278 (distinct ?e89 ?e104))
+(flet ($e279 (= ?e8 ?e105))
+(flet ($e280 (distinct ?e110 ?e121))
+(flet ($e281 (= ?e89 ?e100))
+(flet ($e282 (distinct ?e93 ?e117))
+(flet ($e283 (distinct ?e121 ?e116))
+(flet ($e284 (= ?e107 ?e104))
+(flet ($e285 (distinct ?e10 v5))
+(flet ($e286 (distinct ?e116 ?e9))
+(flet ($e287 (= ?e103 ?e98))
+(flet ($e288 (implies $e272 $e127))
+(flet ($e289 (implies $e275 $e25))
+(flet ($e290 (if_then_else $e204 $e223 $e241))
+(flet ($e291 (if_then_else $e226 $e209 $e280))
+(flet ($e292 (and $e243 $e218))
+(flet ($e293 (xor $e230 $e191))
+(flet ($e294 (and $e27 $e32))
+(flet ($e295 (iff $e15 $e163))
+(flet ($e296 (implies $e124 $e270))
+(flet ($e297 (xor $e150 $e200))
+(flet ($e298 (not $e221))
+(flet ($e299 (implies $e211 $e211))
+(flet ($e300 (and $e145 $e251))
+(flet ($e301 (implies $e278 $e22))
+(flet ($e302 (and $e215 $e153))
+(flet ($e303 (and $e300 $e228))
+(flet ($e304 (iff $e210 $e30))
+(flet ($e305 (if_then_else $e135 $e291 $e152))
+(flet ($e306 (not $e195))
+(flet ($e307 (not $e143))
+(flet ($e308 (or $e132 $e138))
+(flet ($e309 (or $e253 $e307))
+(flet ($e310 (iff $e229 $e294))
+(flet ($e311 (or $e182 $e173))
+(flet ($e312 (and $e233 $e188))
+(flet ($e313 (iff $e246 $e130))
+(flet ($e314 (xor $e212 $e126))
+(flet ($e315 (implies $e168 $e18))
+(flet ($e316 (or $e21 $e287))
+(flet ($e317 (or $e183 $e203))
+(flet ($e318 (or $e159 $e277))
+(flet ($e319 (if_then_else $e258 $e238 $e224))
+(flet ($e320 (implies $e262 $e312))
+(flet ($e321 (not $e271))
+(flet ($e322 (xor $e167 $e193))
+(flet ($e323 (xor $e304 $e290))
+(flet ($e324 (iff $e125 $e199))
+(flet ($e325 (and $e19 $e186))
+(flet ($e326 (implies $e279 $e321))
+(flet ($e327 (or $e139 $e263))
+(flet ($e328 (not $e137))
+(flet ($e329 (or $e136 $e319))
+(flet ($e330 (and $e318 $e234))
+(flet ($e331 (or $e24 $e299))
+(flet ($e332 (or $e33 $e254))
+(flet ($e333 (or $e295 $e206))
+(flet ($e334 (iff $e283 $e236))
+(flet ($e335 (and $e252 $e123))
+(flet ($e336 (or $e141 $e317))
+(flet ($e337 (and $e166 $e249))
+(flet ($e338 (implies $e198 $e160))
+(flet ($e339 (not $e242))
+(flet ($e340 (or $e324 $e217))
+(flet ($e341 (implies $e265 $e185))
+(flet ($e342 (or $e245 $e171))
+(flet ($e343 (implies $e337 $e296))
+(flet ($e344 (if_then_else $e292 $e161 $e220))
+(flet ($e345 (implies $e122 $e335))
+(flet ($e346 (if_then_else $e176 $e261 $e257))
+(flet ($e347 (xor $e187 $e256))
+(flet ($e348 (if_then_else $e344 $e284 $e327))
+(flet ($e349 (xor $e293 $e31))
+(flet ($e350 (xor $e336 $e142))
+(flet ($e351 (iff $e302 $e313))
+(flet ($e352 (if_then_else $e154 $e174 $e285))
+(flet ($e353 (iff $e316 $e208))
+(flet ($e354 (if_then_else $e309 $e133 $e158))
+(flet ($e355 (not $e348))
+(flet ($e356 (or $e140 $e255))
+(flet ($e357 (iff $e216 $e219))
+(flet ($e358 (if_then_else $e169 $e129 $e331))
+(flet ($e359 (and $e164 $e147))
+(flet ($e360 (if_then_else $e311 $e250 $e181))
+(flet ($e361 (not $e332))
+(flet ($e362 (not $e320))
+(flet ($e363 (iff $e205 $e175))
+(flet ($e364 (and $e247 $e194))
+(flet ($e365 (not $e148))
+(flet ($e366 (not $e346))
+(flet ($e367 (or $e269 $e297))
+(flet ($e368 (iff $e322 $e180))
+(flet ($e369 (if_then_else $e131 $e259 $e367))
+(flet ($e370 (iff $e298 $e239))
+(flet ($e371 (iff $e352 $e306))
+(flet ($e372 (not $e202))
+(flet ($e373 (implies $e315 $e264))
+(flet ($e374 (or $e357 $e192))
+(flet ($e375 (iff $e214 $e281))
+(flet ($e376 (and $e26 $e156))
+(flet ($e377 (xor $e308 $e17))
+(flet ($e378 (or $e268 $e162))
+(flet ($e379 (if_then_else $e353 $e333 $e177))
+(flet ($e380 (not $e377))
+(flet ($e381 (xor $e235 $e235))
+(flet ($e382 (not $e338))
+(flet ($e383 (and $e360 $e144))
+(flet ($e384 (if_then_else $e345 $e149 $e170))
+(flet ($e385 (or $e362 $e323))
+(flet ($e386 (not $e369))
+(flet ($e387 (iff $e289 $e273))
+(flet ($e388 (xor $e222 $e213))
+(flet ($e389 (iff $e178 $e356))
+(flet ($e390 (xor $e165 $e248))
+(flet ($e391 (if_then_else $e379 $e34 $e288))
+(flet ($e392 (iff $e301 $e155))
+(flet ($e393 (implies $e370 $e260))
+(flet ($e394 (implies $e392 $e373))
+(flet ($e395 (xor $e378 $e310))
+(flet ($e396 (or $e359 $e276))
+(flet ($e397 (iff $e387 $e244))
+(flet ($e398 (if_then_else $e266 $e267 $e394))
+(flet ($e399 (implies $e366 $e365))
+(flet ($e400 (implies $e397 $e350))
+(flet ($e401 (and $e314 $e343))
+(flet ($e402 (not $e134))
+(flet ($e403 (and $e382 $e157))
+(flet ($e404 (if_then_else $e363 $e151 $e190))
+(flet ($e405 (implies $e381 $e231))
+(flet ($e406 (xor $e179 $e20))
+(flet ($e407 (xor $e325 $e282))
+(flet ($e408 (and $e396 $e384))
+(flet ($e409 (not $e407))
+(flet ($e410 (not $e375))
+(flet ($e411 (not $e358))
+(flet ($e412 (and $e16 $e286))
+(flet ($e413 (implies $e364 $e172))
+(flet ($e414 (iff $e406 $e404))
+(flet ($e415 (or $e342 $e334))
+(flet ($e416 (if_then_else $e349 $e400 $e413))
+(flet ($e417 (xor $e398 $e414))
+(flet ($e418 (not $e399))
+(flet ($e419 (and $e380 $e374))
+(flet ($e420 (xor $e128 $e393))
+(flet ($e421 (not $e385))
+(flet ($e422 (implies $e326 $e303))
+(flet ($e423 (if_then_else $e405 $e412 $e412))
+(flet ($e424 (implies $e395 $e423))
+(flet ($e425 (if_then_else $e386 $e355 $e227))
+(flet ($e426 (xor $e383 $e237))
+(flet ($e427 (xor $e146 $e402))
+(flet ($e428 (or $e420 $e418))
+(flet ($e429 (if_then_else $e376 $e354 $e371))
+(flet ($e430 (or $e409 $e424))
+(flet ($e431 (if_then_else $e361 $e429 $e225))
+(flet ($e432 (or $e330 $e329))
+(flet ($e433 (not $e232))
+(flet ($e434 (if_then_else $e340 $e184 $e432))
+(flet ($e435 (or $e197 $e389))
+(flet ($e436 (not $e426))
+(flet ($e437 (if_then_else $e207 $e347 $e339))
+(flet ($e438 (if_then_else $e427 $e391 $e411))
+(flet ($e439 (xor $e430 $e410))
+(flet ($e440 (or $e390 $e437))
+(flet ($e441 (implies $e368 $e240))
+(flet ($e442 (and $e441 $e408))
+(flet ($e443 (xor $e201 $e434))
+(flet ($e444 (if_then_else $e305 $e23 $e328))
+(flet ($e445 (xor $e415 $e419))
+(flet ($e446 (implies $e444 $e417))
+(flet ($e447 (if_then_else $e351 $e416 $e29))
+(flet ($e448 (implies $e431 $e446))
+(flet ($e449 (if_then_else $e439 $e388 $e440))
+(flet ($e450 (and $e403 $e442))
+(flet ($e451 (implies $e448 $e448))
+(flet ($e452 (not $e189))
+(flet ($e453 (and $e451 $e449))
+(flet ($e454 (or $e425 $e28))
+(flet ($e455 (if_then_else $e372 $e454 $e447))
+(flet ($e456 (not $e428))
+(flet ($e457 (or $e341 $e421))
+(flet ($e458 (or $e452 $e433))
+(flet ($e459 (iff $e455 $e453))
+(flet ($e460 (or $e445 $e459))
+(flet ($e461 (and $e457 $e450))
+(flet ($e462 (or $e438 $e456))
+(flet ($e463 (not $e461))
+(flet ($e464 (xor $e443 $e274))
+(flet ($e465 (xor $e460 $e462))
+(flet ($e466 (xor $e401 $e401))
+(flet ($e467 (not $e436))
+(flet ($e468 (or $e464 $e464))
+(flet ($e469 (iff $e196 $e196))
+(flet ($e470 (not $e467))
+(flet ($e471 (not $e470))
+(flet ($e472 (or $e466 $e465))
+(flet ($e473 (implies $e435 $e472))
+(flet ($e474 (not $e463))
+(flet ($e475 (not $e458))
+(flet ($e476 (iff $e422 $e475))
+(flet ($e477 (and $e473 $e468))
+(flet ($e478 (iff $e471 $e474))
+(flet ($e479 (or $e476 $e469))
+(flet ($e480 (iff $e479 $e479))
+(flet ($e481 (not $e477))
+(flet ($e482 (or $e481 $e480))
+(flet ($e483 (xor $e478 $e482))
+$e483
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/incorrect9.smt b/test/regress/regress0/arrays/incorrect9.smt
new file mode 100644
index 000000000..36bf7a22c
--- /dev/null
+++ b/test/regress/regress0/arrays/incorrect9.smt
@@ -0,0 +1,189 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status unsat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Index))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Element))
+:extrafuns ((v4 Element))
+:extrafuns ((v5 Element))
+:extrafuns ((v6 Element))
+:extrafuns ((v7 Element))
+:formula
+(let (?e8 (store v0 v2 v7))
+(let (?e9 (select ?e8 v1))
+(flet ($e10 (= v0 ?e8))
+(flet ($e11 (distinct v2 v1))
+(flet ($e12 (distinct v6 ?e9))
+(flet ($e13 (distinct v4 v3))
+(flet ($e14 (= v6 v4))
+(flet ($e15 (distinct v4 v4))
+(flet ($e16 (= v6 v7))
+(flet ($e17 (= v5 v6))
+(let (?e18 (ite $e10 v0 ?e8))
+(let (?e19 (ite $e13 v0 v0))
+(let (?e20 (ite $e13 v0 v0))
+(let (?e21 (ite $e11 ?e19 v0))
+(let (?e22 (ite $e14 ?e18 ?e20))
+(let (?e23 (ite $e10 v0 ?e21))
+(let (?e24 (ite $e13 ?e21 ?e21))
+(let (?e25 (ite $e13 ?e22 ?e21))
+(let (?e26 (ite $e15 ?e23 ?e18))
+(let (?e27 (ite $e12 ?e23 ?e26))
+(let (?e28 (ite $e16 ?e26 ?e23))
+(let (?e29 (ite $e17 ?e27 ?e26))
+(let (?e30 (ite $e10 v1 v1))
+(let (?e31 (ite $e12 v2 v1))
+(let (?e32 (ite $e17 v2 v1))
+(let (?e33 (ite $e15 v1 v2))
+(let (?e34 (ite $e14 ?e30 ?e32))
+(let (?e35 (ite $e11 ?e33 ?e34))
+(let (?e36 (ite $e16 ?e32 ?e31))
+(let (?e37 (ite $e11 ?e35 v1))
+(let (?e38 (ite $e13 v1 ?e37))
+(let (?e39 (ite $e15 v4 v6))
+(let (?e40 (ite $e13 v5 v6))
+(let (?e41 (ite $e16 ?e9 v3))
+(let (?e42 (ite $e12 ?e40 v3))
+(let (?e43 (ite $e11 v5 v7))
+(let (?e44 (ite $e10 ?e40 ?e43))
+(let (?e45 (ite $e14 v4 ?e44))
+(let (?e46 (ite $e17 ?e39 v4))
+(let (?e47 (store ?e8 ?e38 v7))
+(let (?e48 (select ?e18 ?e33))
+(flet ($e49 (= ?e18 ?e18))
+(flet ($e50 (distinct ?e23 ?e26))
+(flet ($e51 (distinct ?e28 ?e19))
+(flet ($e52 (distinct ?e47 ?e18))
+(flet ($e53 (= ?e27 ?e18))
+(flet ($e54 (distinct ?e19 ?e26))
+(flet ($e55 (distinct ?e47 v0))
+(flet ($e56 (distinct ?e19 ?e24))
+(flet ($e57 (= ?e8 ?e26))
+(flet ($e58 (distinct ?e18 ?e8))
+(flet ($e59 (distinct ?e26 ?e29))
+(flet ($e60 (= ?e19 ?e25))
+(flet ($e61 (distinct ?e29 ?e22))
+(flet ($e62 (distinct ?e22 v0))
+(flet ($e63 (distinct ?e29 ?e18))
+(flet ($e64 (distinct v0 ?e26))
+(flet ($e65 (= ?e24 ?e47))
+(flet ($e66 (distinct ?e29 ?e23))
+(flet ($e67 (distinct ?e27 ?e27))
+(flet ($e68 (distinct ?e27 ?e24))
+(flet ($e69 (= ?e29 ?e23))
+(flet ($e70 (distinct ?e8 ?e20))
+(flet ($e71 (= ?e25 ?e8))
+(flet ($e72 (= ?e18 ?e47))
+(flet ($e73 (distinct ?e22 ?e24))
+(flet ($e74 (distinct ?e21 ?e24))
+(flet ($e75 (distinct ?e38 v2))
+(flet ($e76 (distinct ?e30 ?e34))
+(flet ($e77 (distinct ?e34 ?e34))
+(flet ($e78 (distinct ?e35 ?e33))
+(flet ($e79 (distinct ?e33 ?e36))
+(flet ($e80 (distinct ?e38 ?e30))
+(flet ($e81 (= ?e35 ?e35))
+(flet ($e82 (distinct v2 ?e33))
+(flet ($e83 (= ?e34 ?e34))
+(flet ($e84 (distinct ?e37 ?e33))
+(flet ($e85 (distinct ?e30 ?e35))
+(flet ($e86 (distinct ?e37 v2))
+(flet ($e87 (distinct ?e31 v1))
+(flet ($e88 (distinct ?e32 ?e30))
+(flet ($e89 (distinct ?e40 v5))
+(flet ($e90 (distinct ?e44 v4))
+(flet ($e91 (distinct ?e9 ?e46))
+(flet ($e92 (= ?e40 ?e46))
+(flet ($e93 (= ?e46 v3))
+(flet ($e94 (distinct ?e43 v6))
+(flet ($e95 (distinct v6 v4))
+(flet ($e96 (= v4 ?e43))
+(flet ($e97 (= ?e44 ?e9))
+(flet ($e98 (distinct ?e42 ?e41))
+(flet ($e99 (distinct v4 ?e48))
+(flet ($e100 (distinct v4 ?e9))
+(flet ($e101 (distinct ?e44 v7))
+(flet ($e102 (distinct v3 ?e45))
+(flet ($e103 (= v7 ?e46))
+(flet ($e104 (distinct ?e40 v6))
+(flet ($e105 (= v4 ?e41))
+(flet ($e106 (distinct ?e45 ?e40))
+(flet ($e107 (distinct v7 v4))
+(flet ($e108 (= v6 v3))
+(flet ($e109 (distinct ?e39 v3))
+(flet ($e110 (or $e81 $e90))
+(flet ($e111 (xor $e92 $e10))
+(flet ($e112 (iff $e11 $e57))
+(flet ($e113 (iff $e50 $e49))
+(flet ($e114 (not $e91))
+(flet ($e115 (if_then_else $e69 $e51 $e64))
+(flet ($e116 (if_then_else $e98 $e97 $e82))
+(flet ($e117 (xor $e67 $e71))
+(flet ($e118 (if_then_else $e61 $e88 $e55))
+(flet ($e119 (implies $e59 $e99))
+(flet ($e120 (or $e13 $e117))
+(flet ($e121 (iff $e73 $e112))
+(flet ($e122 (and $e94 $e68))
+(flet ($e123 (not $e60))
+(flet ($e124 (and $e100 $e15))
+(flet ($e125 (or $e70 $e111))
+(flet ($e126 (or $e75 $e119))
+(flet ($e127 (xor $e121 $e17))
+(flet ($e128 (iff $e127 $e76))
+(flet ($e129 (if_then_else $e72 $e16 $e115))
+(flet ($e130 (not $e65))
+(flet ($e131 (xor $e85 $e93))
+(flet ($e132 (and $e103 $e89))
+(flet ($e133 (if_then_else $e128 $e14 $e79))
+(flet ($e134 (implies $e114 $e12))
+(flet ($e135 (not $e133))
+(flet ($e136 (iff $e129 $e105))
+(flet ($e137 (xor $e87 $e135))
+(flet ($e138 (and $e137 $e118))
+(flet ($e139 (implies $e131 $e74))
+(flet ($e140 (iff $e126 $e116))
+(flet ($e141 (or $e120 $e120))
+(flet ($e142 (if_then_else $e101 $e113 $e134))
+(flet ($e143 (and $e52 $e140))
+(flet ($e144 (iff $e139 $e122))
+(flet ($e145 (or $e136 $e104))
+(flet ($e146 (not $e54))
+(flet ($e147 (if_then_else $e96 $e95 $e109))
+(flet ($e148 (iff $e123 $e78))
+(flet ($e149 (and $e146 $e146))
+(flet ($e150 (implies $e108 $e107))
+(flet ($e151 (xor $e62 $e147))
+(flet ($e152 (not $e77))
+(flet ($e153 (if_then_else $e150 $e145 $e102))
+(flet ($e154 (iff $e142 $e130))
+(flet ($e155 (and $e86 $e138))
+(flet ($e156 (and $e149 $e155))
+(flet ($e157 (implies $e80 $e66))
+(flet ($e158 (implies $e156 $e143))
+(flet ($e159 (iff $e154 $e157))
+(flet ($e160 (not $e56))
+(flet ($e161 (xor $e63 $e141))
+(flet ($e162 (or $e125 $e151))
+(flet ($e163 (iff $e58 $e83))
+(flet ($e164 (or $e110 $e132))
+(flet ($e165 (or $e163 $e153))
+(flet ($e166 (and $e53 $e159))
+(flet ($e167 (and $e152 $e165))
+(flet ($e168 (not $e160))
+(flet ($e169 (iff $e164 $e166))
+(flet ($e170 (not $e106))
+(flet ($e171 (and $e124 $e169))
+(flet ($e172 (if_then_else $e167 $e144 $e167))
+(flet ($e173 (iff $e162 $e170))
+(flet ($e174 (and $e172 $e171))
+(flet ($e175 (iff $e161 $e168))
+(flet ($e176 (and $e173 $e175))
+(flet ($e177 (implies $e174 $e176))
+(flet ($e178 (iff $e148 $e158))
+(flet ($e179 (iff $e177 $e84))
+(flet ($e180 (iff $e178 $e178))
+(flet ($e181 (implies $e180 $e179))
+$e181
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
author	Morgan Deters <mdeters@gmail.com>	2011-07-11 16:38:38 +0000
committer	Morgan Deters <mdeters@gmail.com>	2011-07-11 16:38:38 +0000
commit	2ae8fae8c1e1de22c2324e5c63c5d7fd73a4582e (patch)
tree	a2aeb46410f1b9c9e06226864e700639a6d25f45
parent	e72fdcf6333d575e9c737a6274aa627dc9c54b47 (diff)