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