diff options
Diffstat (limited to 'test/regress/regress0/aufbv/fuzz01.smt')
-rw-r--r-- | test/regress/regress0/aufbv/fuzz01.smt | 365 |
1 files changed, 365 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/fuzz01.smt b/test/regress/regress0/aufbv/fuzz01.smt new file mode 100644 index 000000000..233427ae0 --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz01.smt @@ -0,0 +1,365 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status unknown +: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 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |