Fix for fuzzer-found model bug

(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)

2 files changed, 350 insertions, 0 deletions

diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index cc4a1556f..8ed9096c4 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -20,6 +20,7 @@ TESTS =	\
 	fuzz03.smt \
 	fuzz04.smt \
 	fuzz05.smt \
+	fuzz06.smt \
 	a17.smt \
 	error72.delta2.smt \
 	x2.smt
diff --git a/test/regress/regress0/auflia/fuzz06.smt b/test/regress/regress0/auflia/fuzz06.smt
new file mode 100644
index 000000000..88c2a9d5c
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz06.smt
@@ -0,0 +1,349 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:status sat
+:extrafuns ((f0 Int Int))
+:extrafuns ((f1 Array Array Array))
+:extrapreds ((p0 Int))
+:extrapreds ((p1 Array Array Array))
+:extrafuns ((v0 Int))
+:extrafuns ((v1 Array))
+:formula
+(let (?e2 0)
+(let (?e3 (ite (p0 v0) 1 0))
+(let (?e4 (ite (p0 v0) 1 0))
+(let (?e5 (~ ?e4))
+(let (?e6 (ite (p0 ?e3) 1 0))
+(let (?e7 (f0 ?e3))
+(let (?e8 (* ?e4 (~ ?e2)))
+(let (?e9 (store v1 ?e5 ?e8))
+(let (?e10 (select ?e9 ?e4))
+(let (?e11 (store ?e9 ?e8 ?e7))
+(let (?e12 (select ?e11 ?e10))
+(let (?e13 (f1 ?e11 ?e11))
+(let (?e14 (f1 v1 ?e13))
+(let (?e15 (f1 ?e9 ?e13))
+(flet ($e16 (p1 ?e14 ?e11 ?e15))
+(flet ($e17 (p1 ?e13 ?e15 v1))
+(flet ($e18 (p1 ?e9 ?e9 ?e14))
+(flet ($e19 (p0 ?e7))
+(flet ($e20 (<= v0 ?e4))
+(flet ($e21 (> ?e7 ?e12))
+(flet ($e22 (= ?e7 ?e12))
+(flet ($e23 (distinct ?e6 ?e5))
+(flet ($e24 (p0 ?e7))
+(flet ($e25 (>= ?e3 ?e8))
+(flet ($e26 (< ?e3 ?e7))
+(flet ($e27 (<= ?e7 v0))
+(flet ($e28 (p0 ?e10))
+(let (?e29 (ite $e27 ?e15 ?e13))
+(let (?e30 (ite $e28 ?e14 ?e14))
+(let (?e31 (ite $e26 ?e9 v1))
+(let (?e32 (ite $e17 ?e11 ?e13))
+(let (?e33 (ite $e23 ?e13 ?e13))
+(let (?e34 (ite $e25 ?e14 ?e30))
+(let (?e35 (ite $e22 ?e30 ?e30))
+(let (?e36 (ite $e25 ?e11 ?e31))
+(let (?e37 (ite $e22 ?e14 ?e35))
+(let (?e38 (ite $e19 ?e36 ?e35))
+(let (?e39 (ite $e21 ?e36 ?e9))
+(let (?e40 (ite $e16 ?e39 ?e11))
+(let (?e41 (ite $e28 ?e29 v1))
+(let (?e42 (ite $e25 ?e33 ?e36))
+(let (?e43 (ite $e21 ?e29 ?e9))
+(let (?e44 (ite $e18 ?e30 ?e13))
+(let (?e45 (ite $e18 ?e11 ?e41))
+(let (?e46 (ite $e20 ?e15 ?e34))
+(let (?e47 (ite $e24 ?e40 ?e13))
+(let (?e48 (ite $e26 ?e7 ?e6))
+(let (?e49 (ite $e21 ?e10 ?e6))
+(let (?e50 (ite $e22 v0 ?e8))
+(let (?e51 (ite $e19 ?e5 ?e4))
+(let (?e52 (ite $e16 ?e12 ?e10))
+(let (?e53 (ite $e16 ?e49 ?e8))
+(let (?e54 (ite $e21 ?e3 v0))
+(let (?e55 (ite $e24 ?e51 ?e52))
+(let (?e56 (ite $e23 ?e10 ?e5))
+(let (?e57 (ite $e18 ?e50 ?e49))
+(let (?e58 (ite $e17 ?e10 ?e4))
+(let (?e59 (ite $e27 ?e57 ?e12))
+(let (?e60 (ite $e21 ?e10 ?e3))
+(let (?e61 (ite $e28 ?e7 ?e55))
+(let (?e62 (ite $e20 ?e53 ?e53))
+(let (?e63 (ite $e25 ?e48 ?e8))
+(let (?e64 (store ?e45 ?e49 ?e8))
+(let (?e65 (store ?e43 ?e55 ?e57))
+(let (?e66 (select ?e34 v0))
+(let (?e67 (store ?e9 ?e66 ?e54))
+(let (?e68 (select ?e64 ?e56))
+(let (?e69 (f1 ?e11 ?e30))
+(let (?e70 (f1 ?e34 ?e36))
+(let (?e71 (f1 ?e38 ?e39))
+(let (?e72 (f1 ?e31 ?e45))
+(let (?e73 (f1 ?e43 ?e43))
+(let (?e74 (f1 ?e37 ?e65))
+(let (?e75 (f1 ?e9 ?e38))
+(let (?e76 (f1 ?e37 ?e14))
+(let (?e77 (f1 ?e13 ?e39))
+(let (?e78 (f1 ?e34 ?e39))
+(let (?e79 (f1 ?e64 ?e64))
+(let (?e80 (f1 ?e15 ?e15))
+(let (?e81 (f1 v1 v1))
+(let (?e82 (f1 ?e47 ?e71))
+(let (?e83 (f1 ?e77 ?e13))
+(let (?e84 (f1 ?e32 ?e32))
+(let (?e85 (f1 ?e46 ?e46))
+(let (?e86 (f1 ?e36 ?e72))
+(let (?e87 (f1 ?e81 ?e65))
+(let (?e88 (f1 ?e29 ?e45))
+(let (?e89 (f1 ?e44 ?e31))
+(let (?e90 (f1 ?e41 ?e41))
+(let (?e91 (f1 ?e34 ?e42))
+(let (?e92 (f1 ?e35 ?e35))
+(let (?e93 (f1 ?e33 ?e33))
+(let (?e94 (f1 ?e11 ?e14))
+(let (?e95 (f1 ?e67 ?e34))
+(let (?e96 (f1 ?e86 ?e37))
+(let (?e97 (f1 ?e40 ?e40))
+(let (?e98 (- ?e56 ?e5))
+(let (?e99 (+ ?e52 ?e57))
+(let (?e100 (ite (p0 ?e51) 1 0))
+(let (?e101 (ite (p0 ?e12) 1 0))
+(let (?e102 (ite (p0 ?e58) 1 0))
+(let (?e103 (+ v0 ?e10))
+(let (?e104 (~ ?e48))
+(let (?e105 (* ?e2 ?e12))
+(let (?e106 (- ?e3 ?e101))
+(let (?e107 (- ?e59 ?e100))
+(let (?e108 (ite (p0 ?e10) 1 0))
+(let (?e109 (* ?e2 ?e102))
+(let (?e110 (ite (p0 ?e7) 1 0))
+(let (?e111 (* ?e53 (~ ?e2)))
+(let (?e112 (* ?e2 ?e4))
+(let (?e113 (~ ?e106))
+(let (?e114 (~ ?e57))
+(let (?e115 (* ?e68 (~ ?e2)))
+(let (?e116 (- ?e4 ?e50))
+(let (?e117 (* ?e2 ?e49))
+(let (?e118 (ite (p0 ?e61) 1 0))
+(let (?e119 (ite (p0 ?e62) 1 0))
+(let (?e120 (* ?e10 ?e2))
+(let (?e121 (ite (p0 ?e119) 1 0))
+(let (?e122 (f0 ?e55))
+(let (?e123 (* (~ ?e2) ?e66))
+(let (?e124 (* ?e2 ?e63))
+(let (?e125 (ite (p0 ?e106) 1 0))
+(let (?e126 (f0 ?e102))
+(let (?e127 (f0 ?e55))
+(let (?e128 (f0 ?e103))
+(let (?e129 (~ ?e8))
+(let (?e130 (- ?e126 ?e6))
+(let (?e131 (* (~ ?e2) ?e60))
+(let (?e132 (* (~ ?e2) ?e54))
+(flet ($e133 (p1 ?e15 ?e73 ?e14))
+(flet ($e134 (p1 ?e47 ?e78 ?e81))
+(flet ($e135 (p1 ?e44 ?e80 ?e37))
+(flet ($e136 (p1 ?e42 ?e73 ?e91))
+(flet ($e137 (p1 ?e43 ?e37 ?e14))
+(flet ($e138 (p1 ?e73 ?e87 ?e34))
+(flet ($e139 (p1 ?e75 ?e46 ?e75))
+(flet ($e140 (p1 ?e96 ?e96 ?e88))
+(flet ($e141 (p1 ?e89 ?e78 ?e87))
+(flet ($e142 (p1 ?e70 ?e95 ?e47))
+(flet ($e143 (p1 ?e39 ?e96 ?e74))
+(flet ($e144 (p1 ?e91 ?e72 ?e70))
+(flet ($e145 (p1 v1 ?e65 ?e44))
+(flet ($e146 (p1 ?e90 ?e70 ?e79))
+(flet ($e147 (p1 ?e94 ?e91 ?e13))
+(flet ($e148 (p1 ?e41 ?e93 ?e32))
+(flet ($e149 (p1 ?e40 ?e91 ?e93))
+(flet ($e150 (p1 ?e92 ?e34 ?e80))
+(flet ($e151 (p1 ?e71 ?e44 ?e78))
+(flet ($e152 (p1 ?e43 ?e34 ?e73))
+(flet ($e153 (p1 ?e81 ?e73 ?e70))
+(flet ($e154 (p1 ?e86 ?e86 ?e38))
+(flet ($e155 (p1 ?e45 v1 ?e36))
+(flet ($e156 (p1 ?e43 ?e30 ?e37))
+(flet ($e157 (p1 ?e84 ?e78 ?e45))
+(flet ($e158 (p1 ?e67 ?e38 ?e90))
+(flet ($e159 (p1 ?e31 ?e81 ?e13))
+(flet ($e160 (p1 ?e64 ?e47 ?e94))
+(flet ($e161 (p1 ?e29 ?e75 ?e76))
+(flet ($e162 (p1 ?e85 ?e96 ?e82))
+(flet ($e163 (p1 ?e33 ?e29 ?e38))
+(flet ($e164 (p1 ?e31 ?e78 ?e69))
+(flet ($e165 (p1 ?e97 ?e9 ?e35))
+(flet ($e166 (p1 ?e83 ?e71 ?e79))
+(flet ($e167 (p1 ?e11 ?e67 ?e31))
+(flet ($e168 (p1 ?e39 ?e93 ?e96))
+(flet ($e169 (p1 ?e65 ?e85 ?e44))
+(flet ($e170 (p1 ?e76 ?e40 ?e15))
+(flet ($e171 (p1 ?e77 ?e34 ?e14))
+(flet ($e172 (distinct ?e129 ?e62))
+(flet ($e173 (p0 ?e116))
+(flet ($e174 (> ?e120 ?e10))
+(flet ($e175 (p0 ?e102))
+(flet ($e176 (> ?e50 ?e53))
+(flet ($e177 (> ?e119 ?e127))
+(flet ($e178 (distinct ?e117 ?e55))
+(flet ($e179 (= ?e122 ?e102))
+(flet ($e180 (< ?e123 ?e52))
+(flet ($e181 (> ?e66 ?e51))
+(flet ($e182 (= ?e121 ?e4))
+(flet ($e183 (distinct ?e130 ?e102))
+(flet ($e184 (< ?e111 ?e4))
+(flet ($e185 (p0 ?e68))
+(flet ($e186 (distinct ?e3 ?e3))
+(flet ($e187 (>= ?e66 ?e59))
+(flet ($e188 (< ?e10 ?e48))
+(flet ($e189 (distinct ?e5 ?e52))
+(flet ($e190 (= ?e101 ?e54))
+(flet ($e191 (>= ?e8 ?e116))
+(flet ($e192 (<= ?e62 ?e12))
+(flet ($e193 (< ?e131 ?e114))
+(flet ($e194 (>= ?e49 ?e125))
+(flet ($e195 (> ?e100 ?e7))
+(flet ($e196 (p0 ?e101))
+(flet ($e197 (distinct ?e118 ?e52))
+(flet ($e198 (<= v0 ?e60))
+(flet ($e199 (p0 ?e128))
+(flet ($e200 (>= ?e6 ?e106))
+(flet ($e201 (= ?e50 ?e61))
+(flet ($e202 (> ?e115 ?e132))
+(flet ($e203 (distinct ?e57 ?e102))
+(flet ($e204 (>= ?e102 ?e55))
+(flet ($e205 (p0 ?e55))
+(flet ($e206 (<= ?e113 ?e132))
+(flet ($e207 (<= ?e124 ?e106))
+(flet ($e208 (> ?e68 ?e117))
+(flet ($e209 (p0 ?e56))
+(flet ($e210 (<= ?e63 ?e112))
+(flet ($e211 (<= ?e119 ?e5))
+(flet ($e212 (= ?e105 ?e51))
+(flet ($e213 (< ?e6 ?e118))
+(flet ($e214 (p0 ?e66))
+(flet ($e215 (>= ?e58 ?e101))
+(flet ($e216 (distinct ?e109 ?e57))
+(flet ($e217 (distinct ?e99 ?e103))
+(flet ($e218 (<= ?e126 ?e58))
+(flet ($e219 (>= ?e107 ?e120))
+(flet ($e220 (< ?e125 ?e124))
+(flet ($e221 (> ?e98 ?e105))
+(flet ($e222 (p0 ?e118))
+(flet ($e223 (= ?e108 ?e4))
+(flet ($e224 (= ?e58 ?e114))
+(flet ($e225 (< ?e110 ?e123))
+(flet ($e226 (distinct ?e104 ?e111))
+(flet ($e227 (iff $e179 $e21))
+(flet ($e228 (if_then_else $e185 $e171 $e141))
+(flet ($e229 (and $e152 $e216))
+(flet ($e230 (and $e133 $e165))
+(flet ($e231 (and $e155 $e217))
+(flet ($e232 (iff $e16 $e180))
+(flet ($e233 (if_then_else $e168 $e191 $e153))
+(flet ($e234 (implies $e159 $e147))
+(flet ($e235 (not $e203))
+(flet ($e236 (xor $e28 $e223))
+(flet ($e237 (and $e174 $e172))
+(flet ($e238 (or $e194 $e197))
+(flet ($e239 (iff $e149 $e201))
+(flet ($e240 (not $e181))
+(flet ($e241 (or $e238 $e157))
+(flet ($e242 (and $e190 $e225))
+(flet ($e243 (implies $e140 $e215))
+(flet ($e244 (xor $e176 $e20))
+(flet ($e245 (not $e241))
+(flet ($e246 (iff $e243 $e158))
+(flet ($e247 (iff $e18 $e169))
+(flet ($e248 (xor $e173 $e210))
+(flet ($e249 (if_then_else $e212 $e143 $e218))
+(flet ($e250 (not $e177))
+(flet ($e251 (or $e207 $e163))
+(flet ($e252 (implies $e214 $e156))
+(flet ($e253 (or $e170 $e166))
+(flet ($e254 (iff $e206 $e209))
+(flet ($e255 (and $e231 $e189))
+(flet ($e256 (or $e148 $e167))
+(flet ($e257 (if_then_else $e237 $e248 $e235))
+(flet ($e258 (or $e138 $e142))
+(flet ($e259 (or $e249 $e164))
+(flet ($e260 (and $e208 $e204))
+(flet ($e261 (xor $e260 $e202))
+(flet ($e262 (xor $e193 $e136))
+(flet ($e263 (if_then_else $e184 $e219 $e227))
+(flet ($e264 (not $e145))
+(flet ($e265 (or $e256 $e187))
+(flet ($e266 (implies $e160 $e205))
+(flet ($e267 (iff $e178 $e134))
+(flet ($e268 (or $e220 $e27))
+(flet ($e269 (and $e265 $e25))
+(flet ($e270 (not $e242))
+(flet ($e271 (or $e270 $e255))
+(flet ($e272 (not $e199))
+(flet ($e273 (xor $e239 $e154))
+(flet ($e274 (or $e144 $e144))
+(flet ($e275 (if_then_else $e267 $e230 $e258))
+(flet ($e276 (not $e22))
+(flet ($e277 (and $e17 $e192))
+(flet ($e278 (and $e246 $e135))
+(flet ($e279 (and $e228 $e234))
+(flet ($e280 (and $e232 $e263))
+(flet ($e281 (and $e268 $e269))
+(flet ($e282 (if_then_else $e188 $e229 $e183))
+(flet ($e283 (if_then_else $e150 $e276 $e236))
+(flet ($e284 (if_then_else $e252 $e24 $e211))
+(flet ($e285 (iff $e264 $e151))
+(flet ($e286 (xor $e200 $e175))
+(flet ($e287 (or $e281 $e250))
+(flet ($e288 (if_then_else $e262 $e262 $e280))
+(flet ($e289 (not $e26))
+(flet ($e290 (if_then_else $e245 $e259 $e245))
+(flet ($e291 (not $e162))
+(flet ($e292 (if_then_else $e266 $e251 $e289))
+(flet ($e293 (implies $e254 $e275))
+(flet ($e294 (or $e273 $e293))
+(flet ($e295 (xor $e272 $e224))
+(flet ($e296 (implies $e257 $e240))
+(flet ($e297 (iff $e253 $e23))
+(flet ($e298 (iff $e19 $e292))
+(flet ($e299 (implies $e282 $e196))
+(flet ($e300 (iff $e284 $e139))
+(flet ($e301 (implies $e297 $e283))
+(flet ($e302 (and $e291 $e221))
+(flet ($e303 (not $e247))
+(flet ($e304 (xor $e294 $e161))
+(flet ($e305 (not $e244))
+(flet ($e306 (iff $e290 $e279))
+(flet ($e307 (and $e300 $e182))
+(flet ($e308 (implies $e288 $e195))
+(flet ($e309 (if_then_else $e304 $e299 $e186))
+(flet ($e310 (if_then_else $e261 $e222 $e213))
+(flet ($e311 (or $e286 $e301))
+(flet ($e312 (and $e311 $e298))
+(flet ($e313 (and $e295 $e302))
+(flet ($e314 (if_then_else $e305 $e278 $e278))
+(flet ($e315 (not $e226))
+(flet ($e316 (not $e303))
+(flet ($e317 (not $e315))
+(flet ($e318 (and $e296 $e137))
+(flet ($e319 (if_then_else $e307 $e308 $e313))
+(flet ($e320 (xor $e233 $e319))
+(flet ($e321 (if_then_else $e317 $e310 $e274))
+(flet ($e322 (not $e146))
+(flet ($e323 (xor $e198 $e321))
+(flet ($e324 (implies $e316 $e271))
+(flet ($e325 (xor $e312 $e314))
+(flet ($e326 (implies $e285 $e306))
+(flet ($e327 (if_then_else $e324 $e325 $e325))
+(flet ($e328 (if_then_else $e322 $e287 $e326))
+(flet ($e329 (implies $e323 $e309))
+(flet ($e330 (if_then_else $e327 $e329 $e318))
+(flet ($e331 (if_then_else $e277 $e330 $e277))
+(flet ($e332 (not $e328))
+(flet ($e333 (implies $e332 $e332))
+(flet ($e334 (not $e320))
+(flet ($e335 (implies $e333 $e334))
+(flet ($e336 (xor $e335 $e335))
+(flet ($e337 (iff $e331 $e336))
+$e337
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+