diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-09-04 10:06:56 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-04 10:06:56 -0700 |
commit | ad521125586f437693410dd78275044d0174a927 (patch) | |
tree | 54453e3454d0279b9975d8f1f7ec61d010083478 /test/regress/regress0 | |
parent | f727de338f15a02e07d2a79cf94940a9786e0864 (diff) |
Remove duplicate regression tests. (#3227)
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/bug374.delta01.smt | 1197 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.04.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress0/hung10_itesdk_output2.smt2 | 30 | ||||
-rw-r--r-- | test/regress/regress0/hung13sdk_output2.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/queries0.cvc | 11 |
7 files changed, 3 insertions, 1281 deletions
diff --git a/test/regress/regress0/bug374.delta01.smt b/test/regress/regress0/bug374.delta01.smt deleted file mode 100644 index e338417c5..000000000 --- a/test/regress/regress0/bug374.delta01.smt +++ /dev/null @@ -1,1197 +0,0 @@ -(benchmark fuzzsmt -:logic AUFLIA -:status unknown -:extrafuns ((f0 Int Int Int)) -:extrafuns ((f1 Array Array Array Array)) -:extrapreds ((p0 Int)) -:extrapreds ((p1 Array)) -:extrafuns ((v0 Int)) -:extrafuns ((v1 Array)) -:assumption -(exists (?qvar0 Int) (?qvar1 Int) (?qvar2 Int) -(flet ($qf0 (<= (f0 ?qvar1 ?qvar2) (f0 ?qvar0 ?qvar2))) -$qf0 -)) -:formula -(let (?e2 1) -(let (?e3 0) -(let (?e4 (ite (p0 v0) 1 0)) -(let (?e5 (* ?e3 v0)) -(let (?e6 (+ ?e5 ?e5)) -(let (?e7 (f0 ?e6 ?e4)) -(let (?e8 (~ v0)) -(let (?e9 (f0 ?e4 ?e5)) -(let (?e10 (f0 ?e6 ?e6)) -(let (?e11 (- ?e9 ?e7)) -(let (?e12 (+ ?e10 ?e7)) -(let (?e13 (ite (p0 ?e12) 1 0)) -(let (?e14 (* ?e3 ?e12)) -(let (?e15 (+ ?e8 ?e7)) -(let (?e16 (f0 ?e15 ?e10)) -(let (?e17 (* ?e15 ?e2)) -(let (?e18 (store v1 ?e12 ?e14)) -(let (?e19 (store v1 ?e8 ?e12)) -(let (?e20 (f1 v1 v1 v1)) -(let (?e21 (f1 ?e18 ?e20 ?e19)) -(flet ($e22 (p1 v1)) -(flet ($e23 (p1 ?e18)) -(flet ($e24 (p1 v1)) -(flet ($e25 (p1 ?e19)) -(flet ($e26 (p1 ?e20)) -(flet ($e27 (p1 ?e21)) -(flet ($e28 (<= ?e14 ?e16)) -(flet ($e29 (>= ?e4 v0)) -(flet ($e30 (< ?e13 ?e13)) -(flet ($e31 (<= ?e9 ?e6)) -(flet ($e32 (< ?e5 ?e13)) -(flet ($e33 (< ?e8 ?e11)) -(flet ($e34 (> ?e8 ?e9)) -(flet ($e35 (<= ?e7 ?e4)) -(flet ($e36 (distinct ?e13 ?e11)) -(flet ($e37 (distinct ?e17 ?e15)) -(flet ($e38 (= ?e8 ?e8)) -(flet ($e39 (distinct ?e16 ?e17)) -(flet ($e40 (= ?e12 ?e8)) -(flet ($e41 (distinct v0 ?e12)) -(flet ($e42 (= ?e11 ?e16)) -(flet ($e43 (< ?e10 ?e14)) -(flet ($e44 (> ?e17 ?e5)) -(flet ($e45 (distinct ?e11 ?e9)) -(flet ($e46 (> ?e14 v0)) -(flet ($e47 (<= v0 ?e7)) -(flet ($e48 (<= ?e13 ?e17)) -(flet ($e49 (> ?e13 ?e7)) -(flet ($e50 (> ?e17 v0)) -(flet ($e51 (>= ?e11 ?e14)) -(flet ($e52 (<= ?e14 ?e13)) -(flet ($e53 (<= ?e8 ?e6)) -(flet ($e54 (<= v0 ?e16)) -(flet ($e55 (distinct ?e6 v0)) -(flet ($e56 (> ?e7 ?e10)) -(flet ($e57 (distinct ?e11 ?e13)) -(flet ($e58 (> ?e6 ?e13)) -(flet ($e59 (distinct v0 ?e12)) -(flet ($e60 (distinct ?e14 ?e9)) -(flet ($e61 (> ?e8 ?e15)) -(flet ($e62 (= ?e9 ?e16)) -(flet ($e63 (= ?e14 ?e13)) -(flet ($e64 (> ?e11 ?e6)) -(flet ($e65 (distinct ?e16 ?e9)) -(flet ($e66 (>= ?e5 ?e7)) -(flet ($e67 (<= ?e9 ?e17)) -(flet ($e68 (= ?e13 v0)) -(flet ($e69 (p0 ?e13)) -(let (?e70 (ite $e33 ?e18 ?e18)) -(let (?e71 (ite $e25 ?e21 ?e19)) -(let (?e72 (ite $e23 ?e71 ?e18)) -(let (?e73 (ite $e36 v1 ?e71)) -(let (?e74 (ite $e44 v1 ?e21)) -(let (?e75 (ite $e65 ?e20 ?e20)) -(let (?e76 (ite $e30 v1 ?e71)) -(let (?e77 (ite $e28 ?e21 ?e20)) -(let (?e78 (ite $e67 ?e77 ?e75)) -(let (?e79 (ite $e29 ?e21 ?e70)) -(let (?e80 (ite $e54 ?e18 ?e74)) -(let (?e81 (ite $e53 ?e80 ?e79)) -(let (?e82 (ite $e27 v1 ?e79)) -(let (?e83 (ite $e37 ?e18 ?e75)) -(let (?e84 (ite $e30 ?e78 ?e82)) -(let (?e85 (ite $e47 ?e74 ?e21)) -(let (?e86 (ite $e67 ?e19 ?e21)) -(let (?e87 (ite $e32 ?e78 ?e86)) -(let (?e88 (ite $e50 ?e72 ?e80)) -(let (?e89 (ite $e63 ?e84 ?e88)) -(let (?e90 (ite $e46 ?e73 ?e21)) -(let (?e91 (ite $e27 ?e20 ?e74)) -(let (?e92 (ite $e60 ?e91 ?e83)) -(let (?e93 (ite $e55 ?e71 ?e19)) -(let (?e94 (ite $e40 ?e85 ?e81)) -(let (?e95 (ite $e56 ?e78 ?e20)) -(let (?e96 (ite $e27 ?e92 ?e79)) -(let (?e97 (ite $e68 ?e95 ?e86)) -(let (?e98 (ite $e39 ?e77 ?e94)) -(let (?e99 (ite $e57 ?e87 ?e79)) -(let (?e100 (ite $e60 ?e91 ?e99)) -(let (?e101 (ite $e33 ?e89 ?e93)) -(let (?e102 (ite $e43 ?e72 ?e82)) -(let (?e103 (ite $e24 ?e74 ?e81)) -(let (?e104 (ite $e38 ?e99 ?e99)) -(let (?e105 (ite $e64 ?e91 ?e77)) -(let (?e106 (ite $e57 ?e93 ?e79)) -(let (?e107 (ite $e51 ?e96 ?e88)) -(let (?e108 (ite $e24 ?e76 ?e102)) -(let (?e109 (ite $e62 ?e93 ?e97)) -(let (?e110 (ite $e26 ?e106 v1)) -(let (?e111 (ite $e48 ?e106 ?e70)) -(let (?e112 (ite $e58 ?e73 ?e76)) -(let (?e113 (ite $e61 ?e111 ?e106)) -(let (?e114 (ite $e69 ?e105 ?e81)) -(let (?e115 (ite $e22 ?e96 ?e100)) -(let (?e116 (ite $e48 ?e109 ?e88)) -(let (?e117 (ite $e31 v1 ?e77)) -(let (?e118 (ite $e41 ?e93 ?e86)) -(let (?e119 (ite $e24 ?e113 ?e20)) -(let (?e120 (ite $e46 ?e101 ?e110)) -(let (?e121 (ite $e28 ?e77 ?e96)) -(let (?e122 (ite $e49 ?e107 ?e105)) -(let (?e123 (ite $e59 ?e21 ?e73)) -(let (?e124 (ite $e22 ?e116 ?e116)) -(let (?e125 (ite $e31 ?e77 ?e111)) -(let (?e126 (ite $e66 ?e103 ?e93)) -(let (?e127 (ite $e45 ?e96 ?e100)) -(let (?e128 (ite $e52 ?e125 ?e78)) -(let (?e129 (ite $e38 ?e70 ?e112)) -(let (?e130 (ite $e42 ?e105 ?e77)) -(let (?e131 (ite $e38 ?e91 ?e119)) -(let (?e132 (ite $e35 ?e113 ?e96)) -(let (?e133 (ite $e34 ?e115 ?e86)) -(let (?e134 (ite $e57 v0 ?e9)) -(let (?e135 (ite $e22 ?e7 ?e11)) -(let (?e136 (ite $e44 ?e135 ?e10)) -(let (?e137 (ite $e46 ?e10 ?e14)) -(let (?e138 (ite $e31 ?e4 ?e16)) -(let (?e139 (ite $e63 ?e17 ?e10)) -(let (?e140 (ite $e62 ?e4 ?e8)) -(let (?e141 (ite $e69 ?e12 ?e138)) -(let (?e142 (ite $e44 ?e13 ?e140)) -(let (?e143 (ite $e53 ?e15 ?e15)) -(let (?e144 (ite $e59 ?e142 ?e137)) -(let (?e145 (ite $e24 ?e4 ?e137)) -(let (?e146 (ite $e68 ?e13 ?e4)) -(let (?e147 (ite $e49 ?e12 ?e14)) -(let (?e148 (ite $e49 ?e6 ?e134)) -(let (?e149 (ite $e54 ?e137 ?e9)) -(let (?e150 (ite $e60 ?e5 ?e9)) -(let (?e151 (ite $e64 ?e13 ?e4)) -(let (?e152 (ite $e65 ?e139 ?e149)) -(let (?e153 (ite $e34 ?e143 ?e138)) -(let (?e154 (ite $e40 ?e145 ?e151)) -(let (?e155 (ite $e32 ?e141 ?e137)) -(let (?e156 (ite $e56 ?e16 ?e148)) -(let (?e157 (ite $e28 ?e152 ?e14)) -(let (?e158 (ite $e47 ?e141 ?e152)) -(let (?e159 (ite $e43 ?e8 ?e6)) -(let (?e160 (ite $e51 ?e135 ?e146)) -(let (?e161 (ite $e50 ?e141 ?e151)) -(let (?e162 (ite $e69 ?e14 ?e148)) -(let (?e163 (ite $e45 ?e145 ?e154)) -(let (?e164 (ite $e55 ?e150 ?e4)) -(let (?e165 (ite $e46 ?e146 ?e4)) -(let (?e166 (ite $e63 ?e142 ?e143)) -(let (?e167 (ite $e24 ?e156 ?e5)) -(let (?e168 (ite $e30 ?e164 ?e146)) -(let (?e169 (ite $e38 ?e11 ?e165)) -(let (?e170 (ite $e48 ?e12 ?e135)) -(let (?e171 (ite $e25 ?e168 ?e4)) -(let (?e172 (ite $e33 ?e163 ?e142)) -(let (?e173 (ite $e49 ?e7 ?e159)) -(let (?e174 (ite $e69 ?e16 ?e10)) -(let (?e175 (ite $e46 ?e156 ?e166)) -(let (?e176 (ite $e39 ?e135 ?e134)) -(let (?e177 (ite $e57 ?e161 ?e9)) -(let (?e178 (ite $e33 ?e153 ?e139)) -(let (?e179 (ite $e62 ?e138 ?e169)) -(let (?e180 (ite $e23 ?e146 ?e166)) -(let (?e181 (ite $e66 ?e140 ?e148)) -(let (?e182 (ite $e32 ?e163 ?e136)) -(let (?e183 (ite $e58 ?e134 ?e141)) -(let (?e184 (ite $e61 ?e9 ?e174)) -(let (?e185 (ite $e37 ?e155 ?e148)) -(let (?e186 (ite $e34 ?e157 ?e185)) -(let (?e187 (ite $e68 ?e139 ?e12)) -(let (?e188 (ite $e34 ?e164 ?e168)) -(let (?e189 (ite $e42 ?e160 ?e139)) -(let (?e190 (ite $e36 ?e17 ?e138)) -(let (?e191 (ite $e52 ?e173 ?e143)) -(let (?e192 (ite $e35 ?e157 ?e140)) -(let (?e193 (ite $e65 ?e139 ?e184)) -(let (?e194 (ite $e27 ?e9 ?e141)) -(let (?e195 (ite $e24 ?e167 ?e144)) -(let (?e196 (ite $e67 ?e177 ?e144)) -(let (?e197 (ite $e26 ?e14 ?e174)) -(let (?e198 (ite $e47 ?e182 ?e156)) -(let (?e199 (ite $e28 ?e156 ?e158)) -(let (?e200 (ite $e41 ?e163 ?e185)) -(let (?e201 (ite $e52 ?e190 ?e178)) -(let (?e202 (ite $e29 ?e186 ?e171)) -(let (?e203 (store ?e133 ?e177 ?e190)) -(let (?e204 (store ?e102 ?e193 ?e151)) -(let (?e205 (select ?e120 ?e173)) -(let (?e206 (store ?e101 ?e6 ?e202)) -(let (?e207 (f1 ?e114 ?e124 ?e87)) -(let (?e208 (f1 ?e99 ?e19 ?e116)) -(let (?e209 (f1 ?e91 ?e91 ?e91)) -(let (?e210 (f1 ?e92 ?e112 ?e95)) -(let (?e211 (f1 ?e210 ?e123 ?e72)) -(let (?e212 (f1 ?e82 ?e203 ?e84)) -(let (?e213 (f1 ?e127 ?e91 ?e122)) -(let (?e214 (f1 ?e75 ?e75 ?e75)) -(let (?e215 (f1 ?e126 ?e111 ?e209)) -(let (?e216 (f1 ?e77 ?e77 ?e77)) -(let (?e217 (f1 ?e94 ?e94 ?e94)) -(let (?e218 (f1 ?e80 ?e80 ?e87)) -(let (?e219 (f1 ?e80 ?e207 ?e73)) -(let (?e220 (f1 ?e76 ?e76 ?e90)) -(let (?e221 (f1 ?e128 ?e128 ?e207)) -(let (?e222 (f1 ?e86 ?e108 ?e98)) -(let (?e223 (f1 ?e109 ?e73 ?e72)) -(let (?e224 (f1 ?e97 ?e97 ?e80)) -(let (?e225 (f1 ?e223 ?e76 ?e206)) -(let (?e226 (f1 ?e113 ?e113 ?e113)) -(let (?e227 (f1 ?e86 ?e118 ?e204)) -(let (?e228 (f1 ?e116 ?e203 ?e214)) -(let (?e229 (f1 ?e88 ?e219 ?e120)) -(let (?e230 (f1 ?e70 ?e77 ?e220)) -(let (?e231 (f1 ?e109 ?e72 ?e91)) -(let (?e232 (f1 v1 ?e130 ?e211)) -(let (?e233 (f1 ?e91 ?e128 ?e130)) -(let (?e234 (f1 ?e21 ?e207 ?e117)) -(let (?e235 (f1 ?e78 ?e78 ?e133)) -(let (?e236 (f1 ?e115 ?e94 ?e210)) -(let (?e237 (f1 ?e100 ?e80 ?e214)) -(let (?e238 (f1 ?e113 ?e77 ?e120)) -(let (?e239 (f1 ?e113 ?e108 ?e212)) -(let (?e240 (f1 ?e107 ?e107 ?e226)) -(let (?e241 (f1 ?e106 ?e106 ?e235)) -(let (?e242 (f1 ?e121 ?e121 ?e219)) -(let (?e243 (f1 ?e110 ?e110 ?e110)) -(let (?e244 (f1 ?e115 ?e107 ?e225)) -(let (?e245 (f1 ?e226 ?e83 ?e100)) -(let (?e246 (f1 ?e18 ?e18 ?e116)) -(let (?e247 (f1 v1 ?e107 ?e98)) -(let (?e248 (f1 ?e235 ?e121 ?e241)) -(let (?e249 (f1 ?e71 ?e96 ?e210)) -(let (?e250 (f1 ?e101 ?e212 ?e237)) -(let (?e251 (f1 ?e132 ?e132 ?e110)) -(let (?e252 (f1 ?e133 ?e233 ?e129)) -(let (?e253 (f1 ?e77 ?e81 ?e118)) -(let (?e254 (f1 ?e231 ?e106 ?e98)) -(let (?e255 (f1 ?e87 ?e76 ?e73)) -(let (?e256 (f1 ?e248 ?e103 ?e222)) -(let (?e257 (f1 ?e105 ?e105 ?e254)) -(let (?e258 (f1 ?e243 ?e104 ?e120)) -(let (?e259 (f1 ?e20 ?e126 ?e243)) -(let (?e260 (f1 ?e259 ?e102 ?e115)) -(let (?e261 (f1 ?e128 ?e73 ?e222)) -(let (?e262 (f1 ?e125 ?e101 ?e126)) -(let (?e263 (f1 ?e119 ?e77 ?e240)) -(let (?e264 (f1 ?e131 ?e225 ?e229)) -(let (?e265 (f1 ?e254 ?e109 ?e230)) -(let (?e266 (f1 ?e211 ?e242 ?e219)) -(let (?e267 (f1 ?e85 ?e128 ?e76)) -(let (?e268 (f1 ?e89 ?e241 ?e262)) -(let (?e269 (f1 ?e74 ?e122 ?e117)) -(let (?e270 (f1 ?e93 ?e93 ?e93)) -(let (?e271 (f1 ?e79 ?e79 ?e79)) -(let (?e272 (* ?e192 (~ ?e2))) -(let (?e273 (ite (p0 ?e177) 1 0)) -(let (?e274 (ite (p0 ?e165) 1 0)) -(let (?e275 (~ ?e156)) -(let (?e276 (+ ?e162 ?e12)) -(let (?e277 (f0 ?e148 ?e272)) -(let (?e278 (f0 ?e8 ?e11)) -(let (?e279 (+ ?e198 ?e6)) -(let (?e280 (~ ?e182)) -(let (?e281 (+ ?e16 ?e141)) -(let (?e282 (* (~ ?e3) ?e157)) -(let (?e283 (ite (p0 ?e146) 1 0)) -(let (?e284 (~ ?e189)) -(let (?e285 (- ?e277 ?e189)) -(let (?e286 (- ?e284 ?e158)) -(let (?e287 (~ ?e176)) -(let (?e288 (* ?e3 ?e178)) -(let (?e289 (* ?e3 ?e136)) -(let (?e290 (* ?e3 ?e4)) -(let (?e291 (- ?e146 ?e152)) -(let (?e292 (f0 ?e135 ?e136)) -(let (?e293 (f0 ?e278 ?e161)) -(let (?e294 (~ ?e10)) -(let (?e295 (ite (p0 ?e163) 1 0)) -(let (?e296 (f0 ?e8 ?e192)) -(let (?e297 (* ?e159 (~ ?e3))) -(let (?e298 (- ?e145 ?e159)) -(let (?e299 (- ?e158 ?e200)) -(let (?e300 (+ ?e170 ?e7)) -(let (?e301 (f0 ?e142 ?e295)) -(let (?e302 (+ ?e193 ?e149)) -(let (?e303 (* ?e301 (~ ?e3))) -(let (?e304 (* ?e190 ?e2)) -(let (?e305 (- ?e15 ?e152)) -(let (?e306 (+ ?e179 ?e138)) -(let (?e307 (* (~ ?e3) ?e147)) -(let (?e308 (- ?e178 ?e202)) -(let (?e309 (* ?e172 ?e2)) -(let (?e310 (ite (p0 ?e183) 1 0)) -(let (?e311 (f0 ?e294 ?e149)) -(let (?e312 (- ?e151 ?e202)) -(let (?e313 (f0 ?e164 v0)) -(let (?e314 (f0 ?e165 ?e4)) -(let (?e315 (- ?e143 ?e285)) -(let (?e316 (f0 ?e134 ?e174)) -(let (?e317 (~ ?e175)) -(let (?e318 (+ ?e9 ?e185)) -(let (?e319 (* (~ ?e2) ?e137)) -(let (?e320 (* ?e169 ?e2)) -(let (?e321 (* ?e3 ?e146)) -(let (?e322 (* ?e184 ?e2)) -(let (?e323 (f0 ?e179 ?e169)) -(let (?e324 (f0 ?e144 ?e297)) -(let (?e325 (+ ?e153 ?e154)) -(let (?e326 (f0 ?e173 ?e151)) -(let (?e327 (~ ?e191)) -(let (?e328 (f0 ?e201 ?e323)) -(let (?e329 (+ ?e278 ?e272)) -(let (?e330 (* ?e150 (~ ?e2))) -(let (?e331 (* ?e197 (~ ?e3))) -(let (?e332 (- ?e205 ?e169)) -(let (?e333 (- ?e17 ?e288)) -(let (?e334 (ite (p0 ?e199) 1 0)) -(let (?e335 (f0 ?e181 ?e304)) -(let (?e336 (- ?e14 ?e201)) -(let (?e337 (f0 ?e168 ?e291)) -(let (?e338 (f0 ?e279 ?e180)) -(let (?e339 (+ ?e160 ?e162)) -(let (?e340 (- ?e196 ?e163)) -(let (?e341 (f0 ?e140 ?e175)) -(let (?e342 (- ?e147 ?e282)) -(let (?e343 (* ?e5 (~ ?e3))) -(let (?e344 (f0 ?e284 ?e298)) -(let (?e345 (- ?e284 ?e272)) -(let (?e346 (* ?e2 ?e326)) -(let (?e347 (ite (p0 ?e139) 1 0)) -(let (?e348 (f0 ?e273 ?e285)) -(let (?e349 (* ?e2 ?e315)) -(let (?e350 (* (~ ?e3) ?e15)) -(let (?e351 (ite (p0 ?e320) 1 0)) -(let (?e352 (- ?e155 ?e317)) -(let (?e353 (* ?e194 ?e3)) -(let (?e354 (~ ?e143)) -(let (?e355 (ite (p0 ?e338) 1 0)) -(let (?e356 (- ?e158 ?e151)) -(let (?e357 (ite (p0 ?e296) 1 0)) -(let (?e358 (- ?e166 ?e9)) -(let (?e359 (~ ?e195)) -(let (?e360 (+ ?e148 ?e200)) -(let (?e361 (- ?e186 ?e162)) -(let (?e362 (- ?e192 ?e136)) -(let (?e363 (- ?e167 ?e301)) -(let (?e364 (ite (p0 ?e13) 1 0)) -(let (?e365 (ite (p0 ?e282) 1 0)) -(let (?e366 (* (~ ?e3) ?e8)) -(let (?e367 (- ?e342 ?e360)) -(let (?e368 (- ?e181 ?e4)) -(let (?e369 (* ?e3 ?e188)) -(let (?e370 (- ?e171 ?e146)) -(let (?e371 (* ?e293 (~ ?e2))) -(let (?e372 (* (~ ?e2) ?e187)) -(flet ($e373 (p1 ?e101)) -(flet ($e374 (p1 ?e247)) -(flet ($e375 (p1 ?e270)) -(flet ($e376 (p1 ?e125)) -(flet ($e377 (p1 ?e235)) -(flet ($e378 (p1 ?e254)) -(flet ($e379 (p1 ?e214)) -(flet ($e380 (p1 ?e111)) -(flet ($e381 (p1 ?e112)) -(flet ($e382 (p1 ?e239)) -(flet ($e383 (p1 ?e110)) -(flet ($e384 (p1 ?e212)) -(flet ($e385 (p1 ?e75)) -(flet ($e386 (p1 ?e261)) -(flet ($e387 (p1 ?e258)) -(flet ($e388 (p1 ?e223)) -(flet ($e389 (p1 ?e124)) -(flet ($e390 (p1 ?e209)) -(flet ($e391 (p1 ?e120)) -(flet ($e392 (p1 ?e89)) -(flet ($e393 (p1 ?e207)) -(flet ($e394 (p1 ?e90)) -(flet ($e395 (p1 ?e81)) -(flet ($e396 (p1 ?e204)) -(flet ($e397 (p1 ?e94)) -(flet ($e398 (p1 ?e125)) -(flet ($e399 (p1 ?e230)) -(flet ($e400 (p1 ?e132)) -(flet ($e401 (p1 ?e93)) -(flet ($e402 (p1 ?e266)) -(flet ($e403 (p1 ?e79)) -(flet ($e404 (p1 ?e92)) -(flet ($e405 (p1 ?e241)) -(flet ($e406 (p1 ?e70)) -(flet ($e407 (p1 ?e95)) -(flet ($e408 (p1 ?e250)) -(flet ($e409 (p1 ?e110)) -(flet ($e410 (p1 ?e267)) -(flet ($e411 (p1 ?e234)) -(flet ($e412 (p1 ?e248)) -(flet ($e413 (p1 ?e98)) -(flet ($e414 (p1 ?e133)) -(flet ($e415 (p1 ?e128)) -(flet ($e416 (p1 ?e84)) -(flet ($e417 (p1 ?e83)) -(flet ($e418 (p1 ?e77)) -(flet ($e419 (p1 ?e251)) -(flet ($e420 (p1 ?e21)) -(flet ($e421 (p1 ?e263)) -(flet ($e422 (p1 ?e114)) -(flet ($e423 (p1 ?e19)) -(flet ($e424 (p1 ?e229)) -(flet ($e425 (p1 ?e242)) -(flet ($e426 (p1 ?e209)) -(flet ($e427 (p1 ?e221)) -(flet ($e428 (p1 ?e78)) -(flet ($e429 (p1 ?e70)) -(flet ($e430 (p1 ?e264)) -(flet ($e431 (p1 ?e224)) -(flet ($e432 (p1 ?e20)) -(flet ($e433 (p1 ?e246)) -(flet ($e434 (p1 ?e90)) -(flet ($e435 (p1 ?e90)) -(flet ($e436 (p1 ?e129)) -(flet ($e437 (p1 ?e129)) -(flet ($e438 (p1 ?e247)) -(flet ($e439 (p1 ?e252)) -(flet ($e440 (p1 ?e255)) -(flet ($e441 (p1 ?e106)) -(flet ($e442 (p1 ?e228)) -(flet ($e443 (p1 ?e242)) -(flet ($e444 (p1 ?e108)) -(flet ($e445 (p1 ?e86)) -(flet ($e446 (p1 ?e88)) -(flet ($e447 (p1 ?e238)) -(flet ($e448 (p1 ?e233)) -(flet ($e449 (p1 ?e241)) -(flet ($e450 (p1 ?e255)) -(flet ($e451 (p1 ?e74)) -(flet ($e452 (p1 ?e95)) -(flet ($e453 (p1 ?e103)) -(flet ($e454 (p1 ?e130)) -(flet ($e455 (p1 ?e269)) -(flet ($e456 (p1 ?e240)) -(flet ($e457 (p1 ?e117)) -(flet ($e458 (p1 ?e241)) -(flet ($e459 (p1 ?e127)) -(flet ($e460 (p1 ?e232)) -(flet ($e461 (p1 ?e73)) -(flet ($e462 (p1 ?e253)) -(flet ($e463 (p1 ?e268)) -(flet ($e464 (p1 ?e133)) -(flet ($e465 (p1 ?e101)) -(flet ($e466 (p1 ?e216)) -(flet ($e467 (p1 ?e72)) -(flet ($e468 (p1 ?e118)) -(flet ($e469 (p1 ?e109)) -(flet ($e470 (p1 ?e123)) -(flet ($e471 (p1 ?e71)) -(flet ($e472 (p1 ?e103)) -(flet ($e473 (p1 ?e111)) -(flet ($e474 (p1 ?e215)) -(flet ($e475 (p1 ?e102)) -(flet ($e476 (p1 ?e260)) -(flet ($e477 (p1 ?e107)) -(flet ($e478 (p1 ?e244)) -(flet ($e479 (p1 ?e87)) -(flet ($e480 (p1 ?e18)) -(flet ($e481 (p1 ?e88)) -(flet ($e482 (p1 ?e208)) -(flet ($e483 (p1 ?e84)) -(flet ($e484 (p1 ?e217)) -(flet ($e485 (p1 ?e233)) -(flet ($e486 (p1 ?e265)) -(flet ($e487 (p1 ?e100)) -(flet ($e488 (p1 ?e210)) -(flet ($e489 (p1 ?e242)) -(flet ($e490 (p1 ?e214)) -(flet ($e491 (p1 ?e230)) -(flet ($e492 (p1 ?e116)) -(flet ($e493 (p1 ?e104)) -(flet ($e494 (p1 ?e80)) -(flet ($e495 (p1 ?e203)) -(flet ($e496 (p1 ?e76)) -(flet ($e497 (p1 ?e271)) -(flet ($e498 (p1 v1)) -(flet ($e499 (p1 ?e106)) -(flet ($e500 (p1 ?e204)) -(flet ($e501 (p1 ?e113)) -(flet ($e502 (p1 ?e262)) -(flet ($e503 (p1 ?e105)) -(flet ($e504 (p1 ?e225)) -(flet ($e505 (p1 ?e131)) -(flet ($e506 (p1 ?e121)) -(flet ($e507 (p1 ?e119)) -(flet ($e508 (p1 ?e248)) -(flet ($e509 (p1 ?e219)) -(flet ($e510 (p1 ?e71)) -(flet ($e511 (p1 ?e96)) -(flet ($e512 (p1 ?e74)) -(flet ($e513 (p1 ?e270)) -(flet ($e514 (p1 ?e211)) -(flet ($e515 (p1 ?e236)) -(flet ($e516 (p1 ?e82)) -(flet ($e517 (p1 ?e229)) -(flet ($e518 (p1 ?e85)) -(flet ($e519 (p1 ?e122)) -(flet ($e520 (p1 ?e243)) -(flet ($e521 (p1 ?e97)) -(flet ($e522 (p1 ?e96)) -(flet ($e523 (p1 ?e231)) -(flet ($e524 (p1 ?e234)) -(flet ($e525 (p1 ?e112)) -(flet ($e526 (p1 ?e259)) -(flet ($e527 (p1 ?e213)) -(flet ($e528 (p1 v1)) -(flet ($e529 (p1 ?e206)) -(flet ($e530 (p1 ?e222)) -(flet ($e531 (p1 ?e249)) -(flet ($e532 (p1 ?e218)) -(flet ($e533 (p1 ?e256)) -(flet ($e534 (p1 ?e220)) -(flet ($e535 (p1 ?e264)) -(flet ($e536 (p1 ?e246)) -(flet ($e537 (p1 ?e94)) -(flet ($e538 (p1 ?e125)) -(flet ($e539 (p1 ?e18)) -(flet ($e540 (p1 ?e119)) -(flet ($e541 (p1 ?e127)) -(flet ($e542 (p1 ?e99)) -(flet ($e543 (p1 ?e126)) -(flet ($e544 (p1 ?e263)) -(flet ($e545 (p1 ?e78)) -(flet ($e546 (p1 ?e257)) -(flet ($e547 (p1 ?e81)) -(flet ($e548 (p1 ?e76)) -(flet ($e549 (p1 ?e115)) -(flet ($e550 (p1 ?e96)) -(flet ($e551 (p1 ?e99)) -(flet ($e552 (p1 ?e265)) -(flet ($e553 (p1 ?e237)) -(flet ($e554 (p1 ?e226)) -(flet ($e555 (p1 ?e244)) -(flet ($e556 (p1 ?e91)) -(flet ($e557 (p1 ?e245)) -(flet ($e558 (p1 ?e72)) -(flet ($e559 (p1 ?e130)) -(flet ($e560 (p1 ?e219)) -(flet ($e561 (p1 ?e227)) -(flet ($e562 (p0 ?e8)) -(flet ($e563 (>= ?e162 ?e164)) -(flet ($e564 (>= ?e346 ?e289)) -(flet ($e565 (< ?e317 ?e287)) -(flet ($e566 (<= ?e16 ?e363)) -(flet ($e567 (distinct ?e357 ?e317)) -(flet ($e568 (>= ?e294 ?e141)) -(flet ($e569 (> ?e358 ?e10)) -(flet ($e570 (= ?e12 ?e328)) -(flet ($e571 (> ?e301 ?e307)) -(flet ($e572 (< ?e280 ?e321)) -(flet ($e573 (p0 ?e153)) -(flet ($e574 (< ?e137 ?e315)) -(flet ($e575 (distinct ?e370 ?e200)) -(flet ($e576 (> ?e350 ?e202)) -(flet ($e577 (> ?e165 ?e298)) -(flet ($e578 (distinct ?e178 ?e282)) -(flet ($e579 (<= ?e201 ?e338)) -(flet ($e580 (distinct ?e324 ?e158)) -(flet ($e581 (= ?e9 ?e14)) -(flet ($e582 (>= ?e281 ?e359)) -(flet ($e583 (< ?e329 ?e175)) -(flet ($e584 (< ?e311 ?e325)) -(flet ($e585 (>= ?e188 ?e146)) -(flet ($e586 (= ?e174 ?e17)) -(flet ($e587 (distinct ?e277 ?e279)) -(flet ($e588 (< ?e294 ?e295)) -(flet ($e589 (= ?e361 ?e369)) -(flet ($e590 (<= ?e347 ?e277)) -(flet ($e591 (<= ?e277 ?e163)) -(flet ($e592 (> ?e157 ?e332)) -(flet ($e593 (>= ?e320 ?e320)) -(flet ($e594 (distinct ?e364 ?e332)) -(flet ($e595 (<= ?e349 ?e184)) -(flet ($e596 (distinct ?e284 ?e195)) -(flet ($e597 (> ?e301 ?e335)) -(flet ($e598 (<= ?e205 ?e156)) -(flet ($e599 (<= ?e136 ?e345)) -(flet ($e600 (<= ?e354 ?e357)) -(flet ($e601 (< ?e339 ?e282)) -(flet ($e602 (< ?e341 ?e135)) -(flet ($e603 (< ?e7 ?e289)) -(flet ($e604 (p0 ?e364)) -(flet ($e605 (p0 ?e187)) -(flet ($e606 (distinct ?e149 ?e319)) -(flet ($e607 (p0 ?e297)) -(flet ($e608 (= ?e151 ?e9)) -(flet ($e609 (< ?e367 ?e148)) -(flet ($e610 (= ?e287 ?e13)) -(flet ($e611 (= ?e168 ?e278)) -(flet ($e612 (< ?e345 ?e290)) -(flet ($e613 (p0 ?e196)) -(flet ($e614 (p0 ?e313)) -(flet ($e615 (<= ?e305 ?e149)) -(flet ($e616 (>= ?e372 ?e330)) -(flet ($e617 (distinct ?e366 ?e341)) -(flet ($e618 (= ?e344 ?e329)) -(flet ($e619 (<= ?e145 ?e310)) -(flet ($e620 (> ?e140 ?e367)) -(flet ($e621 (> ?e191 ?e196)) -(flet ($e622 (> ?e323 ?e326)) -(flet ($e623 (< ?e181 ?e190)) -(flet ($e624 (< ?e273 ?e139)) -(flet ($e625 (= ?e316 ?e361)) -(flet ($e626 (> ?e346 ?e154)) -(flet ($e627 (< ?e332 ?e304)) -(flet ($e628 (p0 ?e300)) -(flet ($e629 (<= ?e302 ?e359)) -(flet ($e630 (<= ?e357 ?e341)) -(flet ($e631 (p0 ?e337)) -(flet ($e632 (>= ?e318 ?e143)) -(flet ($e633 (= ?e173 ?e338)) -(flet ($e634 (= ?e11 ?e359)) -(flet ($e635 (<= ?e276 ?e10)) -(flet ($e636 (<= ?e333 ?e290)) -(flet ($e637 (<= ?e286 ?e293)) -(flet ($e638 (< ?e150 ?e173)) -(flet ($e639 (distinct ?e306 ?e153)) -(flet ($e640 (>= ?e272 ?e176)) -(flet ($e641 (distinct ?e343 ?e346)) -(flet ($e642 (distinct ?e371 ?e283)) -(flet ($e643 (distinct v0 ?e365)) -(flet ($e644 (= ?e312 ?e317)) -(flet ($e645 (<= ?e134 ?e151)) -(flet ($e646 (> ?e322 ?e189)) -(flet ($e647 (p0 ?e356)) -(flet ($e648 (>= ?e166 ?e341)) -(flet ($e649 (< ?e342 ?e313)) -(flet ($e650 (p0 ?e336)) -(flet ($e651 (= ?e187 ?e10)) -(flet ($e652 (distinct ?e362 ?e195)) -(flet ($e653 (>= ?e167 ?e305)) -(flet ($e654 (< ?e170 ?e288)) -(flet ($e655 (distinct ?e161 ?e166)) -(flet ($e656 (< ?e299 ?e283)) -(flet ($e657 (p0 ?e327)) -(flet ($e658 (= ?e340 ?e9)) -(flet ($e659 (p0 ?e340)) -(flet ($e660 (<= ?e177 ?e330)) -(flet ($e661 (distinct ?e205 ?e12)) -(flet ($e662 (distinct ?e339 ?e8)) -(flet ($e663 (= ?e330 ?e311)) -(flet ($e664 (p0 ?e171)) -(flet ($e665 (= ?e5 ?e161)) -(flet ($e666 (< ?e136 ?e277)) -(flet ($e667 (p0 ?e15)) -(flet ($e668 (p0 ?e168)) -(flet ($e669 (= ?e334 ?e328)) -(flet ($e670 (p0 ?e367)) -(flet ($e671 (<= ?e342 ?e6)) -(flet ($e672 (distinct ?e306 ?e14)) -(flet ($e673 (<= ?e274 ?e320)) -(flet ($e674 (> ?e171 ?e173)) -(flet ($e675 (distinct ?e365 ?e5)) -(flet ($e676 (distinct ?e327 ?e351)) -(flet ($e677 (distinct ?e16 ?e277)) -(flet ($e678 (= ?e361 ?e371)) -(flet ($e679 (>= ?e179 ?e319)) -(flet ($e680 (>= ?e188 ?e303)) -(flet ($e681 (p0 ?e161)) -(flet ($e682 (> ?e353 ?e354)) -(flet ($e683 (> ?e142 ?e337)) -(flet ($e684 (< ?e159 ?e281)) -(flet ($e685 (>= ?e306 ?e183)) -(flet ($e686 (>= ?e198 ?e143)) -(flet ($e687 (= ?e285 ?e194)) -(flet ($e688 (= ?e138 ?e273)) -(flet ($e689 (<= ?e172 ?e290)) -(flet ($e690 (< ?e16 ?e12)) -(flet ($e691 (= ?e368 ?e287)) -(flet ($e692 (>= ?e340 ?e308)) -(flet ($e693 (= ?e194 ?e370)) -(flet ($e694 (distinct ?e296 ?e198)) -(flet ($e695 (= ?e4 ?e139)) -(flet ($e696 (> ?e275 ?e296)) -(flet ($e697 (p0 ?e352)) -(flet ($e698 (= ?e205 ?e138)) -(flet ($e699 (>= ?e331 ?e308)) -(flet ($e700 (>= ?e147 ?e287)) -(flet ($e701 (p0 ?e306)) -(flet ($e702 (> ?e348 ?e344)) -(flet ($e703 (>= ?e169 ?e353)) -(flet ($e704 (<= ?e180 ?e337)) -(flet ($e705 (< ?e287 ?e301)) -(flet ($e706 (> ?e360 ?e309)) -(flet ($e707 (distinct ?e184 ?e17)) -(flet ($e708 (>= ?e173 ?e153)) -(flet ($e709 (> ?e339 ?e14)) -(flet ($e710 (> ?e370 ?e327)) -(flet ($e711 (distinct ?e368 ?e301)) -(flet ($e712 (< ?e160 ?e279)) -(flet ($e713 (distinct ?e163 ?e5)) -(flet ($e714 (>= ?e356 ?e156)) -(flet ($e715 (< ?e192 ?e176)) -(flet ($e716 (distinct ?e302 ?e140)) -(flet ($e717 (> ?e300 ?e355)) -(flet ($e718 (<= ?e291 ?e324)) -(flet ($e719 (p0 ?e314)) -(flet ($e720 (>= ?e199 ?e369)) -(flet ($e721 (= ?e274 ?e364)) -(flet ($e722 (p0 ?e205)) -(flet ($e723 (distinct ?e317 ?e10)) -(flet ($e724 (> ?e155 ?e169)) -(flet ($e725 (>= ?e182 ?e280)) -(flet ($e726 (>= ?e292 ?e331)) -(flet ($e727 (p0 ?e193)) -(flet ($e728 (< ?e190 ?e366)) -(flet ($e729 (<= ?e179 ?e324)) -(flet ($e730 (> ?e289 ?e4)) -(flet ($e731 (>= ?e186 ?e283)) -(flet ($e732 (<= ?e185 ?e339)) -(flet ($e733 (<= ?e308 ?e365)) -(flet ($e734 (> ?e317 ?e367)) -(flet ($e735 (p0 v0)) -(flet ($e736 (>= ?e300 ?e288)) -(flet ($e737 (>= ?e317 ?e192)) -(flet ($e738 (distinct ?e187 ?e190)) -(flet ($e739 (> ?e272 ?e189)) -(flet ($e740 (> ?e152 ?e159)) -(flet ($e741 (<= ?e274 ?e179)) -(flet ($e742 (< ?e304 ?e281)) -(flet ($e743 (p0 ?e135)) -(flet ($e744 (>= ?e366 ?e156)) -(flet ($e745 (<= ?e197 ?e338)) -(flet ($e746 (distinct ?e349 ?e339)) -(flet ($e747 (distinct ?e284 ?e167)) -(flet ($e748 (= ?e144 ?e134)) -(flet ($e749 (not $e411)) -(flet ($e750 (xor $e519 $e498)) -(flet ($e751 (implies $e639 $e39)) -(flet ($e752 (or $e60 $e590)) -(flet ($e753 (or $e644 $e62)) -(flet ($e754 (or $e447 $e683)) -(flet ($e755 (if_then_else $e712 $e387 $e26)) -(flet ($e756 (implies $e727 $e661)) -(flet ($e757 (if_then_else $e653 $e749 $e31)) -(flet ($e758 (implies $e757 $e607)) -(flet ($e759 (not $e591)) -(flet ($e760 (or $e725 $e677)) -(flet ($e761 (xor $e614 $e461)) -(flet ($e762 (and $e500 $e713)) -(flet ($e763 (iff $e584 $e656)) -(flet ($e764 (implies $e422 $e487)) -(flet ($e765 (if_then_else $e420 $e423 $e692)) -(flet ($e766 (xor $e27 $e480)) -(flet ($e767 (or $e602 $e43)) -(flet ($e768 (or $e723 $e453)) -(flet ($e769 (not $e389)) -(flet ($e770 (and $e600 $e391)) -(flet ($e771 (and $e493 $e706)) -(flet ($e772 (implies $e716 $e655)) -(flet ($e773 (not $e633)) -(flet ($e774 (iff $e528 $e22)) -(flet ($e775 (if_then_else $e431 $e474 $e507)) -(flet ($e776 (implies $e437 $e388)) -(flet ($e777 (if_then_else $e45 $e593 $e440)) -(flet ($e778 (implies $e703 $e549)) -(flet ($e779 (xor $e581 $e574)) -(flet ($e780 (xor $e401 $e38)) -(flet ($e781 (not $e646)) -(flet ($e782 (iff $e376 $e729)) -(flet ($e783 (if_then_else $e777 $e451 $e696)) -(flet ($e784 (and $e565 $e627)) -(flet ($e785 (implies $e415 $e617)) -(flet ($e786 (if_then_else $e746 $e785 $e408)) -(flet ($e787 (or $e648 $e414)) -(flet ($e788 (and $e527 $e473)) -(flet ($e789 (xor $e66 $e709)) -(flet ($e790 (and $e564 $e479)) -(flet ($e791 (xor $e448 $e520)) -(flet ($e792 (if_then_else $e702 $e385 $e413)) -(flet ($e793 (or $e611 $e46)) -(flet ($e794 (implies $e485 $e418)) -(flet ($e795 (and $e542 $e396)) -(flet ($e796 (or $e454 $e740)) -(flet ($e797 (iff $e782 $e640)) -(flet ($e798 (xor $e658 $e637)) -(flet ($e799 (and $e753 $e626)) -(flet ($e800 (or $e442 $e523)) -(flet ($e801 (implies $e642 $e776)) -(flet ($e802 (implies $e625 $e524)) -(flet ($e803 (if_then_else $e559 $e596 $e790)) -(flet ($e804 (xor $e750 $e50)) -(flet ($e805 (not $e463)) -(flet ($e806 (not $e651)) -(flet ($e807 (or $e419 $e674)) -(flet ($e808 (implies $e622 $e435)) -(flet ($e809 (if_then_else $e700 $e405 $e689)) -(flet ($e810 (iff $e583 $e34)) -(flet ($e811 (iff $e561 $e707)) -(flet ($e812 (implies $e562 $e735)) -(flet ($e813 (not $e58)) -(flet ($e814 (iff $e481 $e615)) -(flet ($e815 (not $e450)) -(flet ($e816 (and $e813 $e638)) -(flet ($e817 (and $e695 $e536)) -(flet ($e818 (and $e477 $e569)) -(flet ($e819 (iff $e784 $e478)) -(flet ($e820 (not $e384)) -(flet ($e821 (implies $e510 $e508)) -(flet ($e822 (iff $e526 $e56)) -(flet ($e823 (not $e634)) -(flet ($e824 (iff $e531 $e538)) -(flet ($e825 (or $e787 $e445)) -(flet ($e826 (iff $e63 $e578)) -(flet ($e827 (and $e496 $e618)) -(flet ($e828 (or $e662 $e613)) -(flet ($e829 (iff $e601 $e25)) -(flet ($e830 (not $e691)) -(flet ($e831 (not $e530)) -(flet ($e832 (and $e654 $e570)) -(flet ($e833 (or $e754 $e802)) -(flet ($e834 (and $e551 $e717)) -(flet ($e835 (xor $e53 $e586)) -(flet ($e836 (implies $e763 $e64)) -(flet ($e837 (iff $e760 $e766)) -(flet ($e838 (if_then_else $e805 $e444 $e395)) -(flet ($e839 (xor $e718 $e816)) -(flet ($e840 (if_then_else $e592 $e57 $e681)) -(flet ($e841 (iff $e379 $e488)) -(flet ($e842 (iff $e775 $e428)) -(flet ($e843 (not $e636)) -(flet ($e844 (and $e623 $e624)) -(flet ($e845 (xor $e409 $e705)) -(flet ($e846 (and $e489 $e557)) -(flet ($e847 (if_then_else $e41 $e460 $e724)) -(flet ($e848 (implies $e779 $e834)) -(flet ($e849 (implies $e769 $e739)) -(flet ($e850 (implies $e686 $e759)) -(flet ($e851 (if_then_else $e483 $e789 $e719)) -(flet ($e852 (not $e641)) -(flet ($e853 (implies $e567 $e803)) -(flet ($e854 (if_then_else $e742 $e378 $e843)) -(flet ($e855 (iff $e434 $e398)) -(flet ($e856 (or $e827 $e400)) -(flet ($e857 (xor $e563 $e687)) -(flet ($e858 (implies $e33 $e744)) -(flet ($e859 (implies $e793 $e455)) -(flet ($e860 (iff $e539 $e823)) -(flet ($e861 (or $e61 $e443)) -(flet ($e862 (and $e425 $e629)) -(flet ($e863 (not $e585)) -(flet ($e864 (not $e664)) -(flet ($e865 (and $e678 $e669)) -(flet ($e866 (or $e30 $e667)) -(flet ($e867 (or $e647 $e861)) -(flet ($e868 (xor $e35 $e492)) -(flet ($e869 (or $e577 $e685)) -(flet ($e870 (if_then_else $e393 $e51 $e69)) -(flet ($e871 (or $e711 $e589)) -(flet ($e872 (or $e466 $e863)) -(flet ($e873 (and $e44 $e858)) -(flet ($e874 (implies $e786 $e798)) -(flet ($e875 (implies $e558 $e844)) -(flet ($e876 (or $e441 $e649)) -(flet ($e877 (implies $e36 $e518)) -(flet ($e878 (xor $e751 $e675)) -(flet ($e879 (xor $e575 $e682)) -(flet ($e880 (iff $e821 $e801)) -(flet ($e881 (not $e791)) -(flet ($e882 (not $e394)) -(flet ($e883 (and $e630 $e459)) -(flet ($e884 (iff $e877 $e40)) -(flet ($e885 (if_then_else $e495 $e399 $e374)) -(flet ($e886 (or $e869 $e29)) -(flet ($e887 (iff $e486 $e845)) -(flet ($e888 (iff $e738 $e603)) -(flet ($e889 (xor $e521 $e566)) -(flet ($e890 (xor $e604 $e814)) -(flet ($e891 (if_then_else $e694 $e541 $e535)) -(flet ($e892 (and $e554 $e732)) -(flet ($e893 (implies $e880 $e822)) -(flet ($e894 (implies $e668 $e870)) -(flet ($e895 (if_then_else $e795 $e672 $e470)) -(flet ($e896 (implies $e806 $e560)) -(flet ($e897 (implies $e893 $e841)) -(flet ($e898 (if_then_else $e812 $e835 $e887)) -(flet ($e899 (or $e842 $e576)) -(flet ($e900 (not $e676)) -(flet ($e901 (or $e878 $e768)) -(flet ($e902 (and $e726 $e889)) -(flet ($e903 (not $e587)) -(flet ($e904 (and $e375 $e652)) -(flet ($e905 (implies $e874 $e761)) -(flet ($e906 (not $e469)) -(flet ($e907 (xor $e728 $e888)) -(flet ($e908 (if_then_else $e547 $e458 $e905)) -(flet ($e909 (not $e848)) -(flet ($e910 (xor $e810 $e799)) -(flet ($e911 (not $e553)) -(flet ($e912 (if_then_else $e612 $e772 $e433)) -(flet ($e913 (and $e745 $e872)) -(flet ($e914 (xor $e688 $e882)) -(flet ($e915 (xor $e421 $e780)) -(flet ($e916 (implies $e714 $e693)) -(flet ($e917 (implies $e424 $e467)) -(flet ($e918 (or $e770 $e482)) -(flet ($e919 (if_then_else $e765 $e839 $e608)) -(flet ($e920 (implies $e494 $e430)) -(flet ($e921 (and $e620 $e873)) -(flet ($e922 (if_then_else $e901 $e833 $e511)) -(flet ($e923 (and $e643 $e800)) -(flet ($e924 (xor $e912 $e820)) -(flet ($e925 (iff $e49 $e23)) -(flet ($e926 (iff $e830 $e914)) -(flet ($e927 (xor $e919 $e32)) -(flet ($e928 (implies $e859 $e853)) -(flet ($e929 (or $e771 $e406)) -(flet ($e930 (and $e824 $e514)) -(flet ($e931 (if_then_else $e509 $e548 $e851)) -(flet ($e932 (or $e865 $e606)) -(flet ($e933 (not $e47)) -(flet ($e934 (if_then_else $e571 $e894 $e657)) -(flet ($e935 (implies $e891 $e758)) -(flet ($e936 (or $e502 $e532)) -(flet ($e937 (and $e619 $e831)) -(flet ($e938 (or $e529 $e794)) -(flet ($e939 (and $e819 $e807)) -(flet ($e940 (if_then_else $e383 $e24 $e896)) -(flet ($e941 (iff $e934 $e934)) -(flet ($e942 (implies $e417 $e402)) -(flet ($e943 (implies $e426 $e412)) -(flet ($e944 (not $e849)) -(flet ($e945 (or $e941 $e499)) -(flet ($e946 (if_then_else $e631 $e895 $e663)) -(flet ($e947 (iff $e928 $e403)) -(flet ($e948 (and $e826 $e730)) -(flet ($e949 (not $e397)) -(flet ($e950 (implies $e390 $e710)) -(flet ($e951 (iff $e932 $e920)) -(flet ($e952 (not $e52)) -(flet ($e953 (or $e862 $e28)) -(flet ($e954 (if_then_else $e597 $e599 $e762)) -(flet ($e955 (implies $e54 $e946)) -(flet ($e956 (or $e513 $e755)) -(flet ($e957 (if_then_else $e505 $e955 $e809)) -(flet ($e958 (if_then_else $e884 $e792 $e927)) -(flet ($e959 (and $e540 $e438)) -(flet ($e960 (or $e909 $e462)) -(flet ($e961 (and $e491 $e860)) -(flet ($e962 (xor $e943 $e788)) -(flet ($e963 (xor $e736 $e55)) -(flet ($e964 (iff $e825 $e864)) -(flet ($e965 (if_then_else $e933 $e846 $e582)) -(flet ($e966 (implies $e836 $e452)) -(flet ($e967 (implies $e796 $e811)) -(flet ($e968 (and $e867 $e818)) -(flet ($e969 (iff $e944 $e621)) -(flet ($e970 (or $e650 $e721)) -(flet ($e971 (if_then_else $e381 $e690 $e773)) -(flet ($e972 (implies $e947 $e950)) -(flet ($e973 (and $e948 $e898)) -(flet ($e974 (implies $e840 $e490)) -(flet ($e975 (if_then_else $e537 $e465 $e949)) -(flet ($e976 (and $e924 $e446)) -(flet ($e977 (and $e572 $e525)) -(flet ($e978 (xor $e817 $e464)) -(flet ($e979 (implies $e883 $e722)) -(flet ($e980 (implies $e545 $e767)) -(flet ($e981 (and $e48 $e966)) -(flet ($e982 (not $e890)) -(flet ($e983 (if_then_else $e456 $e876 $e837)) -(flet ($e984 (not $e962)) -(flet ($e985 (and $e808 $e930)) -(flet ($e986 (not $e850)) -(flet ($e987 (xor $e377 $e472)) -(flet ($e988 (if_then_else $e973 $e904 $e980)) -(flet ($e989 (xor $e940 $e847)) -(flet ($e990 (if_then_else $e911 $e902 $e942)) -(flet ($e991 (if_then_else $e449 $e982 $e915)) -(flet ($e992 (xor $e580 $e987)) -(flet ($e993 (xor $e938 $e737)) -(flet ($e994 (implies $e953 $e954)) -(flet ($e995 (xor $e879 $e734)) -(flet ($e996 (if_then_else $e522 $e990 $e937)) -(flet ($e997 (or $e609 $e989)) -(flet ($e998 (not $e436)) -(flet ($e999 (if_then_else $e957 $e429 $e854)) -(flet ($e1000 (implies $e543 $e684)) -(flet ($e1001 (and $e984 $e715)) -(flet ($e1002 (or $e829 $e720)) -(flet ($e1003 (implies $e951 $e503)) -(flet ($e1004 (xor $e704 $e958)) -(flet ($e1005 (if_then_else $e42 $e908 $e988)) -(flet ($e1006 (or $e515 $e382)) -(flet ($e1007 (xor $e963 $e594)) -(flet ($e1008 (implies $e59 $e632)) -(flet ($e1009 (or $e568 $e517)) -(flet ($e1010 (xor $e504 $e991)) -(flet ($e1011 (and $e1002 $e556)) -(flet ($e1012 (if_then_else $e598 $e670 $e971)) -(flet ($e1013 (iff $e981 $e857)) -(flet ($e1014 (or $e929 $e986)) -(flet ($e1015 (not $e595)) -(flet ($e1016 (iff $e555 $e68)) -(flet ($e1017 (or $e918 $e960)) -(flet ($e1018 (iff $e856 $e939)) -(flet ($e1019 (implies $e497 $e665)) -(flet ($e1020 (implies $e921 $e906)) -(flet ($e1021 (xor $e897 $e969)) -(flet ($e1022 (and $e380 $e475)) -(flet ($e1023 (xor $e468 $e868)) -(flet ($e1024 (not $e903)) -(flet ($e1025 (not $e1007)) -(flet ($e1026 (or $e783 $e756)) -(flet ($e1027 (and $e733 $e512)) -(flet ($e1028 (not $e832)) -(flet ($e1029 (if_then_else $e1020 $e1028 $e610)) -(flet ($e1030 (xor $e731 $e673)) -(flet ($e1031 (not $e995)) -(flet ($e1032 (or $e1003 $e952)) -(flet ($e1033 (or $e1011 $e959)) -(flet ($e1034 (and $e1000 $e1013)) -(flet ($e1035 (and $e1016 $e427)) -(flet ($e1036 (xor $e985 $e534)) -(flet ($e1037 (and $e1010 $e881)) -(flet ($e1038 (xor $e1035 $e546)) -(flet ($e1039 (and $e1036 $e922)) -(flet ($e1040 (or $e855 $e506)) -(flet ($e1041 (if_then_else $e774 $e1008 $e925)) -(flet ($e1042 (implies $e975 $e752)) -(flet ($e1043 (and $e1034 $e907)) -(flet ($e1044 (or $e679 $e797)) -(flet ($e1045 (iff $e533 $e471)) -(flet ($e1046 (if_then_else $e993 $e645 $e605)) -(flet ($e1047 (implies $e67 $e1006)) -(flet ($e1048 (implies $e968 $e994)) -(flet ($e1049 (not $e579)) -(flet ($e1050 (if_then_else $e1005 $e1027 $e956)) -(flet ($e1051 (iff $e476 $e628)) -(flet ($e1052 (if_then_else $e926 $e1017 $e871)) -(flet ($e1053 (or $e936 $e1025)) -(flet ($e1054 (implies $e983 $e1053)) -(flet ($e1055 (implies $e977 $e978)) -(flet ($e1056 (iff $e588 $e698)) -(flet ($e1057 (or $e1019 $e999)) -(flet ($e1058 (and $e917 $e931)) -(flet ($e1059 (and $e972 $e432)) -(flet ($e1060 (xor $e979 $e457)) -(flet ($e1061 (and $e1018 $e923)) -(flet ($e1062 (if_then_else $e516 $e1047 $e708)) -(flet ($e1063 (not $e1050)) -(flet ($e1064 (and $e1048 $e886)) -(flet ($e1065 (implies $e815 $e815)) -(flet ($e1066 (iff $e1044 $e741)) -(flet ($e1067 (xor $e974 $e945)) -(flet ($e1068 (if_then_else $e1022 $e660 $e1056)) -(flet ($e1069 (if_then_else $e996 $e701 $e1049)) -(flet ($e1070 (implies $e1039 $e1059)) -(flet ($e1071 (not $e828)) -(flet ($e1072 (if_then_else $e404 $e550 $e852)) -(flet ($e1073 (and $e1065 $e386)) -(flet ($e1074 (or $e804 $e1040)) -(flet ($e1075 (not $e1057)) -(flet ($e1076 (implies $e1067 $e1033)) -(flet ($e1077 (or $e1068 $e1004)) -(flet ($e1078 (implies $e1072 $e1061)) -(flet ($e1079 (or $e1026 $e1021)) -(flet ($e1080 (xor $e1037 $e910)) -(flet ($e1081 (not $e37)) -(flet ($e1082 (xor $e1030 $e900)) -(flet ($e1083 (not $e671)) -(flet ($e1084 (implies $e666 $e697)) -(flet ($e1085 (and $e961 $e764)) -(flet ($e1086 (or $e1085 $e1063)) -(flet ($e1087 (implies $e892 $e680)) -(flet ($e1088 (iff $e1066 $e1069)) -(flet ($e1089 (or $e416 $e635)) -(flet ($e1090 (and $e1051 $e1080)) -(flet ($e1091 (or $e838 $e1073)) -(flet ($e1092 (iff $e1081 $e1060)) -(flet ($e1093 (or $e1086 $e1014)) -(flet ($e1094 (implies $e373 $e1024)) -(flet ($e1095 (and $e1038 $e1087)) -(flet ($e1096 (iff $e1054 $e573)) -(flet ($e1097 (if_then_else $e778 $e992 $e659)) -(flet ($e1098 (not $e552)) -(flet ($e1099 (xor $e913 $e781)) -(flet ($e1100 (xor $e899 $e998)) -(flet ($e1101 (or $e439 $e1074)) -(flet ($e1102 (xor $e1062 $e699)) -(flet ($e1103 (iff $e1052 $e967)) -(flet ($e1104 (and $e1070 $e935)) -(flet ($e1105 (if_then_else $e1029 $e976 $e976)) -(flet ($e1106 (implies $e1015 $e1090)) -(flet ($e1107 (xor $e1045 $e1084)) -(flet ($e1108 (iff $e1082 $e964)) -(flet ($e1109 (not $e1100)) -(flet ($e1110 (if_then_else $e1023 $e1091 $e1107)) -(flet ($e1111 (or $e743 $e747)) -(flet ($e1112 (implies $e1075 $e1094)) -(flet ($e1113 (if_then_else $e1104 $e1083 $e1103)) -(flet ($e1114 (and $e1076 $e501)) -(flet ($e1115 (iff $e1058 $e1092)) -(flet ($e1116 (xor $e748 $e1055)) -(flet ($e1117 (and $e1112 $e1089)) -(flet ($e1118 (not $e1102)) -(flet ($e1119 (if_then_else $e1116 $e65 $e1096)) -(flet ($e1120 (or $e1041 $e1119)) -(flet ($e1121 (or $e392 $e1109)) -(flet ($e1122 (iff $e1114 $e1106)) -(flet ($e1123 (or $e1078 $e965)) -(flet ($e1124 (or $e875 $e997)) -(flet ($e1125 (and $e407 $e1108)) -(flet ($e1126 (or $e1125 $e1043)) -(flet ($e1127 (iff $e1064 $e1117)) -(flet ($e1128 (iff $e1123 $e1042)) -(flet ($e1129 (xor $e1113 $e1124)) -(flet ($e1130 (and $e484 $e1127)) -(flet ($e1131 (iff $e1130 $e1079)) -(flet ($e1132 (implies $e1111 $e1046)) -(flet ($e1133 (implies $e1132 $e410)) -(flet ($e1134 (xor $e970 $e1071)) -(flet ($e1135 (implies $e1121 $e1122)) -(flet ($e1136 (and $e1120 $e1088)) -(flet ($e1137 (xor $e885 $e1093)) -(flet ($e1138 (or $e916 $e1118)) -(flet ($e1139 (implies $e1095 $e1115)) -(flet ($e1140 (if_then_else $e1098 $e1138 $e1126)) -(flet ($e1141 (xor $e1131 $e1131)) -(flet ($e1142 (not $e1032)) -(flet ($e1143 (and $e1141 $e1001)) -(flet ($e1144 (not $e866)) -(flet ($e1145 (not $e1128)) -(flet ($e1146 (iff $e1031 $e1139)) -(flet ($e1147 (not $e1137)) -(flet ($e1148 (and $e1077 $e1105)) -(flet ($e1149 (not $e1144)) -(flet ($e1150 (if_then_else $e1140 $e1009 $e1145)) -(flet ($e1151 (if_then_else $e1097 $e1143 $e1101)) -(flet ($e1152 (implies $e1134 $e1110)) -(flet ($e1153 (xor $e1142 $e1099)) -(flet ($e1154 (not $e1135)) -(flet ($e1155 (if_then_else $e1147 $e1149 $e1136)) -(flet ($e1156 (or $e1152 $e616)) -(flet ($e1157 (not $e1156)) -(flet ($e1158 (xor $e1148 $e1151)) -(flet ($e1159 (implies $e1153 $e1153)) -(flet ($e1160 (and $e1157 $e1133)) -(flet ($e1161 (or $e1154 $e1159)) -(flet ($e1162 (implies $e1155 $e1160)) -(flet ($e1163 (implies $e1162 $e1161)) -(flet ($e1164 (iff $e1163 $e1163)) -(flet ($e1165 (xor $e1146 $e1129)) -(flet ($e1166 (not $e1012)) -(flet ($e1167 (xor $e544 $e1166)) -(flet ($e1168 (iff $e1165 $e1150)) -(flet ($e1169 (xor $e1164 $e1158)) -(flet ($e1170 (if_then_else $e1167 $e1167 $e1169)) -(flet ($e1171 (not $e1168)) -(flet ($e1172 (and $e1171 $e1171)) -(flet ($e1173 (xor $e1170 $e1170)) -(flet ($e1174 (and $e1173 $e1173)) -(flet ($e1175 (iff $e1174 $e1174)) -(flet ($e1176 (xor $e1175 $e1175)) -(flet ($e1177 (implies $e1172 $e1172)) -(flet ($e1178 (and $e1176 $e1176)) -(flet ($e1179 (not $e1177)) -(flet ($e1180 (xor $e1179 $e1178)) -$e1180 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc deleted file mode 100644 index 62c0dd578..000000000 --- a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXPECT: sat - -DATATYPE RightistTree[T] = - node(left:BOOLEAN, right:RightistTree[T]) | - leaf(data:T) -END; - -x : RightistTree[INT]; - -ASSERT x /= leaf(0); - -CHECKSAT; diff --git a/test/regress/regress0/expect/scrub.04.smt2 b/test/regress/regress0/expect/scrub.04.smt2 deleted file mode 100644 index 1c4bbde2b..000000000 --- a/test/regress/regress0/expect/scrub.04.smt2 +++ /dev/null @@ -1,14 +0,0 @@ -; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. -; EXPECT: The fact in question: TERM -; EXPECT: ") -; EXIT: 1 -(set-logic QF_LRA) -(set-info :status unknown) -(declare-fun n () Real) - -; This example is test that LRA rejects multiplication terms - -(assert (= (/ n n) 1)) - -(check-sat) diff --git a/test/regress/regress0/hung10_itesdk_output2.smt2 b/test/regress/regress0/hung10_itesdk_output2.smt2 deleted file mode 100644 index 8bcdfdfbc..000000000 --- a/test/regress/regress0/hung10_itesdk_output2.smt2 +++ /dev/null @@ -1,30 +0,0 @@ -( set-logic QF_ALL_SUPPORTED) -( set-info :source | SMT-COMP'06 organizers |) -( set-info :smt-lib-version 2.0) -( set-info :category "check") -( set-info :status sat) -( declare-fun x1 () Bool) -( declare-fun x2 () Real) -( declare-fun x3 () Real) -( declare-fun x4 () Bool) -( declare-fun x5 () Real) -( declare-fun x6 () Real) -( declare-fun x7 () Real) -( declare-fun x8 () Real) -( declare-fun bo1 () Bool) -( declare-fun bo2 () Bool) -( declare-fun bo3 () Bool) -( declare-fun r1 () Real) -( declare-fun r2 () Real) -( declare-fun r3 () Real) -( define-fun myBoolIte ( ( a Real) ( b Bool) ( c Bool)) Bool - ( ite ( > a 0.0) b c)) -( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real - ( ite a1 b1 c1)) -( declare-fun f ( Real Bool) Real) -( declare-fun fRealRealReal ( Real Real) Real) -( declare-fun fRealReal ( Real) Real) -( declare-fun fReal () Real) -( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3)))) -(check-sat) -(exit) diff --git a/test/regress/regress0/hung13sdk_output2.smt2 b/test/regress/regress0/hung13sdk_output2.smt2 deleted file mode 100644 index bf3ab9a26..000000000 --- a/test/regress/regress0/hung13sdk_output2.smt2 +++ /dev/null @@ -1,14 +0,0 @@ -( set-logic QF_ALL_SUPPORTED) -( set-info :source | SMT-COMP'06 organizers |) -( set-info :smt-lib-version 2.0) -( set-info :category "check") -( set-info :status sat) -( declare-fun x1 () Bool) -( declare-fun x2 () Real) -( declare-fun x3 () Real) -( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real - ( ite a1 b1 c1)) -( declare-fun fReal () Real) -( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3)))) -(check-sat) -(exit) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 index e05c3446d..537f0ee3d 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 @@ -1,10 +1,10 @@ ; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full -; EXPECT: unsat +; EXPECT: sat (set-logic BV) -(set-info :status unsat) +(set-info :status sat) (declare-fun a () (_ BitVec 8)) (declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b))) +(assert (forall ((x (_ BitVec 8))) (= (bvlshr x a) b))) (check-sat) diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc deleted file mode 100644 index 2b9eedcdb..000000000 --- a/test/regress/regress0/queries0.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% Tests the invariants for multiple queries. -% COMMAND-LINE: --incremental - -a, b: BOOLEAN; - -% EXPECT: valid -QUERY (a AND b) OR NOT (a AND b); - -% EXPECT: invalid -QUERY (a OR b); - |