diff options
Diffstat (limited to 'test/regress/regress1/auflia-fuzz06.smt')
-rw-r--r-- | test/regress/regress1/auflia-fuzz06.smt | 349 |
1 files changed, 0 insertions, 349 deletions
diff --git a/test/regress/regress1/auflia-fuzz06.smt b/test/regress/regress1/auflia-fuzz06.smt deleted file mode 100644 index 88c2a9d5c..000000000 --- a/test/regress/regress1/auflia-fuzz06.smt +++ /dev/null @@ -1,349 +0,0 @@ -(benchmark fuzzsmt -:logic QF_AUFLIA -:status sat -:extrafuns ((f0 Int Int)) -:extrafuns ((f1 Array Array Array)) -:extrapreds ((p0 Int)) -:extrapreds ((p1 Array Array Array)) -:extrafuns ((v0 Int)) -:extrafuns ((v1 Array)) -:formula -(let (?e2 0) -(let (?e3 (ite (p0 v0) 1 0)) -(let (?e4 (ite (p0 v0) 1 0)) -(let (?e5 (~ ?e4)) -(let (?e6 (ite (p0 ?e3) 1 0)) -(let (?e7 (f0 ?e3)) -(let (?e8 (* ?e4 (~ ?e2))) -(let (?e9 (store v1 ?e5 ?e8)) -(let (?e10 (select ?e9 ?e4)) -(let (?e11 (store ?e9 ?e8 ?e7)) -(let (?e12 (select ?e11 ?e10)) -(let (?e13 (f1 ?e11 ?e11)) -(let (?e14 (f1 v1 ?e13)) -(let (?e15 (f1 ?e9 ?e13)) -(flet ($e16 (p1 ?e14 ?e11 ?e15)) -(flet ($e17 (p1 ?e13 ?e15 v1)) -(flet ($e18 (p1 ?e9 ?e9 ?e14)) -(flet ($e19 (p0 ?e7)) -(flet ($e20 (<= v0 ?e4)) -(flet ($e21 (> ?e7 ?e12)) -(flet ($e22 (= ?e7 ?e12)) -(flet ($e23 (distinct ?e6 ?e5)) -(flet ($e24 (p0 ?e7)) -(flet ($e25 (>= ?e3 ?e8)) -(flet ($e26 (< ?e3 ?e7)) -(flet ($e27 (<= ?e7 v0)) -(flet ($e28 (p0 ?e10)) -(let (?e29 (ite $e27 ?e15 ?e13)) -(let (?e30 (ite $e28 ?e14 ?e14)) -(let (?e31 (ite $e26 ?e9 v1)) -(let (?e32 (ite $e17 ?e11 ?e13)) -(let (?e33 (ite $e23 ?e13 ?e13)) -(let (?e34 (ite $e25 ?e14 ?e30)) -(let (?e35 (ite $e22 ?e30 ?e30)) -(let (?e36 (ite $e25 ?e11 ?e31)) -(let (?e37 (ite $e22 ?e14 ?e35)) -(let (?e38 (ite $e19 ?e36 ?e35)) -(let (?e39 (ite $e21 ?e36 ?e9)) -(let (?e40 (ite $e16 ?e39 ?e11)) -(let (?e41 (ite $e28 ?e29 v1)) -(let (?e42 (ite $e25 ?e33 ?e36)) -(let (?e43 (ite $e21 ?e29 ?e9)) -(let (?e44 (ite $e18 ?e30 ?e13)) -(let (?e45 (ite $e18 ?e11 ?e41)) -(let (?e46 (ite $e20 ?e15 ?e34)) -(let (?e47 (ite $e24 ?e40 ?e13)) -(let (?e48 (ite $e26 ?e7 ?e6)) -(let (?e49 (ite $e21 ?e10 ?e6)) -(let (?e50 (ite $e22 v0 ?e8)) -(let (?e51 (ite $e19 ?e5 ?e4)) -(let (?e52 (ite $e16 ?e12 ?e10)) -(let (?e53 (ite $e16 ?e49 ?e8)) -(let (?e54 (ite $e21 ?e3 v0)) -(let (?e55 (ite $e24 ?e51 ?e52)) -(let (?e56 (ite $e23 ?e10 ?e5)) -(let (?e57 (ite $e18 ?e50 ?e49)) -(let (?e58 (ite $e17 ?e10 ?e4)) -(let (?e59 (ite $e27 ?e57 ?e12)) -(let (?e60 (ite $e21 ?e10 ?e3)) -(let (?e61 (ite $e28 ?e7 ?e55)) -(let (?e62 (ite $e20 ?e53 ?e53)) -(let (?e63 (ite $e25 ?e48 ?e8)) -(let (?e64 (store ?e45 ?e49 ?e8)) -(let (?e65 (store ?e43 ?e55 ?e57)) -(let (?e66 (select ?e34 v0)) -(let (?e67 (store ?e9 ?e66 ?e54)) -(let (?e68 (select ?e64 ?e56)) -(let (?e69 (f1 ?e11 ?e30)) -(let (?e70 (f1 ?e34 ?e36)) -(let (?e71 (f1 ?e38 ?e39)) -(let (?e72 (f1 ?e31 ?e45)) -(let (?e73 (f1 ?e43 ?e43)) -(let (?e74 (f1 ?e37 ?e65)) -(let (?e75 (f1 ?e9 ?e38)) -(let (?e76 (f1 ?e37 ?e14)) -(let (?e77 (f1 ?e13 ?e39)) -(let (?e78 (f1 ?e34 ?e39)) -(let (?e79 (f1 ?e64 ?e64)) -(let (?e80 (f1 ?e15 ?e15)) -(let (?e81 (f1 v1 v1)) -(let (?e82 (f1 ?e47 ?e71)) -(let (?e83 (f1 ?e77 ?e13)) -(let (?e84 (f1 ?e32 ?e32)) -(let (?e85 (f1 ?e46 ?e46)) -(let (?e86 (f1 ?e36 ?e72)) -(let (?e87 (f1 ?e81 ?e65)) -(let (?e88 (f1 ?e29 ?e45)) -(let (?e89 (f1 ?e44 ?e31)) -(let (?e90 (f1 ?e41 ?e41)) -(let (?e91 (f1 ?e34 ?e42)) -(let (?e92 (f1 ?e35 ?e35)) -(let (?e93 (f1 ?e33 ?e33)) -(let (?e94 (f1 ?e11 ?e14)) -(let (?e95 (f1 ?e67 ?e34)) -(let (?e96 (f1 ?e86 ?e37)) -(let (?e97 (f1 ?e40 ?e40)) -(let (?e98 (- ?e56 ?e5)) -(let (?e99 (+ ?e52 ?e57)) -(let (?e100 (ite (p0 ?e51) 1 0)) -(let (?e101 (ite (p0 ?e12) 1 0)) -(let (?e102 (ite (p0 ?e58) 1 0)) -(let (?e103 (+ v0 ?e10)) -(let (?e104 (~ ?e48)) -(let (?e105 (* ?e2 ?e12)) -(let (?e106 (- ?e3 ?e101)) -(let (?e107 (- ?e59 ?e100)) -(let (?e108 (ite (p0 ?e10) 1 0)) -(let (?e109 (* ?e2 ?e102)) -(let (?e110 (ite (p0 ?e7) 1 0)) -(let (?e111 (* ?e53 (~ ?e2))) -(let (?e112 (* ?e2 ?e4)) -(let (?e113 (~ ?e106)) -(let (?e114 (~ ?e57)) -(let (?e115 (* ?e68 (~ ?e2))) -(let (?e116 (- ?e4 ?e50)) -(let (?e117 (* ?e2 ?e49)) -(let (?e118 (ite (p0 ?e61) 1 0)) -(let (?e119 (ite (p0 ?e62) 1 0)) -(let (?e120 (* ?e10 ?e2)) -(let (?e121 (ite (p0 ?e119) 1 0)) -(let (?e122 (f0 ?e55)) -(let (?e123 (* (~ ?e2) ?e66)) -(let (?e124 (* ?e2 ?e63)) -(let (?e125 (ite (p0 ?e106) 1 0)) -(let (?e126 (f0 ?e102)) -(let (?e127 (f0 ?e55)) -(let (?e128 (f0 ?e103)) -(let (?e129 (~ ?e8)) -(let (?e130 (- ?e126 ?e6)) -(let (?e131 (* (~ ?e2) ?e60)) -(let (?e132 (* (~ ?e2) ?e54)) -(flet ($e133 (p1 ?e15 ?e73 ?e14)) -(flet ($e134 (p1 ?e47 ?e78 ?e81)) -(flet ($e135 (p1 ?e44 ?e80 ?e37)) -(flet ($e136 (p1 ?e42 ?e73 ?e91)) -(flet ($e137 (p1 ?e43 ?e37 ?e14)) -(flet ($e138 (p1 ?e73 ?e87 ?e34)) -(flet ($e139 (p1 ?e75 ?e46 ?e75)) -(flet ($e140 (p1 ?e96 ?e96 ?e88)) -(flet ($e141 (p1 ?e89 ?e78 ?e87)) -(flet ($e142 (p1 ?e70 ?e95 ?e47)) -(flet ($e143 (p1 ?e39 ?e96 ?e74)) -(flet ($e144 (p1 ?e91 ?e72 ?e70)) -(flet ($e145 (p1 v1 ?e65 ?e44)) -(flet ($e146 (p1 ?e90 ?e70 ?e79)) -(flet ($e147 (p1 ?e94 ?e91 ?e13)) -(flet ($e148 (p1 ?e41 ?e93 ?e32)) -(flet ($e149 (p1 ?e40 ?e91 ?e93)) -(flet ($e150 (p1 ?e92 ?e34 ?e80)) -(flet ($e151 (p1 ?e71 ?e44 ?e78)) -(flet ($e152 (p1 ?e43 ?e34 ?e73)) -(flet ($e153 (p1 ?e81 ?e73 ?e70)) -(flet ($e154 (p1 ?e86 ?e86 ?e38)) -(flet ($e155 (p1 ?e45 v1 ?e36)) -(flet ($e156 (p1 ?e43 ?e30 ?e37)) -(flet ($e157 (p1 ?e84 ?e78 ?e45)) -(flet ($e158 (p1 ?e67 ?e38 ?e90)) -(flet ($e159 (p1 ?e31 ?e81 ?e13)) -(flet ($e160 (p1 ?e64 ?e47 ?e94)) -(flet ($e161 (p1 ?e29 ?e75 ?e76)) -(flet ($e162 (p1 ?e85 ?e96 ?e82)) -(flet ($e163 (p1 ?e33 ?e29 ?e38)) -(flet ($e164 (p1 ?e31 ?e78 ?e69)) -(flet ($e165 (p1 ?e97 ?e9 ?e35)) -(flet ($e166 (p1 ?e83 ?e71 ?e79)) -(flet ($e167 (p1 ?e11 ?e67 ?e31)) -(flet ($e168 (p1 ?e39 ?e93 ?e96)) -(flet ($e169 (p1 ?e65 ?e85 ?e44)) -(flet ($e170 (p1 ?e76 ?e40 ?e15)) -(flet ($e171 (p1 ?e77 ?e34 ?e14)) -(flet ($e172 (distinct ?e129 ?e62)) -(flet ($e173 (p0 ?e116)) -(flet ($e174 (> ?e120 ?e10)) -(flet ($e175 (p0 ?e102)) -(flet ($e176 (> ?e50 ?e53)) -(flet ($e177 (> ?e119 ?e127)) -(flet ($e178 (distinct ?e117 ?e55)) -(flet ($e179 (= ?e122 ?e102)) -(flet ($e180 (< ?e123 ?e52)) -(flet ($e181 (> ?e66 ?e51)) -(flet ($e182 (= ?e121 ?e4)) -(flet ($e183 (distinct ?e130 ?e102)) -(flet ($e184 (< ?e111 ?e4)) -(flet ($e185 (p0 ?e68)) -(flet ($e186 (distinct ?e3 ?e3)) -(flet ($e187 (>= ?e66 ?e59)) -(flet ($e188 (< ?e10 ?e48)) -(flet ($e189 (distinct ?e5 ?e52)) -(flet ($e190 (= ?e101 ?e54)) -(flet ($e191 (>= ?e8 ?e116)) -(flet ($e192 (<= ?e62 ?e12)) -(flet ($e193 (< ?e131 ?e114)) -(flet ($e194 (>= ?e49 ?e125)) -(flet ($e195 (> ?e100 ?e7)) -(flet ($e196 (p0 ?e101)) -(flet ($e197 (distinct ?e118 ?e52)) -(flet ($e198 (<= v0 ?e60)) -(flet ($e199 (p0 ?e128)) -(flet ($e200 (>= ?e6 ?e106)) -(flet ($e201 (= ?e50 ?e61)) -(flet ($e202 (> ?e115 ?e132)) -(flet ($e203 (distinct ?e57 ?e102)) -(flet ($e204 (>= ?e102 ?e55)) -(flet ($e205 (p0 ?e55)) -(flet ($e206 (<= ?e113 ?e132)) -(flet ($e207 (<= ?e124 ?e106)) -(flet ($e208 (> ?e68 ?e117)) -(flet ($e209 (p0 ?e56)) -(flet ($e210 (<= ?e63 ?e112)) -(flet ($e211 (<= ?e119 ?e5)) -(flet ($e212 (= ?e105 ?e51)) -(flet ($e213 (< ?e6 ?e118)) -(flet ($e214 (p0 ?e66)) -(flet ($e215 (>= ?e58 ?e101)) -(flet ($e216 (distinct ?e109 ?e57)) -(flet ($e217 (distinct ?e99 ?e103)) -(flet ($e218 (<= ?e126 ?e58)) -(flet ($e219 (>= ?e107 ?e120)) -(flet ($e220 (< ?e125 ?e124)) -(flet ($e221 (> ?e98 ?e105)) -(flet ($e222 (p0 ?e118)) -(flet ($e223 (= ?e108 ?e4)) -(flet ($e224 (= ?e58 ?e114)) -(flet ($e225 (< ?e110 ?e123)) -(flet ($e226 (distinct ?e104 ?e111)) -(flet ($e227 (iff $e179 $e21)) -(flet ($e228 (if_then_else $e185 $e171 $e141)) -(flet ($e229 (and $e152 $e216)) -(flet ($e230 (and $e133 $e165)) -(flet ($e231 (and $e155 $e217)) -(flet ($e232 (iff $e16 $e180)) -(flet ($e233 (if_then_else $e168 $e191 $e153)) -(flet ($e234 (implies $e159 $e147)) -(flet ($e235 (not $e203)) -(flet ($e236 (xor $e28 $e223)) -(flet ($e237 (and $e174 $e172)) -(flet ($e238 (or $e194 $e197)) -(flet ($e239 (iff $e149 $e201)) -(flet ($e240 (not $e181)) -(flet ($e241 (or $e238 $e157)) -(flet ($e242 (and $e190 $e225)) -(flet ($e243 (implies $e140 $e215)) -(flet ($e244 (xor $e176 $e20)) -(flet ($e245 (not $e241)) -(flet ($e246 (iff $e243 $e158)) -(flet ($e247 (iff $e18 $e169)) -(flet ($e248 (xor $e173 $e210)) -(flet ($e249 (if_then_else $e212 $e143 $e218)) -(flet ($e250 (not $e177)) -(flet ($e251 (or $e207 $e163)) -(flet ($e252 (implies $e214 $e156)) -(flet ($e253 (or $e170 $e166)) -(flet ($e254 (iff $e206 $e209)) -(flet ($e255 (and $e231 $e189)) -(flet ($e256 (or $e148 $e167)) -(flet ($e257 (if_then_else $e237 $e248 $e235)) -(flet ($e258 (or $e138 $e142)) -(flet ($e259 (or $e249 $e164)) -(flet ($e260 (and $e208 $e204)) -(flet ($e261 (xor $e260 $e202)) -(flet ($e262 (xor $e193 $e136)) -(flet ($e263 (if_then_else $e184 $e219 $e227)) -(flet ($e264 (not $e145)) -(flet ($e265 (or $e256 $e187)) -(flet ($e266 (implies $e160 $e205)) -(flet ($e267 (iff $e178 $e134)) -(flet ($e268 (or $e220 $e27)) -(flet ($e269 (and $e265 $e25)) -(flet ($e270 (not $e242)) -(flet ($e271 (or $e270 $e255)) -(flet ($e272 (not $e199)) -(flet ($e273 (xor $e239 $e154)) -(flet ($e274 (or $e144 $e144)) -(flet ($e275 (if_then_else $e267 $e230 $e258)) -(flet ($e276 (not $e22)) -(flet ($e277 (and $e17 $e192)) -(flet ($e278 (and $e246 $e135)) -(flet ($e279 (and $e228 $e234)) -(flet ($e280 (and $e232 $e263)) -(flet ($e281 (and $e268 $e269)) -(flet ($e282 (if_then_else $e188 $e229 $e183)) -(flet ($e283 (if_then_else $e150 $e276 $e236)) -(flet ($e284 (if_then_else $e252 $e24 $e211)) -(flet ($e285 (iff $e264 $e151)) -(flet ($e286 (xor $e200 $e175)) -(flet ($e287 (or $e281 $e250)) -(flet ($e288 (if_then_else $e262 $e262 $e280)) -(flet ($e289 (not $e26)) -(flet ($e290 (if_then_else $e245 $e259 $e245)) -(flet ($e291 (not $e162)) -(flet ($e292 (if_then_else $e266 $e251 $e289)) -(flet ($e293 (implies $e254 $e275)) -(flet ($e294 (or $e273 $e293)) -(flet ($e295 (xor $e272 $e224)) -(flet ($e296 (implies $e257 $e240)) -(flet ($e297 (iff $e253 $e23)) -(flet ($e298 (iff $e19 $e292)) -(flet ($e299 (implies $e282 $e196)) -(flet ($e300 (iff $e284 $e139)) -(flet ($e301 (implies $e297 $e283)) -(flet ($e302 (and $e291 $e221)) -(flet ($e303 (not $e247)) -(flet ($e304 (xor $e294 $e161)) -(flet ($e305 (not $e244)) -(flet ($e306 (iff $e290 $e279)) -(flet ($e307 (and $e300 $e182)) -(flet ($e308 (implies $e288 $e195)) -(flet ($e309 (if_then_else $e304 $e299 $e186)) -(flet ($e310 (if_then_else $e261 $e222 $e213)) -(flet ($e311 (or $e286 $e301)) -(flet ($e312 (and $e311 $e298)) -(flet ($e313 (and $e295 $e302)) -(flet ($e314 (if_then_else $e305 $e278 $e278)) -(flet ($e315 (not $e226)) -(flet ($e316 (not $e303)) -(flet ($e317 (not $e315)) -(flet ($e318 (and $e296 $e137)) -(flet ($e319 (if_then_else $e307 $e308 $e313)) -(flet ($e320 (xor $e233 $e319)) -(flet ($e321 (if_then_else $e317 $e310 $e274)) -(flet ($e322 (not $e146)) -(flet ($e323 (xor $e198 $e321)) -(flet ($e324 (implies $e316 $e271)) -(flet ($e325 (xor $e312 $e314)) -(flet ($e326 (implies $e285 $e306)) -(flet ($e327 (if_then_else $e324 $e325 $e325)) -(flet ($e328 (if_then_else $e322 $e287 $e326)) -(flet ($e329 (implies $e323 $e309)) -(flet ($e330 (if_then_else $e327 $e329 $e318)) -(flet ($e331 (if_then_else $e277 $e330 $e277)) -(flet ($e332 (not $e328)) -(flet ($e333 (implies $e332 $e332)) -(flet ($e334 (not $e320)) -(flet ($e335 (implies $e333 $e334)) -(flet ($e336 (xor $e335 $e335)) -(flet ($e337 (iff $e331 $e336)) -$e337 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |