diff options
Diffstat (limited to 'test/regress/regress0/decision/aufbv-fuzz01.smt')
-rw-r--r-- | test/regress/regress0/decision/aufbv-fuzz01.smt | 368 |
1 files changed, 0 insertions, 368 deletions
diff --git a/test/regress/regress0/decision/aufbv-fuzz01.smt b/test/regress/regress0/decision/aufbv-fuzz01.smt deleted file mode 100644 index 0846c4c38..000000000 --- a/test/regress/regress0/decision/aufbv-fuzz01.smt +++ /dev/null @@ -1,368 +0,0 @@ -; COMMAND-LINE: --decision=justification -; EXPECT: sat - -(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 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |