1 files changed, 0 insertions, 370 deletions
diff --git a/test/regress/regress0/bv/fuzz09.smt b/test/regress/regress0/bv/fuzz09.smt
deleted file mode 100644
index ce8e9bfd6..000000000
--- a/test/regress/regress0/bv/fuzz09.smt
+++ /dev/null
@@ -1,370 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:status sat
-:extrafuns ((v0 BitVec[7]))
-:extrafuns ((v1 BitVec[5]))
-:extrafuns ((v2 BitVec[13]))
-:extrafuns ((v3 BitVec[16]))
-:formula
-(let (?e4 bv15872[14])
-(let (?e5 bv148[12])
-(let (?e6 (repeat[1] v2))
-(let (?e7 (ite (bvugt (sign_extend[6] v0) ?e6) bv1[1] bv0[1]))
-(let (?e8 (bvnor (sign_extend[2] v1) v0))
-(let (?e9 (sign_extend[1] v2))
-(let (?e10 (ite (bvsgt (sign_extend[6] v0) v2) bv1[1] bv0[1]))
-(let (?e11 (concat v0 v1))
-(let (?e12 (bvneg ?e6))
-(let (?e13 (bvsub (sign_extend[8] v1) v2))
-(let (?e14 (ite (bvule (sign_extend[13] ?e7) ?e9) bv1[1] bv0[1]))
-(let (?e15 (ite (bvult v1 (zero_extend[4] ?e7)) bv1[1] bv0[1]))
-(let (?e16 (bvnand (sign_extend[1] ?e5) v2))
-(let (?e17 (bvor ?e9 (sign_extend[9] v1)))
-(let (?e18 (bvxnor ?e9 (sign_extend[7] v0)))
-(let (?e19 (bvmul (sign_extend[1] ?e11) ?e16))
-(let (?e20 (bvand ?e18 (sign_extend[13] ?e14)))
-(let (?e21 (bvsub (zero_extend[12] ?e7) v2))
-(let (?e22 (bvmul ?e18 (zero_extend[7] v0)))
-(let (?e23 (rotate_right[13] ?e20))
-(let (?e24 (ite (bvult ?e22 (zero_extend[1] v2)) bv1[1] bv0[1]))
-(let (?e25 (bvneg ?e19))
-(let (?e26 (ite (bvult ?e5 (zero_extend[11] ?e10)) bv1[1] bv0[1]))
-(let (?e27 (bvxor ?e22 ?e4))
-(let (?e28 (ite (distinct (sign_extend[1] ?e5) ?e21) bv1[1] bv0[1]))
-(let (?e29 (bvlshr ?e6 (zero_extend[6] v0)))
-(let (?e30 (bvashr ?e10 ?e28))
-(let (?e31 (bvmul ?e24 ?e26))
-(let (?e32 (bvnand (sign_extend[2] ?e5) ?e20))
-(let (?e33 (bvxor v1 (sign_extend[4] ?e31)))
-(let (?e34 (bvor ?e26 ?e7))
-(let (?e35 (bvnot ?e6))
-(let (?e36 (extract[10:5] ?e21))
-(let (?e37 (ite (= ?e31 ?e15) bv1[1] bv0[1]))
-(let (?e38 (bvnot ?e11))
-(let (?e39 (extract[5:5] ?e13))
-(let (?e40 (bvadd (zero_extend[12] ?e24) ?e29))
-(let (?e41 (bvshl ?e13 (zero_extend[12] ?e7)))
-(let (?e42 (ite (bvuge ?e4 (zero_extend[1] ?e13)) bv1[1] bv0[1]))
-(let (?e43 (bvor (sign_extend[13] ?e15) ?e22))
-(let (?e44 (ite (bvsle ?e25 (zero_extend[6] v0)) bv1[1] bv0[1]))
-(let (?e45 (ite (bvslt ?e19 (sign_extend[8] v1)) bv1[1] bv0[1]))
-(let (?e46 (bvshl (zero_extend[1] ?e35) ?e22))
-(let (?e47 (sign_extend[4] ?e7))
-(let (?e48 (bvxor ?e6 (zero_extend[12] ?e30)))
-(let (?e49 (bvand v0 v0))
-(let (?e50 (bvand (sign_extend[12] ?e28) ?e16))
-(let (?e51 (bvmul (sign_extend[12] ?e34) ?e21))
-(let (?e52 (sign_extend[15] ?e45))
-(let (?e53 (bvnot ?e23))
-(let (?e54 (extract[5:3] ?e12))
-(let (?e55 (ite (bvslt (zero_extend[15] ?e42) ?e52) bv1[1] bv0[1]))
-(let (?e56 (bvneg ?e6))
-(let (?e57 (repeat[3] ?e47))
-(let (?e58 (ite (bvsle ?e38 (sign_extend[11] ?e44)) bv1[1] bv0[1]))
-(let (?e59 (sign_extend[0] ?e21))
-(let (?e60 (ite (bvsle ?e22 (zero_extend[13] ?e58)) bv1[1] bv0[1]))
-(let (?e61 (bvadd ?e7 ?e37))
-(let (?e62 (bvnor v3 (zero_extend[3] ?e50)))
-(flet ($e63 (= ?e46 (zero_extend[13] ?e7)))
-(flet ($e64 (= (zero_extend[12] ?e30) ?e29))
-(flet ($e65 (= (zero_extend[10] ?e54) ?e6))
-(flet ($e66 (= ?e20 (sign_extend[13] ?e44)))
-(flet ($e67 (= ?e43 (zero_extend[1] ?e19)))
-(flet ($e68 (= ?e9 (sign_extend[8] ?e36)))
-(flet ($e69 (= ?e56 (zero_extend[6] ?e49)))
-(flet ($e70 (= ?e52 (sign_extend[3] v2)))
-(flet ($e71 (= ?e6 (zero_extend[8] ?e47)))
-(flet ($e72 (= ?e56 (zero_extend[6] v0)))
-(flet ($e73 (= ?e33 (zero_extend[4] ?e34)))
-(flet ($e74 (= ?e32 ?e27))
-(flet ($e75 (= ?e12 (sign_extend[12] ?e34)))
-(flet ($e76 (= ?e21 ?e6))
-(flet ($e77 (= (sign_extend[12] ?e37) v2))
-(flet ($e78 (= ?e36 (sign_extend[5] ?e30)))
-(flet ($e79 (= v2 ?e13))
-(flet ($e80 (= (zero_extend[12] ?e55) ?e56))
-(flet ($e81 (= ?e52 (zero_extend[2] ?e9)))
-(flet ($e82 (= (sign_extend[12] ?e55) ?e13))
-(flet ($e83 (= ?e57 (sign_extend[1] ?e23)))
-(flet ($e84 (= (zero_extend[7] v0) ?e27))
-(flet ($e85 (= (sign_extend[15] ?e14) v3))
-(flet ($e86 (= ?e62 (sign_extend[2] ?e9)))
-(flet ($e87 (= (zero_extend[13] ?e31) ?e23))
-(flet ($e88 (= (zero_extend[2] ?e5) ?e46))
-(flet ($e89 (= ?e12 (zero_extend[1] ?e38)))
-(flet ($e90 (= ?e13 (zero_extend[12] ?e61)))
-(flet ($e91 (= (zero_extend[12] ?e30) ?e12))
-(flet ($e92 (= (zero_extend[4] ?e61) ?e33))
-(flet ($e93 (= ?e32 (sign_extend[1] ?e12)))
-(flet ($e94 (= ?e40 (sign_extend[12] ?e31)))
-(flet ($e95 (= (sign_extend[11] ?e28) ?e38))
-(flet ($e96 (= ?e36 (sign_extend[5] ?e26)))
-(flet ($e97 (= ?e6 ?e35))
-(flet ($e98 (= ?e52 (zero_extend[9] ?e8)))
-(flet ($e99 (= (sign_extend[7] ?e8) ?e53))
-(flet ($e100 (= (zero_extend[12] ?e42) ?e21))
-(flet ($e101 (= ?e46 (sign_extend[1] ?e51)))
-(flet ($e102 (= ?e46 (zero_extend[13] ?e26)))
-(flet ($e103 (= ?e31 ?e15))
-(flet ($e104 (= ?e59 (sign_extend[12] ?e7)))
-(flet ($e105 (= (sign_extend[12] ?e45) ?e48))
-(flet ($e106 (= ?e4 ?e4))
-(flet ($e107 (= ?e52 (sign_extend[4] ?e38)))
-(flet ($e108 (= ?e62 (sign_extend[3] ?e56)))
-(flet ($e109 (= ?e37 ?e60))
-(flet ($e110 (= (sign_extend[1] ?e36) ?e8))
-(flet ($e111 (= (sign_extend[1] ?e29) ?e22))
-(flet ($e112 (= ?e53 (sign_extend[13] ?e44)))
-(flet ($e113 (= ?e27 (sign_extend[13] ?e31)))
-(flet ($e114 (= (sign_extend[1] ?e59) ?e9))
-(flet ($e115 (= (zero_extend[1] ?e16) ?e22))
-(flet ($e116 (= (zero_extend[13] ?e7) ?e9))
-(flet ($e117 (= ?e40 ?e35))
-(flet ($e118 (= (zero_extend[13] ?e60) ?e22))
-(flet ($e119 (= ?e50 (sign_extend[1] ?e38)))
-(flet ($e120 (= ?e56 ?e35))
-(flet ($e121 (= ?e16 (sign_extend[12] ?e7)))
-(flet ($e122 (= (zero_extend[1] ?e5) ?e59))
-(flet ($e123 (= (sign_extend[7] ?e8) ?e22))
-(flet ($e124 (= ?e9 (sign_extend[1] v2)))
-(flet ($e125 (= (zero_extend[2] ?e39) ?e54))
-(flet ($e126 (= ?e36 (sign_extend[5] ?e34)))
-(flet ($e127 (= (zero_extend[9] ?e8) v3))
-(flet ($e128 (= ?e23 (zero_extend[2] ?e11)))
-(flet ($e129 (= (sign_extend[12] ?e55) ?e56))
-(flet ($e130 (= ?e57 (sign_extend[10] ?e33)))
-(flet ($e131 (= ?e23 ?e32))
-(flet ($e132 (= ?e62 (zero_extend[15] ?e58)))
-(flet ($e133 (= ?e30 ?e42))
-(flet ($e134 (= ?e26 ?e7))
-(flet ($e135 (= v2 ?e21))
-(flet ($e136 (= ?e53 ?e23))
-(flet ($e137 (= ?e23 (sign_extend[13] ?e37)))
-(flet ($e138 (= (sign_extend[13] ?e24) ?e53))
-(flet ($e139 (= (zero_extend[1] ?e13) ?e17))
-(flet ($e140 (= ?e58 ?e7))
-(flet ($e141 (= ?e6 (zero_extend[12] ?e14)))
-(flet ($e142 (= ?e15 ?e37))
-(flet ($e143 (= ?e16 (sign_extend[12] ?e39)))
-(flet ($e144 (= (zero_extend[12] ?e58) ?e59))
-(flet ($e145 (= ?e52 (sign_extend[2] ?e27)))
-(flet ($e146 (= (zero_extend[15] ?e15) ?e52))
-(flet ($e147 (= ?e43 (sign_extend[1] ?e56)))
-(flet ($e148 (= (zero_extend[10] ?e54) ?e35))
-(flet ($e149 (= ?e20 (zero_extend[13] ?e34)))
-(flet ($e150 (= (sign_extend[12] ?e44) ?e41))
-(flet ($e151 (= ?e41 (sign_extend[12] ?e34)))
-(flet ($e152 (= ?e18 (zero_extend[13] ?e55)))
-(flet ($e153 (= (zero_extend[2] ?e9) v3))
-(flet ($e154 (= (sign_extend[13] ?e45) ?e43))
-(flet ($e155 (= ?e40 ?e35))
-(flet ($e156 (= ?e19 (zero_extend[12] ?e61)))
-(flet ($e157 (= (zero_extend[1] ?e5) ?e59))
-(flet ($e158 (= ?e35 (zero_extend[12] ?e37)))
-(flet ($e159 (= ?e53 ?e43))
-(flet ($e160 (= ?e32 (zero_extend[2] ?e5)))
-(flet ($e161 (= ?e54 (sign_extend[2] ?e55)))
-(flet ($e162 (= ?e51 ?e12))
-(flet ($e163 (= (sign_extend[12] ?e34) ?e6))
-(flet ($e164 (= ?e17 ?e53))
-(flet ($e165 (= ?e53 ?e9))
-(flet ($e166 (= ?e8 (sign_extend[6] ?e10)))
-(flet ($e167 (= ?e10 ?e24))
-(flet ($e168 (= (sign_extend[11] ?e47) ?e62))
-(flet ($e169 (= (zero_extend[12] ?e42) v2))
-(flet ($e170 (= (sign_extend[11] ?e15) ?e5))
-(flet ($e171 (= (zero_extend[12] ?e45) v2))
-(flet ($e172 (= (zero_extend[1] ?e56) ?e20))
-(flet ($e173 (= ?e5 (sign_extend[7] v1)))
-(flet ($e174 (= ?e36 (sign_extend[3] ?e54)))
-(flet ($e175 (= ?e6 (sign_extend[12] ?e31)))
-(flet ($e176 (= (sign_extend[13] ?e42) ?e22))
-(flet ($e177 (= (sign_extend[2] ?e17) ?e62))
-(flet ($e178 (= (sign_extend[7] ?e33) ?e11))
-(flet ($e179 (= ?e27 (zero_extend[13] ?e14)))
-(flet ($e180 (= (zero_extend[2] v2) ?e57))
-(flet ($e181 (= v3 (zero_extend[3] ?e40)))
-(flet ($e182 (= ?e30 ?e24))
-(flet ($e183 (= (sign_extend[11] ?e30) ?e11))
-(flet ($e184 (= ?e17 (zero_extend[9] ?e33)))
-(flet ($e185 (= (sign_extend[7] ?e36) ?e51))
-(flet ($e186 (= (zero_extend[13] ?e61) ?e23))
-(flet ($e187 (= (sign_extend[15] ?e44) ?e52))
-(flet ($e188 (= ?e39 ?e34))
-(flet ($e189 (= ?e59 (sign_extend[12] ?e55)))
-(flet ($e190 (= v2 ?e16))
-(flet ($e191 (= ?e36 (zero_extend[5] ?e24)))
-(flet ($e192 (= (sign_extend[12] ?e10) ?e41))
-(flet ($e193 (= ?e57 (zero_extend[2] ?e6)))
-(flet ($e194 (= ?e31 ?e10))
-(flet ($e195 (= ?e38 (zero_extend[11] ?e58)))
-(flet ($e196 (= ?e27 (zero_extend[13] ?e58)))
-(flet ($e197 (= (zero_extend[13] ?e60) ?e4))
-(flet ($e198 (= ?e50 (sign_extend[12] ?e39)))
-(flet ($e199 (= ?e20 ?e32))
-(flet ($e200 (= (zero_extend[1] ?e12) ?e22))
-(flet ($e201 (= ?e51 (sign_extend[12] ?e14)))
-(flet ($e202 (= (sign_extend[2] ?e4) v3))
-(flet ($e203 (= (sign_extend[8] ?e36) ?e20))
-(flet ($e204 (= ?e62 (zero_extend[15] ?e42)))
-(flet ($e205 (= ?e21 (sign_extend[8] v1)))
-(flet ($e206 (= ?e33 (zero_extend[4] ?e60)))
-(flet ($e207 (= ?e55 ?e45))
-(flet ($e208 (= ?e55 ?e45))
-(flet ($e209 (= (zero_extend[13] ?e44) ?e20))
-(flet ($e210 (= (zero_extend[1] ?e11) ?e51))
-(flet ($e211 (= v3 (zero_extend[2] ?e27)))
-(flet ($e212 (= ?e25 ?e21))
-(flet ($e213 (iff $e200 $e110))
-(flet ($e214 (iff $e209 $e138))
-(flet ($e215 (if_then_else $e204 $e156 $e75))
-(flet ($e216 (xor $e191 $e126))
-(flet ($e217 (and $e175 $e151))
-(flet ($e218 (xor $e80 $e196))
-(flet ($e219 (xor $e202 $e187))
-(flet ($e220 (and $e114 $e163))
-(flet ($e221 (or $e63 $e203))
-(flet ($e222 (implies $e131 $e134))
-(flet ($e223 (iff $e152 $e108))
-(flet ($e224 (xor $e119 $e85))
-(flet ($e225 (not $e184))
-(flet ($e226 (implies $e88 $e213))
-(flet ($e227 (not $e161))
-(flet ($e228 (if_then_else $e201 $e103 $e112))
-(flet ($e229 (not $e118))
-(flet ($e230 (and $e82 $e122))
-(flet ($e231 (implies $e90 $e149))
-(flet ($e232 (implies $e120 $e193))
-(flet ($e233 (xor $e109 $e140))
-(flet ($e234 (or $e190 $e113))
-(flet ($e235 (or $e228 $e150))
-(flet ($e236 (or $e76 $e220))
-(flet ($e237 (iff $e144 $e155))
-(flet ($e238 (or $e142 $e159))
-(flet ($e239 (if_then_else $e222 $e158 $e100))
-(flet ($e240 (not $e129))
-(flet ($e241 (and $e164 $e179))
-(flet ($e242 (implies $e73 $e226))
-(flet ($e243 (xor $e166 $e66))
-(flet ($e244 (iff $e168 $e102))
-(flet ($e245 (not $e86))
-(flet ($e246 (if_then_else $e244 $e183 $e83))
-(flet ($e247 (if_then_else $e137 $e225 $e236))
-(flet ($e248 (if_then_else $e79 $e171 $e239))
-(flet ($e249 (xor $e217 $e176))
-(flet ($e250 (xor $e249 $e145))
-(flet ($e251 (implies $e194 $e195))
-(flet ($e252 (iff $e197 $e206))
-(flet ($e253 (xor $e95 $e243))
-(flet ($e254 (xor $e98 $e218))
-(flet ($e255 (not $e157))
-(flet ($e256 (if_then_else $e182 $e221 $e115))
-(flet ($e257 (or $e216 $e177))
-(flet ($e258 (iff $e139 $e235))
-(flet ($e259 (not $e172))
-(flet ($e260 (not $e77))
-(flet ($e261 (and $e180 $e125))
-(flet ($e262 (or $e91 $e87))
-(flet ($e263 (not $e135))
-(flet ($e264 (implies $e130 $e232))
-(flet ($e265 (if_then_else $e240 $e111 $e123))
-(flet ($e266 (not $e121))
-(flet ($e267 (xor $e199 $e147))
-(flet ($e268 (xor $e74 $e170))
-(flet ($e269 (implies $e192 $e267))
-(flet ($e270 (implies $e245 $e65))
-(flet ($e271 (implies $e230 $e148))
-(flet ($e272 (implies $e264 $e205))
-(flet ($e273 (and $e143 $e78))
-(flet ($e274 (not $e257))
-(flet ($e275 (xor $e261 $e167))
-(flet ($e276 (not $e268))
-(flet ($e277 (iff $e93 $e260))
-(flet ($e278 (if_then_else $e242 $e258 $e247))
-(flet ($e279 (if_then_else $e252 $e116 $e214))
-(flet ($e280 (implies $e259 $e189))
-(flet ($e281 (not $e141))
-(flet ($e282 (if_then_else $e96 $e208 $e127))
-(flet ($e283 (iff $e211 $e165))
-(flet ($e284 (implies $e255 $e185))
-(flet ($e285 (if_then_else $e278 $e162 $e272))
-(flet ($e286 (and $e128 $e282))
-(flet ($e287 (or $e263 $e273))
-(flet ($e288 (or $e106 $e215))
-(flet ($e289 (not $e71))
-(flet ($e290 (iff $e207 $e250))
-(flet ($e291 (or $e68 $e68))
-(flet ($e292 (implies $e72 $e212))
-(flet ($e293 (implies $e254 $e277))
-(flet ($e294 (not $e280))
-(flet ($e295 (not $e274))
-(flet ($e296 (implies $e256 $e233))
-(flet ($e297 (implies $e275 $e64))
-(flet ($e298 (or $e234 $e248))
-(flet ($e299 (or $e153 $e223))
-(flet ($e300 (if_then_else $e286 $e224 $e276))
-(flet ($e301 (or $e94 $e124))
-(flet ($e302 (or $e279 $e287))
-(flet ($e303 (if_then_else $e302 $e292 $e174))
-(flet ($e304 (if_then_else $e265 $e104 $e294))
-(flet ($e305 (or $e186 $e173))
-(flet ($e306 (if_then_else $e270 $e133 $e288))
-(flet ($e307 (and $e81 $e305))
-(flet ($e308 (xor $e293 $e291))
-(flet ($e309 (iff $e84 $e303))
-(flet ($e310 (xor $e262 $e284))
-(flet ($e311 (iff $e297 $e178))
-(flet ($e312 (iff $e198 $e132))
-(flet ($e313 (if_then_else $e169 $e304 $e146))
-(flet ($e314 (if_then_else $e306 $e285 $e307))
-(flet ($e315 (and $e281 $e289))
-(flet ($e316 (if_then_else $e309 $e299 $e97))
-(flet ($e317 (or $e266 $e117))
-(flet ($e318 (and $e227 $e301))
-(flet ($e319 (or $e300 $e317))
-(flet ($e320 (iff $e313 $e237))
-(flet ($e321 (or $e241 $e318))
-(flet ($e322 (and $e308 $e188))
-(flet ($e323 (xor $e269 $e154))
-(flet ($e324 (xor $e69 $e246))
-(flet ($e325 (or $e310 $e296))
-(flet ($e326 (implies $e136 $e311))
-(flet ($e327 (or $e326 $e160))
-(flet ($e328 (if_then_else $e295 $e238 $e229))
-(flet ($e329 (or $e316 $e322))
-(flet ($e330 (and $e319 $e89))
-(flet ($e331 (not $e298))
-(flet ($e332 (or $e219 $e92))
-(flet ($e333 (implies $e324 $e271))
-(flet ($e334 (iff $e251 $e323))
-(flet ($e335 (xor $e181 $e327))
-(flet ($e336 (implies $e331 $e210))
-(flet ($e337 (implies $e231 $e290))
-(flet ($e338 (iff $e312 $e99))
-(flet ($e339 (implies $e105 $e337))
-(flet ($e340 (implies $e325 $e339))
-(flet ($e341 (xor $e335 $e101))
-(flet ($e342 (iff $e253 $e330))
-(flet ($e343 (iff $e328 $e341))
-(flet ($e344 (and $e321 $e340))
-(flet ($e345 (and $e314 $e343))
-(flet ($e346 (iff $e333 $e329))
-(flet ($e347 (not $e70))
-(flet ($e348 (or $e283 $e107))
-(flet ($e349 (or $e336 $e345))
-(flet ($e350 (not $e332))
-(flet ($e351 (and $e315 $e342))
-(flet ($e352 (xor $e349 $e348))
-(flet ($e353 (xor $e67 $e344))
-(flet ($e354 (not $e334))
-(flet ($e355 (and $e354 $e352))
-(flet ($e356 (if_then_else $e351 $e355 $e347))
-(flet ($e357 (and $e346 $e320))
-(flet ($e358 (iff $e350 $e338))
-(flet ($e359 (not $e353))
-(flet ($e360 (or $e359 $e357))
-(flet ($e361 (xor $e360 $e356))
-(flet ($e362 (implies $e361 $e358))
-$e362
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-