diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz09.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz09.smt | 370 |
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 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |