diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz09.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz09.smt | 370 |
1 files changed, 370 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz09.smt b/test/regress/regress0/bv/fuzz09.smt new file mode 100644 index 000000000..ce8e9bfd6 --- /dev/null +++ b/test/regress/regress0/bv/fuzz09.smt @@ -0,0 +1,370 @@ +(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 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |