From: Morgan Deters Date: Mon, 11 Jul 2011 16:38:38 +0000 (+0000) Subject: array benchmarks X-Git-Tag: cvc5-1.0.0~8507 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ae8fae8c1e1de22c2324e5c63c5d7fd73a4582e;p=cvc5.git array benchmarks --- diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 8fdeda04a..2e302f1ee 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -10,7 +10,18 @@ TESTS = \ arrays3.smt2 \ arrays4.smt2 -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + incorrect1.smt \ + incorrect2.smt \ + incorrect3.smt \ + incorrect4.smt \ + incorrect5.smt \ + incorrect6.smt \ + incorrect7.smt \ + incorrect8.smt \ + incorrect9.smt \ + incorrect10.smt \ + incorrect11.smt #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/arrays/incorrect1.smt b/test/regress/regress0/arrays/incorrect1.smt new file mode 100644 index 000000000..03b743373 --- /dev/null +++ b/test/regress/regress0/arrays/incorrect1.smt @@ -0,0 +1,132 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Index)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v4 Element)) +:formula +(flet ($e5 (distinct v0 v0)) +(flet ($e6 (= v3 v2)) +(flet ($e7 (= v1 v2)) +(flet ($e8 (distinct v4 v4)) +(let (?e9 (ite $e6 v0 v0)) +(let (?e10 (ite $e8 ?e9 v0)) +(let (?e11 (ite $e8 ?e9 ?e9)) +(let (?e12 (ite $e7 v0 ?e11)) +(let (?e13 (ite $e5 ?e10 ?e11)) +(let (?e14 (ite $e5 v3 v1)) +(let (?e15 (ite $e8 v2 v2)) +(let (?e16 (ite $e6 v3 v1)) +(let (?e17 (ite $e6 ?e15 ?e15)) +(let (?e18 (ite $e8 ?e17 ?e16)) +(let (?e19 (ite $e8 ?e15 ?e15)) +(let (?e20 (ite $e6 v3 ?e19)) +(let (?e21 (ite $e6 ?e15 ?e18)) +(let (?e22 (ite $e6 v1 ?e20)) +(let (?e23 (ite $e7 v3 ?e15)) +(let (?e24 (ite $e8 v4 v4)) +(let (?e25 (ite $e5 v4 v4)) +(let (?e26 (ite $e6 ?e25 ?e25)) +(let (?e27 (ite $e7 v4 ?e25)) +(let (?e28 (select ?e12 ?e18)) +(flet ($e29 (distinct ?e12 ?e9)) +(flet ($e30 (distinct v0 ?e12)) +(flet ($e31 (distinct ?e9 v0)) +(flet ($e32 (= ?e11 ?e9)) +(flet ($e33 (= ?e11 ?e10)) +(flet ($e34 (= ?e10 v0)) +(flet ($e35 (= ?e11 ?e10)) +(flet ($e36 (= v0 ?e9)) +(flet ($e37 (distinct ?e11 ?e12)) +(flet ($e38 (distinct ?e11 ?e9)) +(flet ($e39 (distinct ?e10 ?e11)) +(flet ($e40 (distinct ?e11 ?e13)) +(flet ($e41 (= ?e14 ?e21)) +(flet ($e42 (distinct ?e19 ?e17)) +(flet ($e43 (= ?e22 ?e21)) +(flet ($e44 (distinct ?e14 ?e18)) +(flet ($e45 (distinct v1 ?e21)) +(flet ($e46 (distinct ?e15 v3)) +(flet ($e47 (= v3 ?e19)) +(flet ($e48 (= ?e21 ?e22)) +(flet ($e49 (distinct ?e16 ?e21)) +(flet ($e50 (distinct ?e18 ?e14)) +(flet ($e51 (= v2 v2)) +(flet ($e52 (= ?e15 ?e22)) +(flet ($e53 (distinct ?e18 ?e21)) +(flet ($e54 (= v1 ?e19)) +(flet ($e55 (distinct ?e19 ?e16)) +(flet ($e56 (= ?e21 v2)) +(flet ($e57 (distinct v2 ?e22)) +(flet ($e58 (distinct ?e19 ?e21)) +(flet ($e59 (= v2 ?e19)) +(flet ($e60 (distinct ?e20 v1)) +(flet ($e61 (distinct ?e19 ?e21)) +(flet ($e62 (= ?e19 ?e16)) +(flet ($e63 (distinct ?e19 ?e19)) +(flet ($e64 (distinct ?e16 v1)) +(flet ($e65 (distinct v2 ?e20)) +(flet ($e66 (distinct ?e18 ?e23)) +(flet ($e67 (distinct ?e25 v4)) +(flet ($e68 (= ?e27 ?e27)) +(flet ($e69 (distinct ?e28 ?e27)) +(flet ($e70 (distinct ?e26 ?e26)) +(flet ($e71 (= ?e28 v4)) +(flet ($e72 (= ?e27 ?e24)) +(flet ($e73 (if_then_else $e29 $e38 $e34)) +(flet ($e74 (iff $e57 $e57)) +(flet ($e75 (iff $e71 $e42)) +(flet ($e76 (xor $e61 $e58)) +(flet ($e77 (and $e39 $e30)) +(flet ($e78 (implies $e63 $e36)) +(flet ($e79 (and $e41 $e52)) +(flet ($e80 (not $e70)) +(flet ($e81 (implies $e8 $e33)) +(flet ($e82 (or $e56 $e65)) +(flet ($e83 (or $e78 $e47)) +(flet ($e84 (if_then_else $e77 $e73 $e77)) +(flet ($e85 (or $e45 $e54)) +(flet ($e86 (or $e80 $e43)) +(flet ($e87 (iff $e6 $e32)) +(flet ($e88 (xor $e44 $e40)) +(flet ($e89 (iff $e66 $e55)) +(flet ($e90 (and $e87 $e84)) +(flet ($e91 (not $e67)) +(flet ($e92 (xor $e79 $e31)) +(flet ($e93 (or $e75 $e72)) +(flet ($e94 (and $e51 $e90)) +(flet ($e95 (and $e60 $e35)) +(flet ($e96 (xor $e68 $e82)) +(flet ($e97 (and $e88 $e89)) +(flet ($e98 (and $e59 $e96)) +(flet ($e99 (and $e93 $e92)) +(flet ($e100 (if_then_else $e86 $e76 $e37)) +(flet ($e101 (if_then_else $e81 $e64 $e97)) +(flet ($e102 (or $e5 $e100)) +(flet ($e103 (if_then_else $e48 $e85 $e99)) +(flet ($e104 (if_then_else $e95 $e69 $e94)) +(flet ($e105 (iff $e50 $e98)) +(flet ($e106 (xor $e62 $e83)) +(flet ($e107 (implies $e104 $e7)) +(flet ($e108 (if_then_else $e103 $e102 $e53)) +(flet ($e109 (iff $e105 $e105)) +(flet ($e110 (implies $e74 $e46)) +(flet ($e111 (not $e106)) +(flet ($e112 (xor $e109 $e101)) +(flet ($e113 (or $e111 $e91)) +(flet ($e114 (if_then_else $e107 $e108 $e108)) +(flet ($e115 (iff $e112 $e113)) +(flet ($e116 (iff $e115 $e115)) +(flet ($e117 (and $e110 $e116)) +(flet ($e118 (and $e114 $e114)) +(flet ($e119 (not $e49)) +(flet ($e120 (or $e118 $e118)) +(flet ($e121 (not $e119)) +(flet ($e122 (and $e117 $e121)) +(flet ($e123 (not $e122)) +(flet ($e124 (and $e120 $e123)) +$e124 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect10.smt b/test/regress/regress0/arrays/incorrect10.smt new file mode 100644 index 000000000..402fcc128 --- /dev/null +++ b/test/regress/regress0/arrays/incorrect10.smt @@ -0,0 +1,275 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Index)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Element)) +:formula +(let (?e4 (store v0 v1 v3)) +(let (?e5 (store ?e4 v2 v3)) +(let (?e6 (select ?e5 v1)) +(let (?e7 (select ?e4 v1)) +(let (?e8 (select ?e4 v1)) +(let (?e9 (store ?e4 v2 ?e8)) +(let (?e10 (select ?e9 v1)) +(let (?e11 (select ?e9 v1)) +(flet ($e12 (= v0 v0)) +(flet ($e13 (distinct ?e5 v0)) +(flet ($e14 (= ?e5 ?e9)) +(flet ($e15 (= v0 v0)) +(flet ($e16 (= ?e5 ?e4)) +(flet ($e17 (= v2 v1)) +(flet ($e18 (= ?e10 ?e11)) +(flet ($e19 (= v3 ?e6)) +(flet ($e20 (= ?e6 ?e8)) +(flet ($e21 (distinct ?e6 ?e11)) +(flet ($e22 (= ?e11 ?e10)) +(flet ($e23 (= ?e7 ?e6)) +(let (?e24 (ite $e18 ?e4 ?e4)) +(let (?e25 (ite $e16 ?e5 ?e24)) +(let (?e26 (ite $e14 v0 ?e4)) +(let (?e27 (ite $e17 ?e9 ?e26)) +(let (?e28 (ite $e22 v0 v0)) +(let (?e29 (ite $e20 ?e28 ?e28)) +(let (?e30 (ite $e21 ?e27 ?e9)) +(let (?e31 (ite $e14 ?e27 ?e4)) +(let (?e32 (ite $e15 ?e27 ?e25)) +(let (?e33 (ite $e13 ?e28 ?e4)) +(let (?e34 (ite $e12 ?e33 ?e27)) +(let (?e35 (ite $e23 ?e25 ?e9)) +(let (?e36 (ite $e14 ?e9 ?e9)) +(let (?e37 (ite $e15 ?e26 ?e5)) +(let (?e38 (ite $e19 ?e26 ?e5)) +(let (?e39 (ite $e15 v1 v2)) +(let (?e40 (ite $e16 v2 ?e39)) +(let (?e41 (ite $e18 ?e40 v1)) +(let (?e42 (ite $e21 ?e39 v2)) +(let (?e43 (ite $e17 v1 ?e39)) +(let (?e44 (ite $e13 v1 v2)) +(let (?e45 (ite $e22 ?e40 ?e42)) +(let (?e46 (ite $e23 ?e41 v2)) +(let (?e47 (ite $e12 ?e41 ?e39)) +(let (?e48 (ite $e19 ?e47 ?e39)) +(let (?e49 (ite $e18 v1 v2)) +(let (?e50 (ite $e14 ?e43 ?e49)) +(let (?e51 (ite $e20 ?e49 ?e46)) +(let (?e52 (ite $e16 v3 v3)) +(let (?e53 (ite $e17 ?e10 v3)) +(let (?e54 (ite $e12 ?e6 ?e8)) +(let (?e55 (ite $e12 ?e11 ?e10)) +(let (?e56 (ite $e13 v3 ?e10)) +(let (?e57 (ite $e15 ?e7 ?e54)) +(let (?e58 (ite $e19 ?e10 ?e55)) +(let (?e59 (ite $e18 ?e52 ?e7)) +(let (?e60 (ite $e23 ?e56 ?e8)) +(let (?e61 (ite $e14 ?e57 ?e59)) +(let (?e62 (ite $e12 ?e55 v3)) +(let (?e63 (ite $e22 ?e52 ?e11)) +(let (?e64 (ite $e13 ?e61 v3)) +(let (?e65 (ite $e20 ?e6 ?e63)) +(let (?e66 (ite $e21 ?e11 ?e63)) +(let (?e67 (store ?e28 ?e41 ?e66)) +(let (?e68 (store v0 ?e42 ?e8)) +(let (?e69 (select ?e27 ?e43)) +(let (?e70 (select ?e35 ?e40)) +(let (?e71 (select ?e28 ?e44)) +(let (?e72 (store ?e25 ?e39 ?e65)) +(let (?e73 (select ?e67 ?e45)) +(let (?e74 (store ?e25 v1 ?e66)) +(let (?e75 (select ?e34 ?e48)) +(flet ($e76 (= ?e37 ?e33)) +(flet ($e77 (distinct ?e34 ?e34)) +(flet ($e78 (= ?e32 ?e30)) +(flet ($e79 (distinct ?e31 ?e74)) +(flet ($e80 (= ?e33 ?e26)) +(flet ($e81 (= ?e31 ?e36)) +(flet ($e82 (distinct ?e34 ?e9)) +(flet ($e83 (distinct ?e9 ?e67)) +(flet ($e84 (= ?e28 ?e27)) +(flet ($e85 (distinct ?e33 ?e33)) +(flet ($e86 (= v0 ?e68)) +(flet ($e87 (distinct ?e29 ?e27)) +(flet ($e88 (distinct ?e72 ?e4)) +(flet ($e89 (distinct ?e37 ?e5)) +(flet ($e90 (= ?e67 ?e38)) +(flet ($e91 (distinct ?e27 ?e67)) +(flet ($e92 (distinct ?e30 ?e25)) +(flet ($e93 (distinct ?e33 ?e38)) +(flet ($e94 (= ?e30 ?e25)) +(flet ($e95 (distinct ?e5 ?e37)) +(flet ($e96 (distinct ?e37 ?e35)) +(flet ($e97 (distinct ?e38 ?e29)) +(flet ($e98 (distinct ?e4 ?e4)) +(flet ($e99 (distinct ?e25 ?e26)) +(flet ($e100 (= ?e32 ?e24)) +(flet ($e101 (= ?e40 ?e46)) +(flet ($e102 (distinct ?e51 ?e47)) +(flet ($e103 (= ?e51 ?e47)) +(flet ($e104 (= ?e46 ?e51)) +(flet ($e105 (= ?e41 ?e41)) +(flet ($e106 (distinct ?e43 ?e41)) +(flet ($e107 (distinct ?e49 ?e42)) +(flet ($e108 (distinct ?e44 ?e46)) +(flet ($e109 (distinct ?e45 ?e49)) +(flet ($e110 (= ?e50 ?e43)) +(flet ($e111 (= ?e51 ?e39)) +(flet ($e112 (= ?e45 ?e47)) +(flet ($e113 (= ?e41 v2)) +(flet ($e114 (= ?e51 ?e50)) +(flet ($e115 (distinct ?e45 ?e46)) +(flet ($e116 (distinct v2 ?e47)) +(flet ($e117 (= ?e45 ?e44)) +(flet ($e118 (distinct ?e41 ?e51)) +(flet ($e119 (= ?e46 ?e49)) +(flet ($e120 (distinct ?e50 ?e41)) +(flet ($e121 (= ?e50 ?e49)) +(flet ($e122 (distinct ?e50 ?e50)) +(flet ($e123 (distinct ?e41 ?e48)) +(flet ($e124 (distinct ?e46 ?e46)) +(flet ($e125 (= ?e39 v1)) +(flet ($e126 (distinct ?e6 ?e71)) +(flet ($e127 (= ?e58 ?e61)) +(flet ($e128 (= ?e7 ?e58)) +(flet ($e129 (distinct ?e66 ?e71)) +(flet ($e130 (= ?e7 ?e63)) +(flet ($e131 (= ?e53 ?e59)) +(flet ($e132 (distinct ?e63 ?e55)) +(flet ($e133 (= ?e66 ?e7)) +(flet ($e134 (distinct ?e60 ?e53)) +(flet ($e135 (distinct ?e52 ?e65)) +(flet ($e136 (distinct ?e11 ?e11)) +(flet ($e137 (= ?e54 ?e57)) +(flet ($e138 (= ?e73 v3)) +(flet ($e139 (= ?e70 ?e66)) +(flet ($e140 (distinct ?e59 ?e61)) +(flet ($e141 (distinct ?e7 ?e54)) +(flet ($e142 (= ?e70 ?e73)) +(flet ($e143 (distinct v3 ?e10)) +(flet ($e144 (= ?e7 ?e58)) +(flet ($e145 (= ?e57 ?e69)) +(flet ($e146 (distinct ?e52 ?e58)) +(flet ($e147 (distinct ?e55 ?e62)) +(flet ($e148 (= ?e10 ?e66)) +(flet ($e149 (distinct ?e70 ?e75)) +(flet ($e150 (= v3 ?e60)) +(flet ($e151 (= ?e7 ?e52)) +(flet ($e152 (distinct ?e73 ?e64)) +(flet ($e153 (= ?e56 ?e57)) +(flet ($e154 (distinct ?e52 ?e75)) +(flet ($e155 (distinct ?e66 ?e69)) +(flet ($e156 (= ?e56 ?e63)) +(flet ($e157 (= ?e11 ?e10)) +(flet ($e158 (= ?e69 ?e65)) +(flet ($e159 (distinct ?e52 ?e7)) +(flet ($e160 (= ?e53 ?e8)) +(flet ($e161 (implies $e83 $e151)) +(flet ($e162 (and $e156 $e109)) +(flet ($e163 (not $e133)) +(flet ($e164 (implies $e100 $e143)) +(flet ($e165 (iff $e114 $e162)) +(flet ($e166 (or $e76 $e152)) +(flet ($e167 (and $e12 $e93)) +(flet ($e168 (xor $e164 $e78)) +(flet ($e169 (and $e15 $e106)) +(flet ($e170 (not $e111)) +(flet ($e171 (xor $e18 $e135)) +(flet ($e172 (not $e14)) +(flet ($e173 (iff $e125 $e20)) +(flet ($e174 (iff $e84 $e142)) +(flet ($e175 (if_then_else $e129 $e150 $e153)) +(flet ($e176 (iff $e80 $e118)) +(flet ($e177 (xor $e99 $e103)) +(flet ($e178 (or $e97 $e91)) +(flet ($e179 (if_then_else $e127 $e77 $e172)) +(flet ($e180 (and $e169 $e101)) +(flet ($e181 (or $e147 $e90)) +(flet ($e182 (implies $e181 $e157)) +(flet ($e183 (or $e94 $e119)) +(flet ($e184 (and $e120 $e174)) +(flet ($e185 (iff $e23 $e177)) +(flet ($e186 (or $e86 $e85)) +(flet ($e187 (implies $e132 $e16)) +(flet ($e188 (if_then_else $e187 $e186 $e21)) +(flet ($e189 (or $e92 $e92)) +(flet ($e190 (xor $e113 $e128)) +(flet ($e191 (iff $e179 $e171)) +(flet ($e192 (not $e104)) +(flet ($e193 (and $e137 $e107)) +(flet ($e194 (or $e170 $e176)) +(flet ($e195 (or $e134 $e188)) +(flet ($e196 (and $e112 $e116)) +(flet ($e197 (if_then_else $e122 $e163 $e17)) +(flet ($e198 (if_then_else $e102 $e87 $e13)) +(flet ($e199 (or $e184 $e197)) +(flet ($e200 (implies $e189 $e196)) +(flet ($e201 (and $e191 $e79)) +(flet ($e202 (iff $e145 $e124)) +(flet ($e203 (if_then_else $e139 $e199 $e182)) +(flet ($e204 (iff $e146 $e141)) +(flet ($e205 (iff $e98 $e175)) +(flet ($e206 (or $e190 $e148)) +(flet ($e207 (and $e159 $e185)) +(flet ($e208 (xor $e144 $e165)) +(flet ($e209 (if_then_else $e202 $e167 $e19)) +(flet ($e210 (or $e208 $e180)) +(flet ($e211 (or $e89 $e203)) +(flet ($e212 (not $e198)) +(flet ($e213 (iff $e210 $e211)) +(flet ($e214 (implies $e205 $e81)) +(flet ($e215 (not $e192)) +(flet ($e216 (or $e110 $e213)) +(flet ($e217 (implies $e96 $e154)) +(flet ($e218 (not $e155)) +(flet ($e219 (xor $e136 $e105)) +(flet ($e220 (iff $e217 $e130)) +(flet ($e221 (or $e138 $e126)) +(flet ($e222 (not $e178)) +(flet ($e223 (if_then_else $e215 $e82 $e140)) +(flet ($e224 (not $e221)) +(flet ($e225 (implies $e204 $e220)) +(flet ($e226 (xor $e168 $e209)) +(flet ($e227 (or $e95 $e214)) +(flet ($e228 (implies $e218 $e218)) +(flet ($e229 (not $e225)) +(flet ($e230 (not $e229)) +(flet ($e231 (implies $e222 $e228)) +(flet ($e232 (and $e226 $e121)) +(flet ($e233 (iff $e206 $e108)) +(flet ($e234 (and $e230 $e166)) +(flet ($e235 (implies $e231 $e232)) +(flet ($e236 (not $e88)) +(flet ($e237 (not $e201)) +(flet ($e238 (if_then_else $e237 $e236 $e173)) +(flet ($e239 (and $e235 $e193)) +(flet ($e240 (xor $e239 $e238)) +(flet ($e241 (implies $e123 $e219)) +(flet ($e242 (if_then_else $e234 $e212 $e149)) +(flet ($e243 (or $e115 $e242)) +(flet ($e244 (and $e200 $e183)) +(flet ($e245 (implies $e207 $e233)) +(flet ($e246 (iff $e22 $e241)) +(flet ($e247 (implies $e194 $e240)) +(flet ($e248 (implies $e223 $e131)) +(flet ($e249 (or $e227 $e158)) +(flet ($e250 (and $e160 $e224)) +(flet ($e251 (or $e250 $e243)) +(flet ($e252 (or $e117 $e117)) +(flet ($e253 (and $e195 $e248)) +(flet ($e254 (xor $e253 $e249)) +(flet ($e255 (implies $e246 $e254)) +(flet ($e256 (iff $e251 $e161)) +(flet ($e257 (xor $e216 $e245)) +(flet ($e258 (xor $e255 $e256)) +(flet ($e259 (iff $e244 $e257)) +(flet ($e260 (if_then_else $e247 $e259 $e247)) +(flet ($e261 (xor $e258 $e252)) +(flet ($e262 (not $e260)) +(flet ($e263 (or $e262 $e262)) +(flet ($e264 (iff $e263 $e263)) +(flet ($e265 (and $e261 $e261)) +(flet ($e266 (implies $e264 $e264)) +(flet ($e267 (and $e265 $e266)) +$e267 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect11.smt b/test/regress/regress0/arrays/incorrect11.smt new file mode 100644 index 000000000..0815e98e4 --- /dev/null +++ b/test/regress/regress0/arrays/incorrect11.smt @@ -0,0 +1,96 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Index)) +:extrafuns ((v2 Element)) +:extrafuns ((v3 Element)) +:extrafuns ((v4 Element)) +:formula +(flet ($e5 (distinct v0 v0)) +(flet ($e6 (distinct v1 v1)) +(flet ($e7 (= v2 v3)) +(flet ($e8 (distinct v2 v4)) +(let (?e9 (ite $e7 v0 v0)) +(let (?e10 (ite $e5 v0 v0)) +(let (?e11 (ite $e8 v0 ?e9)) +(let (?e12 (ite $e8 ?e9 ?e9)) +(let (?e13 (ite $e6 ?e10 v0)) +(let (?e14 (ite $e8 v1 v1)) +(let (?e15 (ite $e5 ?e14 v1)) +(let (?e16 (ite $e7 v1 ?e15)) +(let (?e17 (ite $e6 ?e14 ?e15)) +(let (?e18 (ite $e7 v4 v2)) +(let (?e19 (ite $e5 v3 v3)) +(let (?e20 (ite $e8 ?e18 ?e18)) +(let (?e21 (ite $e6 v3 v3)) +(let (?e22 (select ?e13 v1)) +(flet ($e23 (distinct ?e9 ?e9)) +(flet ($e24 (= v0 ?e10)) +(flet ($e25 (distinct ?e9 ?e12)) +(flet ($e26 (= ?e11 v0)) +(flet ($e27 (distinct ?e13 ?e11)) +(flet ($e28 (distinct ?e14 v1)) +(flet ($e29 (= ?e15 ?e16)) +(flet ($e30 (= ?e16 v1)) +(flet ($e31 (distinct v1 ?e15)) +(flet ($e32 (= ?e17 v1)) +(flet ($e33 (= ?e21 ?e18)) +(flet ($e34 (distinct v3 v3)) +(flet ($e35 (= ?e21 ?e20)) +(flet ($e36 (distinct ?e18 v4)) +(flet ($e37 (distinct v2 v4)) +(flet ($e38 (= ?e20 ?e21)) +(flet ($e39 (= v3 v2)) +(flet ($e40 (distinct v3 ?e19)) +(flet ($e41 (distinct v4 ?e18)) +(flet ($e42 (= v3 v3)) +(flet ($e43 (= ?e21 ?e21)) +(flet ($e44 (distinct v2 ?e18)) +(flet ($e45 (distinct v2 v2)) +(flet ($e46 (distinct v3 v3)) +(flet ($e47 (= ?e19 v3)) +(flet ($e48 (= v4 v4)) +(flet ($e49 (= ?e19 v2)) +(flet ($e50 (= ?e20 ?e18)) +(flet ($e51 (distinct ?e22 ?e22)) +(flet ($e52 (or $e42 $e31)) +(flet ($e53 (xor $e39 $e35)) +(flet ($e54 (and $e51 $e30)) +(flet ($e55 (or $e43 $e54)) +(flet ($e56 (xor $e26 $e33)) +(flet ($e57 (not $e41)) +(flet ($e58 (implies $e32 $e50)) +(flet ($e59 (not $e24)) +(flet ($e60 (if_then_else $e53 $e7 $e27)) +(flet ($e61 (and $e48 $e38)) +(flet ($e62 (and $e61 $e52)) +(flet ($e63 (xor $e25 $e58)) +(flet ($e64 (and $e49 $e8)) +(flet ($e65 (xor $e62 $e34)) +(flet ($e66 (iff $e29 $e37)) +(flet ($e67 (if_then_else $e65 $e65 $e65)) +(flet ($e68 (xor $e46 $e55)) +(flet ($e69 (xor $e66 $e56)) +(flet ($e70 (or $e40 $e69)) +(flet ($e71 (xor $e36 $e6)) +(flet ($e72 (iff $e59 $e68)) +(flet ($e73 (and $e64 $e64)) +(flet ($e74 (iff $e57 $e63)) +(flet ($e75 (xor $e67 $e5)) +(flet ($e76 (or $e60 $e60)) +(flet ($e77 (and $e47 $e71)) +(flet ($e78 (xor $e23 $e76)) +(flet ($e79 (xor $e74 $e74)) +(flet ($e80 (and $e28 $e45)) +(flet ($e81 (if_then_else $e75 $e70 $e79)) +(flet ($e82 (if_then_else $e78 $e44 $e77)) +(flet ($e83 (or $e73 $e73)) +(flet ($e84 (iff $e72 $e80)) +(flet ($e85 (not $e82)) +(flet ($e86 (if_then_else $e81 $e81 $e85)) +(flet ($e87 (iff $e86 $e84)) +(flet ($e88 (and $e87 $e83)) +$e88 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect2.smt b/test/regress/regress0/arrays/incorrect2.smt new file mode 100644 index 000000000..2172bbc68 --- /dev/null +++ b/test/regress/regress0/arrays/incorrect2.smt @@ -0,0 +1,350 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Index)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v4 Index)) +:extrafuns ((v5 Element)) +:formula +(flet ($e6 (= v0 v0)) +(flet ($e7 (= v4 v2)) +(flet ($e8 (distinct v3 v2)) +(flet ($e9 (= v3 v3)) +(flet ($e10 (= v2 v3)) +(flet ($e11 (distinct v2 v2)) +(flet ($e12 (distinct v4 v3)) +(flet ($e13 (distinct v4 v2)) +(flet ($e14 (distinct v4 v4)) +(flet ($e15 (distinct v3 v2)) +(flet ($e16 (= v2 v3)) +(flet ($e17 (distinct v1 v2)) +(flet ($e18 (= v5 v5)) +(let (?e19 (ite $e15 v0 v0)) +(let (?e20 (ite $e7 v0 ?e19)) +(let (?e21 (ite $e16 ?e19 ?e19)) +(let (?e22 (ite $e14 ?e19 ?e21)) +(let (?e23 (ite $e9 ?e20 ?e21)) +(let (?e24 (ite $e17 ?e23 ?e23)) +(let (?e25 (ite $e6 ?e19 ?e19)) +(let (?e26 (ite $e9 ?e22 ?e22)) +(let (?e27 (ite $e13 ?e21 ?e19)) +(let (?e28 (ite $e8 ?e21 ?e23)) +(let (?e29 (ite $e18 ?e23 ?e21)) +(let (?e30 (ite $e15 ?e26 ?e19)) +(let (?e31 (ite $e12 ?e19 ?e19)) +(let (?e32 (ite $e14 ?e21 v0)) +(let (?e33 (ite $e10 ?e21 ?e23)) +(let (?e34 (ite $e11 ?e29 ?e27)) +(let (?e35 (ite $e11 v3 v4)) +(let (?e36 (ite $e10 ?e35 v4)) +(let (?e37 (ite $e14 v1 v2)) +(let (?e38 (ite $e17 v3 ?e37)) +(let (?e39 (ite $e16 ?e35 v4)) +(let (?e40 (ite $e10 ?e36 v1)) +(let (?e41 (ite $e18 ?e38 v2)) +(let (?e42 (ite $e16 ?e38 ?e37)) +(let (?e43 (ite $e15 ?e41 v4)) +(let (?e44 (ite $e9 ?e36 ?e35)) +(let (?e45 (ite $e13 ?e36 v1)) +(let (?e46 (ite $e7 ?e36 v2)) +(let (?e47 (ite $e6 ?e43 ?e41)) +(let (?e48 (ite $e8 ?e47 ?e38)) +(let (?e49 (ite $e12 ?e46 v3)) +(let (?e50 (ite $e11 v5 v5)) +(let (?e51 (ite $e16 v5 v5)) +(let (?e52 (ite $e14 ?e51 ?e50)) +(let (?e53 (ite $e12 ?e50 ?e51)) +(let (?e54 (ite $e17 ?e52 v5)) +(let (?e55 (ite $e6 ?e51 ?e53)) +(let (?e56 (ite $e7 v5 ?e51)) +(let (?e57 (ite $e15 ?e51 ?e56)) +(let (?e58 (ite $e13 ?e51 v5)) +(let (?e59 (ite $e17 ?e55 ?e50)) +(let (?e60 (ite $e6 v5 ?e56)) +(let (?e61 (ite $e8 ?e56 ?e58)) +(let (?e62 (ite $e15 ?e59 ?e52)) +(let (?e63 (ite $e14 ?e50 ?e52)) +(let (?e64 (ite $e6 ?e55 ?e54)) +(let (?e65 (ite $e16 ?e54 ?e60)) +(let (?e66 (ite $e9 ?e65 ?e58)) +(let (?e67 (ite $e12 ?e57 ?e62)) +(let (?e68 (ite $e18 ?e51 ?e58)) +(let (?e69 (ite $e10 ?e54 ?e58)) +(let (?e70 (select ?e29 ?e40)) +(flet ($e71 (= ?e23 ?e28)) +(flet ($e72 (= ?e23 ?e26)) +(flet ($e73 (distinct ?e21 ?e19)) +(flet ($e74 (distinct ?e19 ?e32)) +(flet ($e75 (distinct ?e24 ?e26)) +(flet ($e76 (distinct ?e26 ?e30)) +(flet ($e77 (distinct v0 ?e26)) +(flet ($e78 (distinct ?e33 ?e22)) +(flet ($e79 (= ?e34 ?e28)) +(flet ($e80 (= ?e19 ?e32)) +(flet ($e81 (distinct ?e24 ?e30)) +(flet ($e82 (distinct ?e34 ?e23)) +(flet ($e83 (= ?e21 ?e27)) +(flet ($e84 (= v0 ?e21)) +(flet ($e85 (distinct ?e27 ?e21)) +(flet ($e86 (= ?e21 ?e30)) +(flet ($e87 (= ?e26 ?e34)) +(flet ($e88 (= ?e27 ?e33)) +(flet ($e89 (distinct ?e24 ?e26)) +(flet ($e90 (= ?e24 ?e19)) +(flet ($e91 (= ?e33 ?e21)) +(flet ($e92 (= ?e24 ?e33)) +(flet ($e93 (= ?e34 ?e33)) +(flet ($e94 (= ?e33 v0)) +(flet ($e95 (= ?e29 ?e26)) +(flet ($e96 (= ?e25 ?e31)) +(flet ($e97 (distinct ?e19 ?e31)) +(flet ($e98 (= ?e19 ?e29)) +(flet ($e99 (distinct ?e31 ?e31)) +(flet ($e100 (= ?e27 ?e27)) +(flet ($e101 (distinct ?e27 v0)) +(flet ($e102 (distinct ?e23 ?e29)) +(flet ($e103 (distinct ?e27 ?e29)) +(flet ($e104 (= ?e31 ?e29)) +(flet ($e105 (= ?e25 ?e26)) +(flet ($e106 (= ?e26 ?e31)) +(flet ($e107 (= ?e28 ?e33)) +(flet ($e108 (distinct v0 ?e27)) +(flet ($e109 (distinct ?e30 ?e23)) +(flet ($e110 (distinct ?e34 ?e30)) +(flet ($e111 (= ?e30 ?e31)) +(flet ($e112 (= ?e27 ?e32)) +(flet ($e113 (= ?e24 ?e27)) +(flet ($e114 (distinct ?e31 ?e26)) +(flet ($e115 (distinct ?e23 ?e30)) +(flet ($e116 (distinct v0 ?e34)) +(flet ($e117 (= ?e30 ?e21)) +(flet ($e118 (= v0 ?e34)) +(flet ($e119 (= ?e27 ?e26)) +(flet ($e120 (= ?e26 v0)) +(flet ($e121 (distinct ?e26 ?e34)) +(flet ($e122 (= ?e31 ?e33)) +(flet ($e123 (distinct ?e28 ?e21)) +(flet ($e124 (= ?e22 ?e34)) +(flet ($e125 (distinct ?e21 v0)) +(flet ($e126 (distinct ?e34 ?e29)) +(flet ($e127 (= ?e28 ?e30)) +(flet ($e128 (= ?e20 ?e26)) +(flet ($e129 (distinct ?e36 ?e36)) +(flet ($e130 (= v2 ?e41)) +(flet ($e131 (distinct ?e39 ?e38)) +(flet ($e132 (distinct v1 v3)) +(flet ($e133 (= ?e48 ?e38)) +(flet ($e134 (= ?e43 ?e44)) +(flet ($e135 (= ?e41 v4)) +(flet ($e136 (= ?e45 ?e47)) +(flet ($e137 (distinct ?e36 ?e48)) +(flet ($e138 (= ?e47 ?e46)) +(flet ($e139 (= v2 ?e40)) +(flet ($e140 (= ?e45 ?e44)) +(flet ($e141 (= ?e35 v1)) +(flet ($e142 (= v4 v4)) +(flet ($e143 (= ?e42 ?e35)) +(flet ($e144 (= v1 ?e41)) +(flet ($e145 (= ?e47 ?e40)) +(flet ($e146 (= ?e47 v1)) +(flet ($e147 (distinct ?e41 ?e44)) +(flet ($e148 (= ?e35 ?e35)) +(flet ($e149 (distinct ?e35 v1)) +(flet ($e150 (= ?e40 ?e44)) +(flet ($e151 (= ?e45 v2)) +(flet ($e152 (= v2 ?e35)) +(flet ($e153 (distinct ?e38 v3)) +(flet ($e154 (distinct ?e45 ?e38)) +(flet ($e155 (distinct v4 ?e48)) +(flet ($e156 (= ?e49 ?e46)) +(flet ($e157 (distinct ?e40 ?e44)) +(flet ($e158 (= ?e42 ?e46)) +(flet ($e159 (= ?e39 ?e39)) +(flet ($e160 (distinct ?e44 ?e41)) +(flet ($e161 (= ?e48 v2)) +(flet ($e162 (distinct ?e49 ?e46)) +(flet ($e163 (= ?e39 ?e44)) +(flet ($e164 (distinct ?e41 ?e40)) +(flet ($e165 (distinct ?e46 ?e46)) +(flet ($e166 (distinct v3 ?e37)) +(flet ($e167 (= ?e51 ?e53)) +(flet ($e168 (= ?e59 ?e53)) +(flet ($e169 (= ?e67 ?e59)) +(flet ($e170 (distinct ?e55 ?e64)) +(flet ($e171 (distinct ?e58 ?e52)) +(flet ($e172 (= ?e52 ?e52)) +(flet ($e173 (distinct ?e69 ?e61)) +(flet ($e174 (distinct ?e67 ?e56)) +(flet ($e175 (= ?e62 ?e62)) +(flet ($e176 (distinct ?e50 ?e52)) +(flet ($e177 (= ?e52 ?e60)) +(flet ($e178 (distinct ?e68 ?e58)) +(flet ($e179 (= ?e62 ?e50)) +(flet ($e180 (distinct v5 ?e62)) +(flet ($e181 (distinct ?e53 ?e57)) +(flet ($e182 (= ?e63 ?e50)) +(flet ($e183 (= ?e62 ?e56)) +(flet ($e184 (= ?e54 ?e61)) +(flet ($e185 (distinct ?e69 ?e59)) +(flet ($e186 (= ?e65 ?e52)) +(flet ($e187 (distinct ?e64 ?e63)) +(flet ($e188 (= ?e63 ?e66)) +(flet ($e189 (distinct ?e64 ?e67)) +(flet ($e190 (= v5 v5)) +(flet ($e191 (distinct ?e52 ?e60)) +(flet ($e192 (distinct ?e51 ?e70)) +(flet ($e193 (xor $e181 $e149)) +(flet ($e194 (xor $e188 $e96)) +(flet ($e195 (implies $e179 $e73)) +(flet ($e196 (iff $e83 $e91)) +(flet ($e197 (or $e105 $e123)) +(flet ($e198 (and $e121 $e172)) +(flet ($e199 (not $e147)) +(flet ($e200 (iff $e189 $e117)) +(flet ($e201 (or $e155 $e108)) +(flet ($e202 (iff $e144 $e175)) +(flet ($e203 (or $e107 $e201)) +(flet ($e204 (and $e8 $e168)) +(flet ($e205 (iff $e90 $e171)) +(flet ($e206 (or $e157 $e10)) +(flet ($e207 (xor $e92 $e82)) +(flet ($e208 (xor $e180 $e148)) +(flet ($e209 (iff $e191 $e124)) +(flet ($e210 (xor $e110 $e152)) +(flet ($e211 (implies $e102 $e18)) +(flet ($e212 (not $e139)) +(flet ($e213 (implies $e205 $e203)) +(flet ($e214 (not $e209)) +(flet ($e215 (xor $e94 $e192)) +(flet ($e216 (or $e122 $e6)) +(flet ($e217 (and $e145 $e113)) +(flet ($e218 (implies $e161 $e88)) +(flet ($e219 (xor $e202 $e199)) +(flet ($e220 (xor $e135 $e213)) +(flet ($e221 (not $e100)) +(flet ($e222 (not $e87)) +(flet ($e223 (and $e127 $e208)) +(flet ($e224 (implies $e166 $e212)) +(flet ($e225 (not $e115)) +(flet ($e226 (not $e15)) +(flet ($e227 (or $e170 $e120)) +(flet ($e228 (not $e101)) +(flet ($e229 (implies $e156 $e162)) +(flet ($e230 (iff $e125 $e75)) +(flet ($e231 (xor $e223 $e81)) +(flet ($e232 (implies $e174 $e160)) +(flet ($e233 (implies $e97 $e200)) +(flet ($e234 (if_then_else $e103 $e134 $e176)) +(flet ($e235 (and $e133 $e89)) +(flet ($e236 (not $e17)) +(flet ($e237 (implies $e225 $e98)) +(flet ($e238 (or $e130 $e104)) +(flet ($e239 (not $e169)) +(flet ($e240 (implies $e118 $e16)) +(flet ($e241 (iff $e237 $e190)) +(flet ($e242 (not $e227)) +(flet ($e243 (and $e154 $e217)) +(flet ($e244 (if_then_else $e137 $e76 $e236)) +(flet ($e245 (not $e153)) +(flet ($e246 (and $e138 $e93)) +(flet ($e247 (not $e197)) +(flet ($e248 (xor $e141 $e210)) +(flet ($e249 (iff $e140 $e246)) +(flet ($e250 (or $e187 $e72)) +(flet ($e251 (implies $e228 $e14)) +(flet ($e252 (if_then_else $e193 $e11 $e85)) +(flet ($e253 (iff $e158 $e80)) +(flet ($e254 (or $e167 $e86)) +(flet ($e255 (not $e243)) +(flet ($e256 (or $e79 $e7)) +(flet ($e257 (implies $e109 $e9)) +(flet ($e258 (xor $e177 $e126)) +(flet ($e259 (xor $e254 $e13)) +(flet ($e260 (or $e226 $e250)) +(flet ($e261 (not $e95)) +(flet ($e262 (iff $e99 $e234)) +(flet ($e263 (implies $e260 $e242)) +(flet ($e264 (implies $e173 $e233)) +(flet ($e265 (if_then_else $e218 $e214 $e12)) +(flet ($e266 (and $e221 $e248)) +(flet ($e267 (or $e106 $e206)) +(flet ($e268 (iff $e263 $e245)) +(flet ($e269 (if_then_else $e262 $e216 $e266)) +(flet ($e270 (and $e257 $e247)) +(flet ($e271 (if_then_else $e198 $e270 $e132)) +(flet ($e272 (xor $e230 $e204)) +(flet ($e273 (not $e235)) +(flet ($e274 (and $e143 $e220)) +(flet ($e275 (and $e128 $e142)) +(flet ($e276 (and $e114 $e74)) +(flet ($e277 (if_then_else $e252 $e195 $e146)) +(flet ($e278 (xor $e277 $e275)) +(flet ($e279 (implies $e232 $e259)) +(flet ($e280 (xor $e264 $e164)) +(flet ($e281 (or $e112 $e159)) +(flet ($e282 (xor $e240 $e78)) +(flet ($e283 (or $e231 $e258)) +(flet ($e284 (if_then_else $e77 $e136 $e71)) +(flet ($e285 (implies $e279 $e251)) +(flet ($e286 (or $e241 $e238)) +(flet ($e287 (and $e274 $e244)) +(flet ($e288 (or $e185 $e196)) +(flet ($e289 (and $e84 $e267)) +(flet ($e290 (and $e219 $e215)) +(flet ($e291 (or $e268 $e278)) +(flet ($e292 (if_then_else $e186 $e119 $e256)) +(flet ($e293 (iff $e253 $e289)) +(flet ($e294 (not $e151)) +(flet ($e295 (implies $e239 $e294)) +(flet ($e296 (iff $e207 $e290)) +(flet ($e297 (if_then_else $e291 $e182 $e283)) +(flet ($e298 (iff $e131 $e150)) +(flet ($e299 (if_then_else $e184 $e269 $e288)) +(flet ($e300 (xor $e249 $e229)) +(flet ($e301 (not $e272)) +(flet ($e302 (if_then_else $e281 $e261 $e129)) +(flet ($e303 (or $e296 $e183)) +(flet ($e304 (not $e299)) +(flet ($e305 (and $e222 $e178)) +(flet ($e306 (implies $e224 $e255)) +(flet ($e307 (not $e302)) +(flet ($e308 (xor $e271 $e285)) +(flet ($e309 (and $e301 $e305)) +(flet ($e310 (or $e297 $e116)) +(flet ($e311 (and $e287 $e295)) +(flet ($e312 (if_then_else $e310 $e282 $e303)) +(flet ($e313 (and $e304 $e312)) +(flet ($e314 (implies $e211 $e286)) +(flet ($e315 (implies $e273 $e307)) +(flet ($e316 (xor $e165 $e292)) +(flet ($e317 (iff $e306 $e300)) +(flet ($e318 (implies $e313 $e314)) +(flet ($e319 (and $e298 $e194)) +(flet ($e320 (not $e308)) +(flet ($e321 (not $e311)) +(flet ($e322 (not $e321)) +(flet ($e323 (not $e319)) +(flet ($e324 (implies $e280 $e276)) +(flet ($e325 (or $e111 $e323)) +(flet ($e326 (and $e315 $e315)) +(flet ($e327 (iff $e265 $e316)) +(flet ($e328 (iff $e325 $e324)) +(flet ($e329 (implies $e163 $e284)) +(flet ($e330 (not $e320)) +(flet ($e331 (and $e293 $e330)) +(flet ($e332 (or $e326 $e318)) +(flet ($e333 (implies $e328 $e328)) +(flet ($e334 (iff $e309 $e309)) +(flet ($e335 (iff $e334 $e332)) +(flet ($e336 (not $e322)) +(flet ($e337 (and $e331 $e333)) +(flet ($e338 (or $e327 $e337)) +(flet ($e339 (implies $e329 $e317)) +(flet ($e340 (iff $e338 $e335)) +(flet ($e341 (implies $e339 $e340)) +(flet ($e342 (xor $e336 $e341)) +$e342 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect3.smt b/test/regress/regress0/arrays/incorrect3.smt new file mode 100644 index 000000000..f8184783d --- /dev/null +++ b/test/regress/regress0/arrays/incorrect3.smt @@ -0,0 +1,446 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Index)) +:extrafuns ((v2 Element)) +:extrafuns ((v3 Element)) +:extrafuns ((v4 Element)) +:extrafuns ((v5 Element)) +:extrafuns ((v6 Element)) +:formula +(let (?e7 (store v0 v1 v2)) +(let (?e8 (select ?e7 v1)) +(let (?e9 (select ?e7 v1)) +(flet ($e10 (distinct v0 v0)) +(flet ($e11 (= ?e7 v0)) +(flet ($e12 (distinct v1 v1)) +(flet ($e13 (distinct v4 ?e9)) +(flet ($e14 (distinct v2 v6)) +(flet ($e15 (= ?e9 ?e9)) +(flet ($e16 (distinct v2 v5)) +(flet ($e17 (= v6 v5)) +(flet ($e18 (= v3 v3)) +(flet ($e19 (= v2 v2)) +(flet ($e20 (distinct v2 v2)) +(flet ($e21 (distinct v3 v4)) +(flet ($e22 (distinct v4 ?e9)) +(flet ($e23 (distinct v4 v5)) +(flet ($e24 (= ?e9 v3)) +(flet ($e25 (= v3 ?e8)) +(let (?e26 (ite $e21 v0 v0)) +(let (?e27 (ite $e20 ?e7 v0)) +(let (?e28 (ite $e13 ?e26 v0)) +(let (?e29 (ite $e22 ?e7 ?e7)) +(let (?e30 (ite $e17 ?e29 ?e29)) +(let (?e31 (ite $e16 ?e28 ?e28)) +(let (?e32 (ite $e18 ?e29 ?e30)) +(let (?e33 (ite $e11 ?e28 ?e29)) +(let (?e34 (ite $e15 ?e29 ?e31)) +(let (?e35 (ite $e21 ?e30 ?e26)) +(let (?e36 (ite $e11 ?e32 ?e30)) +(let (?e37 (ite $e14 ?e35 ?e34)) +(let (?e38 (ite $e17 ?e7 ?e28)) +(let (?e39 (ite $e19 ?e7 ?e7)) +(let (?e40 (ite $e23 ?e32 v0)) +(let (?e41 (ite $e12 ?e26 ?e29)) +(let (?e42 (ite $e10 ?e36 ?e27)) +(let (?e43 (ite $e10 v0 ?e7)) +(let (?e44 (ite $e16 ?e41 ?e43)) +(let (?e45 (ite $e11 ?e41 ?e43)) +(let (?e46 (ite $e24 ?e33 ?e32)) +(let (?e47 (ite $e17 ?e38 v0)) +(let (?e48 (ite $e25 ?e27 ?e28)) +(let (?e49 (ite $e20 v1 v1)) +(let (?e50 (ite $e16 v1 ?e49)) +(let (?e51 (ite $e12 ?e50 v1)) +(let (?e52 (ite $e16 ?e51 ?e51)) +(let (?e53 (ite $e19 ?e51 ?e52)) +(let (?e54 (ite $e11 v1 v1)) +(let (?e55 (ite $e14 ?e49 ?e50)) +(let (?e56 (ite $e19 ?e52 ?e52)) +(let (?e57 (ite $e14 ?e51 ?e54)) +(let (?e58 (ite $e20 v1 ?e53)) +(let (?e59 (ite $e15 ?e50 ?e53)) +(let (?e60 (ite $e17 ?e55 ?e49)) +(let (?e61 (ite $e10 ?e60 ?e50)) +(let (?e62 (ite $e23 ?e57 ?e52)) +(let (?e63 (ite $e23 ?e62 ?e61)) +(let (?e64 (ite $e13 ?e51 ?e57)) +(let (?e65 (ite $e21 ?e55 ?e63)) +(let (?e66 (ite $e25 ?e51 ?e56)) +(let (?e67 (ite $e24 ?e50 ?e55)) +(let (?e68 (ite $e14 ?e66 ?e66)) +(let (?e69 (ite $e19 ?e52 ?e67)) +(let (?e70 (ite $e11 ?e53 ?e54)) +(let (?e71 (ite $e18 ?e56 ?e69)) +(let (?e72 (ite $e22 ?e55 ?e52)) +(let (?e73 (ite $e16 v6 v5)) +(let (?e74 (ite $e12 v4 v3)) +(let (?e75 (ite $e25 v6 v3)) +(let (?e76 (ite $e17 v5 v6)) +(let (?e77 (ite $e20 ?e8 v2)) +(let (?e78 (ite $e24 v5 ?e9)) +(let (?e79 (ite $e23 v3 v5)) +(let (?e80 (ite $e13 ?e8 ?e77)) +(let (?e81 (ite $e23 v5 ?e75)) +(let (?e82 (ite $e21 v4 v5)) +(let (?e83 (ite $e19 v5 v5)) +(let (?e84 (ite $e12 v4 ?e78)) +(let (?e85 (ite $e11 ?e76 v4)) +(let (?e86 (ite $e20 ?e77 ?e82)) +(let (?e87 (ite $e12 v5 ?e75)) +(let (?e88 (ite $e18 ?e76 ?e84)) +(let (?e89 (ite $e16 ?e76 ?e75)) +(let (?e90 (ite $e17 ?e77 ?e85)) +(let (?e91 (ite $e17 ?e77 v4)) +(let (?e92 (ite $e10 ?e91 ?e78)) +(let (?e93 (ite $e18 v2 ?e73)) +(let (?e94 (ite $e12 v3 ?e93)) +(let (?e95 (ite $e15 ?e74 ?e73)) +(let (?e96 (ite $e22 ?e95 v2)) +(let (?e97 (ite $e25 v6 v5)) +(let (?e98 (ite $e14 ?e97 v3)) +(let (?e99 (store ?e45 ?e61 ?e74)) +(let (?e100 (select ?e44 ?e60)) +(let (?e101 (select ?e46 ?e57)) +(let (?e102 (store ?e37 ?e67 ?e79)) +(let (?e103 (select ?e33 ?e61)) +(flet ($e104 (= ?e48 ?e43)) +(flet ($e105 (distinct ?e40 ?e35)) +(flet ($e106 (distinct ?e32 ?e44)) +(flet ($e107 (distinct v0 ?e42)) +(flet ($e108 (= ?e32 ?e38)) +(flet ($e109 (distinct ?e41 ?e28)) +(flet ($e110 (distinct ?e34 ?e31)) +(flet ($e111 (= ?e26 v0)) +(flet ($e112 (distinct ?e31 ?e46)) +(flet ($e113 (distinct ?e48 ?e42)) +(flet ($e114 (distinct ?e44 ?e29)) +(flet ($e115 (distinct ?e31 ?e102)) +(flet ($e116 (distinct ?e37 ?e102)) +(flet ($e117 (= ?e38 ?e27)) +(flet ($e118 (distinct ?e46 ?e46)) +(flet ($e119 (distinct ?e26 ?e48)) +(flet ($e120 (= ?e38 ?e33)) +(flet ($e121 (distinct ?e31 ?e48)) +(flet ($e122 (= ?e7 ?e40)) +(flet ($e123 (= ?e27 ?e41)) +(flet ($e124 (distinct ?e39 ?e36)) +(flet ($e125 (distinct ?e36 ?e37)) +(flet ($e126 (distinct ?e44 ?e41)) +(flet ($e127 (= ?e40 ?e34)) +(flet ($e128 (distinct ?e27 ?e43)) +(flet ($e129 (distinct ?e43 ?e32)) +(flet ($e130 (distinct ?e46 ?e44)) +(flet ($e131 (= ?e37 ?e32)) +(flet ($e132 (= ?e99 ?e43)) +(flet ($e133 (distinct ?e42 ?e102)) +(flet ($e134 (distinct ?e30 ?e99)) +(flet ($e135 (distinct ?e27 ?e48)) +(flet ($e136 (= ?e34 ?e41)) +(flet ($e137 (= ?e31 ?e48)) +(flet ($e138 (distinct ?e48 ?e40)) +(flet ($e139 (= ?e46 ?e43)) +(flet ($e140 (distinct ?e32 ?e42)) +(flet ($e141 (distinct ?e42 ?e102)) +(flet ($e142 (= ?e36 ?e27)) +(flet ($e143 (distinct ?e28 ?e45)) +(flet ($e144 (= ?e43 ?e36)) +(flet ($e145 (= ?e32 ?e40)) +(flet ($e146 (= ?e31 ?e28)) +(flet ($e147 (distinct ?e47 ?e102)) +(flet ($e148 (= ?e58 ?e71)) +(flet ($e149 (distinct ?e49 ?e50)) +(flet ($e150 (distinct ?e71 ?e70)) +(flet ($e151 (= ?e57 ?e59)) +(flet ($e152 (distinct ?e66 ?e67)) +(flet ($e153 (distinct ?e56 ?e69)) +(flet ($e154 (distinct ?e62 ?e57)) +(flet ($e155 (distinct ?e67 ?e61)) +(flet ($e156 (distinct ?e63 ?e55)) +(flet ($e157 (distinct ?e63 ?e69)) +(flet ($e158 (= ?e63 ?e64)) +(flet ($e159 (= ?e50 ?e68)) +(flet ($e160 (= ?e72 ?e63)) +(flet ($e161 (distinct ?e59 ?e57)) +(flet ($e162 (distinct ?e61 ?e58)) +(flet ($e163 (distinct ?e53 ?e71)) +(flet ($e164 (distinct ?e57 ?e66)) +(flet ($e165 (= ?e60 ?e64)) +(flet ($e166 (distinct ?e65 ?e54)) +(flet ($e167 (distinct ?e63 ?e72)) +(flet ($e168 (distinct ?e68 ?e66)) +(flet ($e169 (= ?e66 v1)) +(flet ($e170 (distinct ?e65 ?e59)) +(flet ($e171 (= ?e61 v1)) +(flet ($e172 (= v1 ?e53)) +(flet ($e173 (= ?e60 ?e57)) +(flet ($e174 (= ?e54 ?e49)) +(flet ($e175 (distinct ?e53 ?e54)) +(flet ($e176 (= ?e63 ?e70)) +(flet ($e177 (distinct ?e58 ?e60)) +(flet ($e178 (= ?e54 ?e59)) +(flet ($e179 (distinct ?e60 ?e67)) +(flet ($e180 (distinct ?e54 ?e59)) +(flet ($e181 (= ?e71 ?e72)) +(flet ($e182 (= ?e71 ?e66)) +(flet ($e183 (= ?e66 ?e54)) +(flet ($e184 (distinct ?e56 ?e66)) +(flet ($e185 (distinct ?e59 ?e72)) +(flet ($e186 (= ?e50 ?e50)) +(flet ($e187 (= ?e55 ?e63)) +(flet ($e188 (= ?e58 ?e51)) +(flet ($e189 (= ?e67 ?e72)) +(flet ($e190 (distinct ?e66 ?e71)) +(flet ($e191 (distinct ?e66 ?e68)) +(flet ($e192 (= ?e55 ?e56)) +(flet ($e193 (distinct ?e49 ?e63)) +(flet ($e194 (= ?e61 ?e53)) +(flet ($e195 (distinct ?e57 v1)) +(flet ($e196 (distinct ?e66 ?e68)) +(flet ($e197 (distinct ?e60 ?e71)) +(flet ($e198 (= ?e52 ?e53)) +(flet ($e199 (distinct v2 v5)) +(flet ($e200 (= ?e82 ?e84)) +(flet ($e201 (= ?e94 ?e76)) +(flet ($e202 (distinct ?e9 v6)) +(flet ($e203 (= v2 ?e92)) +(flet ($e204 (= ?e83 ?e88)) +(flet ($e205 (= ?e79 ?e81)) +(flet ($e206 (= ?e93 ?e95)) +(flet ($e207 (= ?e86 ?e73)) +(flet ($e208 (= ?e96 v2)) +(flet ($e209 (distinct ?e84 ?e88)) +(flet ($e210 (distinct ?e93 v5)) +(flet ($e211 (distinct v6 ?e92)) +(flet ($e212 (distinct ?e86 ?e96)) +(flet ($e213 (distinct ?e8 ?e86)) +(flet ($e214 (distinct v5 ?e103)) +(flet ($e215 (= ?e77 ?e9)) +(flet ($e216 (= ?e93 ?e75)) +(flet ($e217 (= v6 ?e79)) +(flet ($e218 (= v3 ?e75)) +(flet ($e219 (= ?e79 ?e75)) +(flet ($e220 (= ?e91 ?e92)) +(flet ($e221 (distinct ?e93 ?e78)) +(flet ($e222 (= ?e98 ?e77)) +(flet ($e223 (= ?e76 ?e98)) +(flet ($e224 (distinct ?e88 ?e94)) +(flet ($e225 (distinct ?e9 ?e74)) +(flet ($e226 (distinct ?e79 ?e91)) +(flet ($e227 (= ?e75 v6)) +(flet ($e228 (distinct ?e86 ?e90)) +(flet ($e229 (distinct ?e101 ?e86)) +(flet ($e230 (= ?e93 v5)) +(flet ($e231 (distinct ?e84 ?e94)) +(flet ($e232 (distinct v2 ?e83)) +(flet ($e233 (distinct ?e85 ?e9)) +(flet ($e234 (distinct ?e87 ?e81)) +(flet ($e235 (distinct v5 ?e77)) +(flet ($e236 (= ?e96 ?e87)) +(flet ($e237 (distinct ?e87 ?e100)) +(flet ($e238 (= ?e73 ?e80)) +(flet ($e239 (= v4 ?e87)) +(flet ($e240 (= ?e73 ?e86)) +(flet ($e241 (distinct v2 ?e90)) +(flet ($e242 (distinct ?e74 ?e9)) +(flet ($e243 (= ?e95 ?e8)) +(flet ($e244 (= v2 v6)) +(flet ($e245 (= ?e97 ?e88)) +(flet ($e246 (distinct ?e74 ?e73)) +(flet ($e247 (distinct ?e94 ?e76)) +(flet ($e248 (= ?e103 ?e85)) +(flet ($e249 (= ?e84 ?e85)) +(flet ($e250 (= ?e73 ?e77)) +(flet ($e251 (= ?e73 v6)) +(flet ($e252 (distinct v4 ?e84)) +(flet ($e253 (distinct ?e98 ?e101)) +(flet ($e254 (distinct ?e87 ?e81)) +(flet ($e255 (= ?e94 ?e77)) +(flet ($e256 (= ?e73 v5)) +(flet ($e257 (distinct ?e81 ?e101)) +(flet ($e258 (distinct ?e103 ?e73)) +(flet ($e259 (distinct ?e92 ?e89)) +(flet ($e260 (and $e120 $e210)) +(flet ($e261 (and $e127 $e173)) +(flet ($e262 (iff $e174 $e249)) +(flet ($e263 (if_then_else $e114 $e240 $e185)) +(flet ($e264 (implies $e198 $e156)) +(flet ($e265 (or $e203 $e263)) +(flet ($e266 (and $e255 $e204)) +(flet ($e267 (implies $e243 $e209)) +(flet ($e268 (if_then_else $e222 $e112 $e199)) +(flet ($e269 (or $e145 $e257)) +(flet ($e270 (if_then_else $e10 $e134 $e136)) +(flet ($e271 (or $e264 $e131)) +(flet ($e272 (iff $e218 $e226)) +(flet ($e273 (xor $e152 $e195)) +(flet ($e274 (xor $e262 $e13)) +(flet ($e275 (if_then_else $e177 $e108 $e12)) +(flet ($e276 (not $e247)) +(flet ($e277 (implies $e180 $e275)) +(flet ($e278 (not $e196)) +(flet ($e279 (and $e242 $e151)) +(flet ($e280 (xor $e273 $e148)) +(flet ($e281 (or $e212 $e235)) +(flet ($e282 (if_then_else $e172 $e201 $e25)) +(flet ($e283 (not $e14)) +(flet ($e284 (if_then_else $e267 $e168 $e146)) +(flet ($e285 (and $e219 $e16)) +(flet ($e286 (xor $e272 $e105)) +(flet ($e287 (xor $e21 $e141)) +(flet ($e288 (xor $e160 $e266)) +(flet ($e289 (xor $e208 $e245)) +(flet ($e290 (or $e116 $e135)) +(flet ($e291 (xor $e202 $e225)) +(flet ($e292 (iff $e133 $e268)) +(flet ($e293 (xor $e179 $e278)) +(flet ($e294 (iff $e110 $e287)) +(flet ($e295 (not $e241)) +(flet ($e296 (and $e163 $e106)) +(flet ($e297 (xor $e265 $e122)) +(flet ($e298 (not $e295)) +(flet ($e299 (iff $e164 $e290)) +(flet ($e300 (and $e244 $e143)) +(flet ($e301 (xor $e238 $e189)) +(flet ($e302 (if_then_else $e15 $e284 $e260)) +(flet ($e303 (or $e259 $e297)) +(flet ($e304 (and $e197 $e190)) +(flet ($e305 (iff $e250 $e296)) +(flet ($e306 (implies $e153 $e118)) +(flet ($e307 (or $e288 $e270)) +(flet ($e308 (if_then_else $e298 $e221 $e253)) +(flet ($e309 (if_then_else $e111 $e23 $e170)) +(flet ($e310 (implies $e159 $e228)) +(flet ($e311 (not $e138)) +(flet ($e312 (or $e167 $e11)) +(flet ($e313 (xor $e279 $e289)) +(flet ($e314 (xor $e206 $e227)) +(flet ($e315 (or $e312 $e157)) +(flet ($e316 (xor $e261 $e313)) +(flet ($e317 (implies $e314 $e183)) +(flet ($e318 (or $e317 $e165)) +(flet ($e319 (implies $e22 $e175)) +(flet ($e320 (if_then_else $e213 $e293 $e293)) +(flet ($e321 (iff $e280 $e299)) +(flet ($e322 (not $e169)) +(flet ($e323 (or $e234 $e117)) +(flet ($e324 (not $e150)) +(flet ($e325 (if_then_else $e223 $e258 $e184)) +(flet ($e326 (xor $e237 $e178)) +(flet ($e327 (or $e307 $e19)) +(flet ($e328 (if_then_else $e303 $e192 $e274)) +(flet ($e329 (xor $e230 $e316)) +(flet ($e330 (implies $e239 $e24)) +(flet ($e331 (and $e324 $e154)) +(flet ($e332 (implies $e246 $e132)) +(flet ($e333 (implies $e121 $e128)) +(flet ($e334 (xor $e181 $e107)) +(flet ($e335 (xor $e322 $e321)) +(flet ($e336 (iff $e200 $e139)) +(flet ($e337 (and $e325 $e147)) +(flet ($e338 (iff $e220 $e166)) +(flet ($e339 (implies $e276 $e326)) +(flet ($e340 (if_then_else $e20 $e104 $e254)) +(flet ($e341 (not $e292)) +(flet ($e342 (implies $e306 $e335)) +(flet ($e343 (implies $e294 $e229)) +(flet ($e344 (or $e328 $e186)) +(flet ($e345 (if_then_else $e162 $e333 $e256)) +(flet ($e346 (iff $e125 $e217)) +(flet ($e347 (and $e345 $e336)) +(flet ($e348 (or $e271 $e251)) +(flet ($e349 (implies $e144 $e342)) +(flet ($e350 (if_then_else $e302 $e308 $e302)) +(flet ($e351 (xor $e182 $e347)) +(flet ($e352 (if_then_else $e18 $e188 $e343)) +(flet ($e353 (iff $e126 $e349)) +(flet ($e354 (or $e233 $e320)) +(flet ($e355 (implies $e215 $e341)) +(flet ($e356 (not $e211)) +(flet ($e357 (not $e344)) +(flet ($e358 (or $e334 $e309)) +(flet ($e359 (or $e315 $e337)) +(flet ($e360 (if_then_else $e277 $e155 $e283)) +(flet ($e361 (not $e339)) +(flet ($e362 (not $e232)) +(flet ($e363 (or $e123 $e142)) +(flet ($e364 (not $e363)) +(flet ($e365 (not $e353)) +(flet ($e366 (and $e124 $e231)) +(flet ($e367 (not $e161)) +(flet ($e368 (or $e364 $e137)) +(flet ($e369 (iff $e367 $e109)) +(flet ($e370 (xor $e360 $e310)) +(flet ($e371 (not $e362)) +(flet ($e372 (and $e357 $e331)) +(flet ($e373 (and $e252 $e207)) +(flet ($e374 (if_then_else $e140 $e140 $e115)) +(flet ($e375 (or $e291 $e214)) +(flet ($e376 (not $e351)) +(flet ($e377 (iff $e311 $e236)) +(flet ($e378 (if_then_else $e372 $e248 $e361)) +(flet ($e379 (xor $e374 $e350)) +(flet ($e380 (and $e216 $e370)) +(flet ($e381 (implies $e301 $e224)) +(flet ($e382 (iff $e379 $e130)) +(flet ($e383 (iff $e158 $e354)) +(flet ($e384 (not $e346)) +(flet ($e385 (or $e171 $e338)) +(flet ($e386 (xor $e191 $e378)) +(flet ($e387 (iff $e282 $e330)) +(flet ($e388 (and $e281 $e281)) +(flet ($e389 (implies $e387 $e318)) +(flet ($e390 (implies $e176 $e359)) +(flet ($e391 (and $e358 $e366)) +(flet ($e392 (implies $e365 $e371)) +(flet ($e393 (and $e383 $e340)) +(flet ($e394 (or $e390 $e369)) +(flet ($e395 (not $e389)) +(flet ($e396 (not $e323)) +(flet ($e397 (and $e394 $e193)) +(flet ($e398 (implies $e391 $e368)) +(flet ($e399 (iff $e395 $e398)) +(flet ($e400 (and $e392 $e129)) +(flet ($e401 (or $e17 $e399)) +(flet ($e402 (implies $e396 $e396)) +(flet ($e403 (iff $e401 $e386)) +(flet ($e404 (implies $e376 $e319)) +(flet ($e405 (if_then_else $e269 $e205 $e194)) +(flet ($e406 (and $e380 $e332)) +(flet ($e407 (xor $e402 $e403)) +(flet ($e408 (if_then_else $e329 $e113 $e382)) +(flet ($e409 (and $e286 $e187)) +(flet ($e410 (implies $e393 $e300)) +(flet ($e411 (implies $e388 $e355)) +(flet ($e412 (implies $e409 $e352)) +(flet ($e413 (implies $e397 $e405)) +(flet ($e414 (xor $e373 $e400)) +(flet ($e415 (not $e285)) +(flet ($e416 (not $e119)) +(flet ($e417 (not $e305)) +(flet ($e418 (xor $e348 $e408)) +(flet ($e419 (if_then_else $e149 $e304 $e415)) +(flet ($e420 (if_then_else $e407 $e377 $e419)) +(flet ($e421 (xor $e381 $e385)) +(flet ($e422 (not $e420)) +(flet ($e423 (iff $e422 $e411)) +(flet ($e424 (or $e375 $e404)) +(flet ($e425 (xor $e414 $e384)) +(flet ($e426 (implies $e327 $e406)) +(flet ($e427 (implies $e424 $e412)) +(flet ($e428 (implies $e421 $e417)) +(flet ($e429 (and $e427 $e413)) +(flet ($e430 (or $e410 $e356)) +(flet ($e431 (if_then_else $e429 $e425 $e418)) +(flet ($e432 (xor $e430 $e430)) +(flet ($e433 (iff $e431 $e426)) +(flet ($e434 (and $e432 $e423)) +(flet ($e435 (xor $e434 $e428)) +(flet ($e436 (xor $e433 $e433)) +(flet ($e437 (and $e416 $e435)) +(flet ($e438 (implies $e437 $e436)) +$e438 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect4.smt b/test/regress/regress0/arrays/incorrect4.smt new file mode 100644 index 000000000..62f28834a --- /dev/null +++ b/test/regress/regress0/arrays/incorrect4.smt @@ -0,0 +1,170 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Index)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v4 Element)) +:extrafuns ((v5 Element)) +:extrafuns ((v6 Element)) +:formula +(flet ($e7 (= v0 v0)) +(flet ($e8 (= v2 v2)) +(flet ($e9 (= v1 v2)) +(flet ($e10 (distinct v1 v2)) +(flet ($e11 (distinct v3 v2)) +(flet ($e12 (distinct v5 v5)) +(flet ($e13 (= v6 v4)) +(let (?e14 (ite $e9 v0 v0)) +(let (?e15 (ite $e7 v0 v0)) +(let (?e16 (ite $e11 ?e14 ?e15)) +(let (?e17 (ite $e8 ?e15 ?e15)) +(let (?e18 (ite $e10 ?e16 v0)) +(let (?e19 (ite $e9 ?e14 ?e15)) +(let (?e20 (ite $e12 ?e17 ?e19)) +(let (?e21 (ite $e8 ?e20 ?e16)) +(let (?e22 (ite $e13 ?e20 ?e16)) +(let (?e23 (ite $e10 v3 v1)) +(let (?e24 (ite $e13 v2 v3)) +(let (?e25 (ite $e11 v2 ?e23)) +(let (?e26 (ite $e12 v2 ?e23)) +(let (?e27 (ite $e8 ?e25 ?e23)) +(let (?e28 (ite $e7 v3 ?e26)) +(let (?e29 (ite $e9 ?e28 v1)) +(let (?e30 (ite $e8 v5 v5)) +(let (?e31 (ite $e10 v4 ?e30)) +(let (?e32 (ite $e11 v6 ?e30)) +(let (?e33 (ite $e7 ?e31 v4)) +(let (?e34 (ite $e10 ?e30 ?e32)) +(let (?e35 (ite $e9 v5 ?e32)) +(let (?e36 (ite $e12 ?e30 v4)) +(let (?e37 (ite $e11 v6 v4)) +(let (?e38 (ite $e12 ?e32 ?e33)) +(let (?e39 (ite $e8 v4 v6)) +(let (?e40 (ite $e13 ?e32 ?e33)) +(let (?e41 (store ?e17 v2 ?e33)) +(let (?e42 (select ?e41 v2)) +(flet ($e43 (= ?e17 ?e22)) +(flet ($e44 (distinct v0 ?e20)) +(flet ($e45 (= ?e14 ?e22)) +(flet ($e46 (= ?e17 ?e17)) +(flet ($e47 (distinct ?e21 ?e17)) +(flet ($e48 (= ?e41 ?e14)) +(flet ($e49 (distinct ?e19 ?e14)) +(flet ($e50 (= ?e14 ?e22)) +(flet ($e51 (= ?e20 ?e21)) +(flet ($e52 (= ?e14 ?e21)) +(flet ($e53 (= ?e19 ?e20)) +(flet ($e54 (= ?e22 ?e20)) +(flet ($e55 (= ?e15 ?e17)) +(flet ($e56 (= ?e16 ?e19)) +(flet ($e57 (= ?e16 ?e15)) +(flet ($e58 (distinct ?e41 ?e41)) +(flet ($e59 (distinct ?e20 ?e21)) +(flet ($e60 (distinct ?e17 ?e14)) +(flet ($e61 (distinct ?e15 ?e22)) +(flet ($e62 (distinct ?e22 ?e22)) +(flet ($e63 (= ?e18 v0)) +(flet ($e64 (= ?e27 ?e28)) +(flet ($e65 (distinct ?e23 v2)) +(flet ($e66 (= ?e23 ?e25)) +(flet ($e67 (distinct ?e24 ?e24)) +(flet ($e68 (distinct ?e28 ?e28)) +(flet ($e69 (= v1 ?e24)) +(flet ($e70 (= ?e29 ?e28)) +(flet ($e71 (distinct v3 ?e26)) +(flet ($e72 (distinct ?e36 ?e33)) +(flet ($e73 (distinct ?e30 v4)) +(flet ($e74 (= ?e39 ?e39)) +(flet ($e75 (= v4 ?e30)) +(flet ($e76 (= ?e33 ?e38)) +(flet ($e77 (= ?e34 ?e40)) +(flet ($e78 (= ?e36 ?e42)) +(flet ($e79 (distinct v4 ?e34)) +(flet ($e80 (distinct ?e30 ?e37)) +(flet ($e81 (= v6 ?e37)) +(flet ($e82 (= v5 ?e39)) +(flet ($e83 (distinct ?e35 ?e30)) +(flet ($e84 (distinct ?e39 ?e38)) +(flet ($e85 (distinct ?e32 ?e30)) +(flet ($e86 (= ?e42 ?e33)) +(flet ($e87 (distinct ?e36 v5)) +(flet ($e88 (distinct ?e30 ?e36)) +(flet ($e89 (= ?e42 v4)) +(flet ($e90 (distinct ?e42 ?e30)) +(flet ($e91 (distinct ?e36 v5)) +(flet ($e92 (= ?e34 ?e38)) +(flet ($e93 (distinct ?e42 v6)) +(flet ($e94 (distinct ?e37 ?e32)) +(flet ($e95 (distinct v6 ?e39)) +(flet ($e96 (= ?e35 ?e37)) +(flet ($e97 (= ?e42 ?e31)) +(flet ($e98 (implies $e89 $e93)) +(flet ($e99 (xor $e10 $e77)) +(flet ($e100 (or $e8 $e71)) +(flet ($e101 (iff $e7 $e43)) +(flet ($e102 (or $e46 $e54)) +(flet ($e103 (and $e78 $e50)) +(flet ($e104 (if_then_else $e67 $e58 $e82)) +(flet ($e105 (not $e85)) +(flet ($e106 (implies $e105 $e9)) +(flet ($e107 (xor $e83 $e66)) +(flet ($e108 (if_then_else $e53 $e57 $e107)) +(flet ($e109 (if_then_else $e97 $e13 $e106)) +(flet ($e110 (and $e60 $e79)) +(flet ($e111 (not $e99)) +(flet ($e112 (implies $e47 $e104)) +(flet ($e113 (and $e73 $e109)) +(flet ($e114 (or $e68 $e11)) +(flet ($e115 (xor $e44 $e96)) +(flet ($e116 (iff $e75 $e102)) +(flet ($e117 (if_then_else $e90 $e86 $e94)) +(flet ($e118 (xor $e62 $e70)) +(flet ($e119 (not $e113)) +(flet ($e120 (iff $e103 $e115)) +(flet ($e121 (or $e98 $e80)) +(flet ($e122 (not $e49)) +(flet ($e123 (or $e48 $e101)) +(flet ($e124 (xor $e108 $e123)) +(flet ($e125 (xor $e91 $e118)) +(flet ($e126 (xor $e56 $e84)) +(flet ($e127 (if_then_else $e110 $e114 $e117)) +(flet ($e128 (iff $e87 $e88)) +(flet ($e129 (implies $e95 $e127)) +(flet ($e130 (and $e52 $e116)) +(flet ($e131 (not $e69)) +(flet ($e132 (iff $e112 $e130)) +(flet ($e133 (or $e128 $e72)) +(flet ($e134 (if_then_else $e133 $e74 $e124)) +(flet ($e135 (implies $e55 $e51)) +(flet ($e136 (and $e126 $e61)) +(flet ($e137 (xor $e65 $e81)) +(flet ($e138 (or $e122 $e111)) +(flet ($e139 (or $e121 $e138)) +(flet ($e140 (implies $e119 $e136)) +(flet ($e141 (not $e140)) +(flet ($e142 (if_then_else $e12 $e59 $e132)) +(flet ($e143 (or $e142 $e129)) +(flet ($e144 (and $e45 $e63)) +(flet ($e145 (if_then_else $e76 $e141 $e131)) +(flet ($e146 (implies $e145 $e137)) +(flet ($e147 (if_then_else $e139 $e139 $e146)) +(flet ($e148 (xor $e144 $e147)) +(flet ($e149 (not $e120)) +(flet ($e150 (iff $e125 $e92)) +(flet ($e151 (or $e135 $e135)) +(flet ($e152 (or $e151 $e100)) +(flet ($e153 (implies $e149 $e152)) +(flet ($e154 (not $e134)) +(flet ($e155 (xor $e154 $e150)) +(flet ($e156 (if_then_else $e64 $e155 $e64)) +(flet ($e157 (or $e153 $e153)) +(flet ($e158 (not $e143)) +(flet ($e159 (and $e148 $e157)) +(flet ($e160 (xor $e159 $e159)) +(flet ($e161 (and $e156 $e158)) +(flet ($e162 (xor $e160 $e161)) +$e162 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect5.smt b/test/regress/regress0/arrays/incorrect5.smt new file mode 100644 index 000000000..a9c8d854c --- /dev/null +++ b/test/regress/regress0/arrays/incorrect5.smt @@ -0,0 +1,313 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Index)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v4 Element)) +:formula +(let (?e5 (store v0 v3 v4)) +(let (?e6 (select v0 v2)) +(let (?e7 (select ?e5 v2)) +(flet ($e8 (= v0 ?e5)) +(flet ($e9 (distinct v2 v1)) +(flet ($e10 (= v3 v2)) +(flet ($e11 (distinct ?e7 ?e7)) +(flet ($e12 (distinct ?e7 ?e7)) +(flet ($e13 (= ?e7 v4)) +(flet ($e14 (distinct ?e6 v4)) +(let (?e15 (ite $e12 ?e5 ?e5)) +(let (?e16 (ite $e13 ?e15 ?e5)) +(let (?e17 (ite $e13 ?e16 ?e5)) +(let (?e18 (ite $e11 ?e15 v0)) +(let (?e19 (ite $e8 ?e5 ?e18)) +(let (?e20 (ite $e10 ?e5 ?e15)) +(let (?e21 (ite $e9 ?e17 ?e5)) +(let (?e22 (ite $e10 ?e16 ?e15)) +(let (?e23 (ite $e14 ?e5 ?e16)) +(let (?e24 (ite $e14 v3 v3)) +(let (?e25 (ite $e10 v2 v1)) +(let (?e26 (ite $e13 ?e25 v1)) +(let (?e27 (ite $e11 v3 ?e24)) +(let (?e28 (ite $e12 ?e24 ?e27)) +(let (?e29 (ite $e9 v1 ?e28)) +(let (?e30 (ite $e12 ?e28 ?e28)) +(let (?e31 (ite $e11 ?e30 ?e25)) +(let (?e32 (ite $e12 v2 ?e27)) +(let (?e33 (ite $e8 ?e25 v2)) +(let (?e34 (ite $e8 ?e7 v4)) +(let (?e35 (ite $e12 ?e6 ?e6)) +(let (?e36 (ite $e11 ?e34 ?e35)) +(let (?e37 (ite $e14 ?e6 ?e6)) +(let (?e38 (ite $e10 v4 ?e34)) +(let (?e39 (ite $e13 ?e6 ?e37)) +(let (?e40 (ite $e10 ?e36 ?e36)) +(let (?e41 (ite $e14 v4 ?e37)) +(let (?e42 (ite $e13 ?e41 ?e37)) +(let (?e43 (ite $e9 ?e36 ?e6)) +(let (?e44 (store ?e16 ?e32 ?e37)) +(let (?e45 (select ?e15 v2)) +(let (?e46 (select ?e18 ?e33)) +(let (?e47 (store ?e44 ?e28 ?e39)) +(let (?e48 (select ?e20 v2)) +(flet ($e49 (distinct ?e44 ?e21)) +(flet ($e50 (= ?e18 ?e18)) +(flet ($e51 (distinct ?e44 ?e15)) +(flet ($e52 (distinct ?e21 ?e19)) +(flet ($e53 (= ?e47 v0)) +(flet ($e54 (distinct v0 ?e17)) +(flet ($e55 (= ?e21 ?e21)) +(flet ($e56 (= ?e19 ?e23)) +(flet ($e57 (= ?e44 ?e5)) +(flet ($e58 (= ?e17 ?e21)) +(flet ($e59 (= ?e44 ?e23)) +(flet ($e60 (distinct ?e47 ?e19)) +(flet ($e61 (distinct ?e5 ?e20)) +(flet ($e62 (distinct ?e20 ?e19)) +(flet ($e63 (= v0 ?e16)) +(flet ($e64 (distinct ?e16 ?e5)) +(flet ($e65 (distinct ?e44 ?e17)) +(flet ($e66 (= ?e5 ?e5)) +(flet ($e67 (distinct ?e47 ?e5)) +(flet ($e68 (distinct ?e19 ?e5)) +(flet ($e69 (distinct ?e18 ?e16)) +(flet ($e70 (= ?e18 ?e22)) +(flet ($e71 (distinct ?e29 v1)) +(flet ($e72 (distinct ?e26 ?e26)) +(flet ($e73 (distinct ?e27 ?e26)) +(flet ($e74 (distinct v3 ?e31)) +(flet ($e75 (= ?e25 ?e28)) +(flet ($e76 (= ?e32 v2)) +(flet ($e77 (= v1 ?e26)) +(flet ($e78 (= ?e32 ?e29)) +(flet ($e79 (distinct ?e24 ?e29)) +(flet ($e80 (= v2 ?e32)) +(flet ($e81 (= v2 ?e24)) +(flet ($e82 (distinct ?e32 ?e25)) +(flet ($e83 (= ?e31 v3)) +(flet ($e84 (= ?e29 ?e29)) +(flet ($e85 (distinct v3 v1)) +(flet ($e86 (= ?e28 ?e27)) +(flet ($e87 (distinct ?e27 ?e26)) +(flet ($e88 (distinct ?e26 ?e26)) +(flet ($e89 (distinct ?e29 v3)) +(flet ($e90 (= ?e26 ?e32)) +(flet ($e91 (= ?e30 v1)) +(flet ($e92 (= ?e31 ?e25)) +(flet ($e93 (= ?e32 v1)) +(flet ($e94 (distinct ?e26 ?e31)) +(flet ($e95 (distinct ?e29 ?e26)) +(flet ($e96 (= v3 v3)) +(flet ($e97 (= v2 ?e29)) +(flet ($e98 (distinct v3 v2)) +(flet ($e99 (= ?e29 v2)) +(flet ($e100 (distinct v1 v3)) +(flet ($e101 (= v2 ?e29)) +(flet ($e102 (distinct ?e24 ?e28)) +(flet ($e103 (= ?e31 ?e30)) +(flet ($e104 (distinct ?e32 ?e33)) +(flet ($e105 (= ?e34 v4)) +(flet ($e106 (= ?e43 ?e45)) +(flet ($e107 (= ?e48 ?e48)) +(flet ($e108 (= ?e46 ?e34)) +(flet ($e109 (= ?e40 ?e40)) +(flet ($e110 (= ?e35 ?e7)) +(flet ($e111 (distinct ?e37 ?e37)) +(flet ($e112 (= ?e34 ?e7)) +(flet ($e113 (= ?e37 ?e6)) +(flet ($e114 (= ?e48 ?e41)) +(flet ($e115 (distinct ?e6 ?e48)) +(flet ($e116 (distinct v4 ?e45)) +(flet ($e117 (distinct ?e45 ?e45)) +(flet ($e118 (distinct ?e42 ?e35)) +(flet ($e119 (distinct ?e37 ?e39)) +(flet ($e120 (distinct ?e6 ?e40)) +(flet ($e121 (= ?e34 ?e41)) +(flet ($e122 (distinct ?e37 ?e46)) +(flet ($e123 (= ?e7 ?e34)) +(flet ($e124 (= ?e35 ?e45)) +(flet ($e125 (= ?e40 ?e37)) +(flet ($e126 (= ?e39 ?e38)) +(flet ($e127 (= ?e46 ?e34)) +(flet ($e128 (= ?e42 ?e48)) +(flet ($e129 (= ?e34 ?e37)) +(flet ($e130 (distinct v4 v4)) +(flet ($e131 (= ?e41 ?e40)) +(flet ($e132 (distinct ?e43 ?e38)) +(flet ($e133 (distinct ?e39 ?e45)) +(flet ($e134 (distinct ?e42 v4)) +(flet ($e135 (= ?e48 ?e34)) +(flet ($e136 (distinct ?e38 ?e35)) +(flet ($e137 (= ?e41 ?e45)) +(flet ($e138 (distinct ?e7 ?e35)) +(flet ($e139 (= ?e7 ?e35)) +(flet ($e140 (= ?e46 ?e7)) +(flet ($e141 (distinct ?e45 v4)) +(flet ($e142 (= v4 ?e35)) +(flet ($e143 (= ?e48 ?e43)) +(flet ($e144 (= ?e37 ?e35)) +(flet ($e145 (distinct ?e34 v4)) +(flet ($e146 (distinct ?e35 ?e41)) +(flet ($e147 (= ?e40 ?e34)) +(flet ($e148 (= ?e46 ?e35)) +(flet ($e149 (= ?e43 ?e41)) +(flet ($e150 (= ?e39 ?e43)) +(flet ($e151 (distinct ?e41 ?e46)) +(flet ($e152 (= ?e7 ?e42)) +(flet ($e153 (distinct ?e43 ?e38)) +(flet ($e154 (distinct ?e37 ?e6)) +(flet ($e155 (= ?e7 ?e7)) +(flet ($e156 (distinct ?e43 ?e7)) +(flet ($e157 (= ?e43 ?e39)) +(flet ($e158 (distinct ?e43 ?e42)) +(flet ($e159 (= ?e39 ?e46)) +(flet ($e160 (distinct ?e41 ?e6)) +(flet ($e161 (= ?e7 ?e43)) +(flet ($e162 (= ?e39 ?e40)) +(flet ($e163 (distinct ?e42 v4)) +(flet ($e164 (distinct ?e35 v4)) +(flet ($e165 (= ?e40 ?e46)) +(flet ($e166 (distinct ?e45 ?e36)) +(flet ($e167 (iff $e137 $e129)) +(flet ($e168 (not $e106)) +(flet ($e169 (if_then_else $e86 $e140 $e85)) +(flet ($e170 (if_then_else $e136 $e56 $e69)) +(flet ($e171 (if_then_else $e169 $e79 $e100)) +(flet ($e172 (xor $e145 $e92)) +(flet ($e173 (implies $e64 $e101)) +(flet ($e174 (not $e171)) +(flet ($e175 (xor $e96 $e71)) +(flet ($e176 (and $e75 $e135)) +(flet ($e177 (or $e143 $e91)) +(flet ($e178 (not $e111)) +(flet ($e179 (if_then_else $e175 $e94 $e168)) +(flet ($e180 (not $e110)) +(flet ($e181 (or $e72 $e8)) +(flet ($e182 (not $e130)) +(flet ($e183 (iff $e10 $e88)) +(flet ($e184 (iff $e103 $e165)) +(flet ($e185 (xor $e76 $e13)) +(flet ($e186 (xor $e172 $e116)) +(flet ($e187 (iff $e180 $e102)) +(flet ($e188 (iff $e183 $e126)) +(flet ($e189 (iff $e121 $e186)) +(flet ($e190 (implies $e90 $e139)) +(flet ($e191 (iff $e124 $e58)) +(flet ($e192 (xor $e57 $e80)) +(flet ($e193 (xor $e133 $e164)) +(flet ($e194 (implies $e60 $e179)) +(flet ($e195 (iff $e170 $e87)) +(flet ($e196 (if_then_else $e63 $e107 $e189)) +(flet ($e197 (xor $e125 $e182)) +(flet ($e198 (implies $e55 $e141)) +(flet ($e199 (xor $e148 $e73)) +(flet ($e200 (iff $e195 $e74)) +(flet ($e201 (not $e67)) +(flet ($e202 (implies $e153 $e166)) +(flet ($e203 (iff $e190 $e118)) +(flet ($e204 (iff $e70 $e187)) +(flet ($e205 (implies $e152 $e131)) +(flet ($e206 (xor $e84 $e122)) +(flet ($e207 (or $e108 $e159)) +(flet ($e208 (implies $e12 $e196)) +(flet ($e209 (xor $e193 $e9)) +(flet ($e210 (implies $e146 $e138)) +(flet ($e211 (and $e194 $e147)) +(flet ($e212 (or $e104 $e65)) +(flet ($e213 (or $e54 $e200)) +(flet ($e214 (and $e114 $e157)) +(flet ($e215 (not $e158)) +(flet ($e216 (implies $e61 $e211)) +(flet ($e217 (implies $e109 $e151)) +(flet ($e218 (if_then_else $e199 $e134 $e132)) +(flet ($e219 (iff $e167 $e119)) +(flet ($e220 (and $e49 $e185)) +(flet ($e221 (or $e155 $e113)) +(flet ($e222 (not $e192)) +(flet ($e223 (not $e99)) +(flet ($e224 (if_then_else $e93 $e89 $e81)) +(flet ($e225 (and $e77 $e221)) +(flet ($e226 (if_then_else $e78 $e214 $e178)) +(flet ($e227 (and $e62 $e123)) +(flet ($e228 (and $e154 $e144)) +(flet ($e229 (xor $e14 $e225)) +(flet ($e230 (if_then_else $e163 $e217 $e163)) +(flet ($e231 (not $e230)) +(flet ($e232 (implies $e174 $e11)) +(flet ($e233 (not $e52)) +(flet ($e234 (if_then_else $e160 $e117 $e53)) +(flet ($e235 (not $e105)) +(flet ($e236 (iff $e51 $e177)) +(flet ($e237 (iff $e203 $e176)) +(flet ($e238 (if_then_else $e120 $e233 $e207)) +(flet ($e239 (or $e50 $e59)) +(flet ($e240 (xor $e115 $e181)) +(flet ($e241 (xor $e112 $e68)) +(flet ($e242 (if_then_else $e236 $e97 $e227)) +(flet ($e243 (not $e66)) +(flet ($e244 (not $e98)) +(flet ($e245 (not $e234)) +(flet ($e246 (if_then_else $e238 $e127 $e184)) +(flet ($e247 (not $e215)) +(flet ($e248 (implies $e224 $e209)) +(flet ($e249 (xor $e220 $e229)) +(flet ($e250 (if_then_else $e128 $e128 $e149)) +(flet ($e251 (implies $e208 $e161)) +(flet ($e252 (or $e222 $e240)) +(flet ($e253 (xor $e201 $e218)) +(flet ($e254 (xor $e232 $e251)) +(flet ($e255 (xor $e244 $e250)) +(flet ($e256 (iff $e249 $e212)) +(flet ($e257 (if_then_else $e142 $e255 $e253)) +(flet ($e258 (if_then_else $e256 $e228 $e198)) +(flet ($e259 (xor $e156 $e243)) +(flet ($e260 (implies $e239 $e242)) +(flet ($e261 (or $e257 $e206)) +(flet ($e262 (and $e204 $e150)) +(flet ($e263 (not $e248)) +(flet ($e264 (and $e258 $e202)) +(flet ($e265 (and $e226 $e247)) +(flet ($e266 (implies $e162 $e265)) +(flet ($e267 (if_then_else $e213 $e173 $e213)) +(flet ($e268 (xor $e246 $e267)) +(flet ($e269 (implies $e252 $e262)) +(flet ($e270 (or $e205 $e223)) +(flet ($e271 (not $e188)) +(flet ($e272 (not $e260)) +(flet ($e273 (and $e219 $e263)) +(flet ($e274 (xor $e95 $e259)) +(flet ($e275 (or $e191 $e191)) +(flet ($e276 (or $e197 $e261)) +(flet ($e277 (and $e216 $e254)) +(flet ($e278 (or $e276 $e264)) +(flet ($e279 (iff $e271 $e237)) +(flet ($e280 (iff $e279 $e269)) +(flet ($e281 (xor $e270 $e210)) +(flet ($e282 (and $e281 $e241)) +(flet ($e283 (and $e235 $e235)) +(flet ($e284 (xor $e283 $e283)) +(flet ($e285 (and $e83 $e277)) +(flet ($e286 (iff $e231 $e278)) +(flet ($e287 (implies $e272 $e275)) +(flet ($e288 (not $e273)) +(flet ($e289 (not $e245)) +(flet ($e290 (and $e274 $e282)) +(flet ($e291 (implies $e266 $e280)) +(flet ($e292 (implies $e288 $e287)) +(flet ($e293 (not $e268)) +(flet ($e294 (xor $e293 $e284)) +(flet ($e295 (if_then_else $e82 $e285 $e290)) +(flet ($e296 (or $e291 $e295)) +(flet ($e297 (not $e286)) +(flet ($e298 (implies $e292 $e292)) +(flet ($e299 (and $e294 $e297)) +(flet ($e300 (implies $e299 $e299)) +(flet ($e301 (xor $e298 $e300)) +(flet ($e302 (if_then_else $e301 $e289 $e289)) +(flet ($e303 (not $e296)) +(flet ($e304 (implies $e302 $e302)) +(flet ($e305 (implies $e304 $e303)) +$e305 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect6.smt b/test/regress/regress0/arrays/incorrect6.smt new file mode 100644 index 000000000..5e9de90aa --- /dev/null +++ b/test/regress/regress0/arrays/incorrect6.smt @@ -0,0 +1,265 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Array)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v4 Element)) +:extrafuns ((v5 Element)) +:extrafuns ((v6 Element)) +:extrafuns ((v7 Element)) +:extrafuns ((v8 Element)) +:formula +(let (?e9 (select v0 v3)) +(flet ($e10 (= v0 v1)) +(flet ($e11 (distinct v2 v2)) +(flet ($e12 (= v3 v2)) +(flet ($e13 (distinct ?e9 v5)) +(flet ($e14 (= ?e9 v6)) +(flet ($e15 (= ?e9 ?e9)) +(flet ($e16 (= v4 v8)) +(flet ($e17 (= v4 v8)) +(flet ($e18 (= v8 v6)) +(flet ($e19 (= ?e9 v5)) +(flet ($e20 (distinct v7 v5)) +(let (?e21 (ite $e20 v0 v0)) +(let (?e22 (ite $e20 ?e21 ?e21)) +(let (?e23 (ite $e11 v1 v0)) +(let (?e24 (ite $e17 ?e22 ?e22)) +(let (?e25 (ite $e10 ?e22 ?e23)) +(let (?e26 (ite $e17 ?e24 v0)) +(let (?e27 (ite $e16 v0 v1)) +(let (?e28 (ite $e13 v1 ?e22)) +(let (?e29 (ite $e18 ?e26 ?e26)) +(let (?e30 (ite $e12 ?e24 ?e28)) +(let (?e31 (ite $e19 ?e27 ?e28)) +(let (?e32 (ite $e15 ?e29 ?e25)) +(let (?e33 (ite $e14 ?e26 ?e26)) +(let (?e34 (ite $e12 v2 v3)) +(let (?e35 (ite $e13 ?e34 ?e34)) +(let (?e36 (ite $e16 v3 v3)) +(let (?e37 (ite $e10 ?e34 ?e34)) +(let (?e38 (ite $e11 ?e35 v2)) +(let (?e39 (ite $e19 ?e34 ?e37)) +(let (?e40 (ite $e14 ?e35 ?e34)) +(let (?e41 (ite $e20 ?e40 v3)) +(let (?e42 (ite $e17 ?e39 ?e36)) +(let (?e43 (ite $e20 ?e40 v2)) +(let (?e44 (ite $e15 ?e43 v2)) +(let (?e45 (ite $e18 ?e43 v2)) +(let (?e46 (ite $e11 v6 v7)) +(let (?e47 (ite $e19 v5 v6)) +(let (?e48 (ite $e10 v8 v5)) +(let (?e49 (ite $e11 v6 ?e48)) +(let (?e50 (ite $e15 ?e9 ?e49)) +(let (?e51 (ite $e15 v4 v4)) +(let (?e52 (ite $e12 ?e50 ?e47)) +(let (?e53 (ite $e13 v6 ?e51)) +(let (?e54 (ite $e18 ?e49 ?e46)) +(let (?e55 (ite $e20 ?e9 ?e50)) +(let (?e56 (ite $e17 ?e53 ?e52)) +(let (?e57 (ite $e14 ?e47 ?e9)) +(let (?e58 (ite $e16 ?e48 ?e52)) +(let (?e59 (select ?e23 ?e39)) +(flet ($e60 (distinct v1 ?e22)) +(flet ($e61 (= ?e25 ?e25)) +(flet ($e62 (distinct ?e32 ?e27)) +(flet ($e63 (distinct ?e31 ?e25)) +(flet ($e64 (distinct ?e22 ?e28)) +(flet ($e65 (= v1 ?e28)) +(flet ($e66 (distinct ?e25 ?e28)) +(flet ($e67 (= v1 ?e25)) +(flet ($e68 (= ?e30 v0)) +(flet ($e69 (distinct ?e25 ?e23)) +(flet ($e70 (distinct ?e21 ?e24)) +(flet ($e71 (= ?e30 ?e25)) +(flet ($e72 (distinct ?e21 v0)) +(flet ($e73 (distinct v1 ?e29)) +(flet ($e74 (distinct ?e32 ?e31)) +(flet ($e75 (distinct ?e25 ?e23)) +(flet ($e76 (= ?e32 ?e21)) +(flet ($e77 (distinct ?e32 ?e31)) +(flet ($e78 (distinct ?e28 ?e24)) +(flet ($e79 (distinct v1 ?e26)) +(flet ($e80 (distinct v1 ?e23)) +(flet ($e81 (distinct v1 v0)) +(flet ($e82 (= ?e29 v1)) +(flet ($e83 (distinct ?e29 ?e22)) +(flet ($e84 (distinct v0 ?e29)) +(flet ($e85 (= ?e28 ?e27)) +(flet ($e86 (distinct ?e25 ?e21)) +(flet ($e87 (distinct ?e28 ?e25)) +(flet ($e88 (= ?e29 ?e21)) +(flet ($e89 (= ?e31 ?e33)) +(flet ($e90 (distinct ?e45 ?e35)) +(flet ($e91 (= ?e37 v3)) +(flet ($e92 (distinct ?e43 ?e35)) +(flet ($e93 (distinct v2 v3)) +(flet ($e94 (distinct ?e40 ?e45)) +(flet ($e95 (distinct ?e38 v3)) +(flet ($e96 (distinct ?e43 ?e37)) +(flet ($e97 (= ?e36 ?e44)) +(flet ($e98 (= ?e39 ?e36)) +(flet ($e99 (distinct ?e38 ?e44)) +(flet ($e100 (distinct ?e44 ?e34)) +(flet ($e101 (distinct ?e43 ?e40)) +(flet ($e102 (distinct v2 v3)) +(flet ($e103 (= ?e43 ?e41)) +(flet ($e104 (= ?e38 ?e40)) +(flet ($e105 (= v3 ?e37)) +(flet ($e106 (= v2 ?e44)) +(flet ($e107 (distinct ?e34 ?e45)) +(flet ($e108 (distinct ?e39 ?e37)) +(flet ($e109 (= ?e36 ?e38)) +(flet ($e110 (= v3 ?e38)) +(flet ($e111 (= ?e39 v3)) +(flet ($e112 (distinct ?e44 ?e45)) +(flet ($e113 (distinct ?e41 ?e40)) +(flet ($e114 (= ?e38 ?e40)) +(flet ($e115 (distinct ?e44 ?e38)) +(flet ($e116 (distinct ?e37 ?e44)) +(flet ($e117 (distinct ?e34 ?e39)) +(flet ($e118 (distinct ?e37 ?e40)) +(flet ($e119 (distinct ?e37 ?e36)) +(flet ($e120 (distinct ?e45 ?e42)) +(flet ($e121 (distinct ?e58 ?e48)) +(flet ($e122 (distinct ?e9 v7)) +(flet ($e123 (distinct v7 v4)) +(flet ($e124 (= ?e59 ?e59)) +(flet ($e125 (= ?e46 ?e49)) +(flet ($e126 (distinct ?e58 ?e48)) +(flet ($e127 (distinct ?e53 ?e46)) +(flet ($e128 (distinct v4 ?e47)) +(flet ($e129 (distinct v4 v5)) +(flet ($e130 (= v7 ?e49)) +(flet ($e131 (distinct v8 v6)) +(flet ($e132 (= ?e48 ?e51)) +(flet ($e133 (distinct ?e51 ?e47)) +(flet ($e134 (= ?e55 ?e49)) +(flet ($e135 (= ?e54 ?e58)) +(flet ($e136 (distinct ?e47 ?e57)) +(flet ($e137 (= ?e48 v4)) +(flet ($e138 (= ?e48 ?e55)) +(flet ($e139 (distinct v8 ?e48)) +(flet ($e140 (distinct ?e55 v7)) +(flet ($e141 (= v4 v6)) +(flet ($e142 (distinct ?e56 ?e53)) +(flet ($e143 (distinct ?e58 ?e49)) +(flet ($e144 (distinct ?e50 v5)) +(flet ($e145 (distinct ?e58 ?e47)) +(flet ($e146 (distinct v8 ?e56)) +(flet ($e147 (= ?e50 ?e52)) +(flet ($e148 (xor $e19 $e117)) +(flet ($e149 (or $e106 $e64)) +(flet ($e150 (or $e74 $e14)) +(flet ($e151 (or $e127 $e110)) +(flet ($e152 (iff $e140 $e113)) +(flet ($e153 (implies $e71 $e144)) +(flet ($e154 (iff $e142 $e85)) +(flet ($e155 (implies $e13 $e13)) +(flet ($e156 (not $e118)) +(flet ($e157 (if_then_else $e123 $e62 $e95)) +(flet ($e158 (implies $e63 $e101)) +(flet ($e159 (iff $e77 $e125)) +(flet ($e160 (or $e73 $e80)) +(flet ($e161 (if_then_else $e143 $e99 $e107)) +(flet ($e162 (iff $e72 $e102)) +(flet ($e163 (or $e100 $e126)) +(flet ($e164 (or $e91 $e162)) +(flet ($e165 (iff $e11 $e75)) +(flet ($e166 (and $e84 $e158)) +(flet ($e167 (or $e16 $e60)) +(flet ($e168 (implies $e149 $e137)) +(flet ($e169 (not $e109)) +(flet ($e170 (and $e61 $e145)) +(flet ($e171 (and $e121 $e68)) +(flet ($e172 (and $e120 $e124)) +(flet ($e173 (and $e165 $e90)) +(flet ($e174 (implies $e168 $e166)) +(flet ($e175 (or $e174 $e173)) +(flet ($e176 (xor $e114 $e105)) +(flet ($e177 (xor $e97 $e66)) +(flet ($e178 (xor $e128 $e122)) +(flet ($e179 (xor $e167 $e176)) +(flet ($e180 (iff $e177 $e108)) +(flet ($e181 (not $e159)) +(flet ($e182 (iff $e178 $e138)) +(flet ($e183 (or $e98 $e169)) +(flet ($e184 (iff $e87 $e83)) +(flet ($e185 (not $e12)) +(flet ($e186 (and $e78 $e151)) +(flet ($e187 (not $e69)) +(flet ($e188 (xor $e94 $e88)) +(flet ($e189 (and $e81 $e141)) +(flet ($e190 (or $e96 $e184)) +(flet ($e191 (iff $e116 $e103)) +(flet ($e192 (or $e147 $e136)) +(flet ($e193 (if_then_else $e179 $e89 $e139)) +(flet ($e194 (implies $e193 $e134)) +(flet ($e195 (iff $e191 $e10)) +(flet ($e196 (iff $e152 $e190)) +(flet ($e197 (iff $e163 $e161)) +(flet ($e198 (iff $e170 $e129)) +(flet ($e199 (or $e195 $e67)) +(flet ($e200 (not $e164)) +(flet ($e201 (and $e104 $e192)) +(flet ($e202 (iff $e65 $e150)) +(flet ($e203 (xor $e200 $e70)) +(flet ($e204 (and $e183 $e79)) +(flet ($e205 (or $e185 $e172)) +(flet ($e206 (not $e18)) +(flet ($e207 (implies $e181 $e198)) +(flet ($e208 (not $e189)) +(flet ($e209 (xor $e171 $e203)) +(flet ($e210 (not $e201)) +(flet ($e211 (implies $e196 $e206)) +(flet ($e212 (iff $e211 $e182)) +(flet ($e213 (implies $e155 $e132)) +(flet ($e214 (if_then_else $e199 $e205 $e148)) +(flet ($e215 (xor $e154 $e86)) +(flet ($e216 (not $e119)) +(flet ($e217 (implies $e20 $e133)) +(flet ($e218 (if_then_else $e215 $e180 $e15)) +(flet ($e219 (implies $e197 $e112)) +(flet ($e220 (implies $e156 $e115)) +(flet ($e221 (and $e204 $e212)) +(flet ($e222 (if_then_else $e220 $e214 $e209)) +(flet ($e223 (implies $e218 $e213)) +(flet ($e224 (if_then_else $e93 $e221 $e130)) +(flet ($e225 (and $e223 $e222)) +(flet ($e226 (xor $e202 $e17)) +(flet ($e227 (not $e225)) +(flet ($e228 (if_then_else $e208 $e210 $e207)) +(flet ($e229 (or $e135 $e131)) +(flet ($e230 (not $e157)) +(flet ($e231 (and $e216 $e216)) +(flet ($e232 (or $e229 $e82)) +(flet ($e233 (implies $e187 $e160)) +(flet ($e234 (implies $e76 $e219)) +(flet ($e235 (not $e186)) +(flet ($e236 (xor $e230 $e188)) +(flet ($e237 (xor $e146 $e227)) +(flet ($e238 (implies $e235 $e235)) +(flet ($e239 (or $e92 $e232)) +(flet ($e240 (implies $e236 $e228)) +(flet ($e241 (not $e217)) +(flet ($e242 (or $e237 $e238)) +(flet ($e243 (implies $e233 $e241)) +(flet ($e244 (iff $e175 $e224)) +(flet ($e245 (if_then_else $e239 $e242 $e244)) +(flet ($e246 (xor $e153 $e234)) +(flet ($e247 (if_then_else $e194 $e246 $e226)) +(flet ($e248 (implies $e247 $e247)) +(flet ($e249 (or $e240 $e245)) +(flet ($e250 (xor $e248 $e111)) +(flet ($e251 (implies $e249 $e249)) +(flet ($e252 (iff $e243 $e243)) +(flet ($e253 (xor $e251 $e251)) +(flet ($e254 (iff $e253 $e253)) +(flet ($e255 (if_then_else $e250 $e254 $e254)) +(flet ($e256 (iff $e255 $e252)) +(flet ($e257 (xor $e231 $e256)) +$e257 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect7.smt b/test/regress/regress0/arrays/incorrect7.smt new file mode 100644 index 000000000..4b406f964 --- /dev/null +++ b/test/regress/regress0/arrays/incorrect7.smt @@ -0,0 +1,80 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Array)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Element)) +:extrafuns ((v4 Element)) +:formula +(flet ($e5 (distinct v0 v0)) +(flet ($e6 (distinct v0 v1)) +(flet ($e7 (distinct v2 v2)) +(flet ($e8 (distinct v3 v4)) +(let (?e9 (ite $e5 v1 v1)) +(let (?e10 (ite $e7 ?e9 v0)) +(let (?e11 (ite $e6 ?e10 v0)) +(let (?e12 (ite $e8 v1 v0)) +(let (?e13 (ite $e8 v2 v2)) +(let (?e14 (ite $e7 ?e13 ?e13)) +(let (?e15 (ite $e5 ?e13 ?e14)) +(let (?e16 (ite $e7 v2 ?e13)) +(let (?e17 (ite $e6 v2 ?e13)) +(let (?e18 (ite $e7 v3 v4)) +(let (?e19 (ite $e8 ?e18 v3)) +(let (?e20 (ite $e6 v3 v4)) +(let (?e21 (ite $e8 ?e19 v4)) +(let (?e22 (ite $e6 ?e20 ?e18)) +(let (?e23 (ite $e5 ?e22 ?e21)) +(let (?e24 (store ?e9 ?e17 ?e23)) +(let (?e25 (select ?e11 ?e15)) +(flet ($e26 (= ?e11 ?e12)) +(flet ($e27 (= ?e11 ?e11)) +(flet ($e28 (= ?e12 ?e11)) +(flet ($e29 (= v0 ?e9)) +(flet ($e30 (= ?e9 v1)) +(flet ($e31 (distinct ?e10 v1)) +(flet ($e32 (= ?e12 ?e24)) +(flet ($e33 (distinct ?e17 ?e14)) +(flet ($e34 (distinct v2 ?e17)) +(flet ($e35 (= ?e13 v2)) +(flet ($e36 (distinct ?e15 ?e16)) +(flet ($e37 (= v4 ?e22)) +(flet ($e38 (distinct v4 ?e18)) +(flet ($e39 (= ?e22 ?e23)) +(flet ($e40 (= ?e23 ?e20)) +(flet ($e41 (distinct ?e21 ?e22)) +(flet ($e42 (= ?e21 ?e23)) +(flet ($e43 (distinct ?e23 v4)) +(flet ($e44 (distinct v4 v3)) +(flet ($e45 (= ?e21 ?e19)) +(flet ($e46 (= ?e22 ?e22)) +(flet ($e47 (distinct ?e20 ?e25)) +(flet ($e48 (not $e7)) +(flet ($e49 (not $e33)) +(flet ($e50 (iff $e35 $e39)) +(flet ($e51 (xor $e28 $e42)) +(flet ($e52 (xor $e31 $e38)) +(flet ($e53 (implies $e46 $e36)) +(flet ($e54 (or $e50 $e37)) +(flet ($e55 (or $e52 $e5)) +(flet ($e56 (and $e34 $e55)) +(flet ($e57 (iff $e47 $e8)) +(flet ($e58 (implies $e48 $e44)) +(flet ($e59 (iff $e45 $e57)) +(flet ($e60 (iff $e41 $e29)) +(flet ($e61 (if_then_else $e58 $e40 $e27)) +(flet ($e62 (iff $e53 $e59)) +(flet ($e63 (if_then_else $e32 $e26 $e54)) +(flet ($e64 (xor $e51 $e60)) +(flet ($e65 (iff $e62 $e6)) +(flet ($e66 (implies $e64 $e49)) +(flet ($e67 (or $e63 $e65)) +(flet ($e68 (if_then_else $e30 $e66 $e61)) +(flet ($e69 (or $e56 $e68)) +(flet ($e70 (and $e69 $e43)) +(flet ($e71 (iff $e67 $e67)) +(flet ($e72 (and $e70 $e71)) +$e72 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect8.smt b/test/regress/regress0/arrays/incorrect8.smt new file mode 100644 index 000000000..a118fec1d --- /dev/null +++ b/test/regress/regress0/arrays/incorrect8.smt @@ -0,0 +1,491 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Array)) +:extrafuns ((v2 Array)) +:extrafuns ((v3 Index)) +:extrafuns ((v4 Index)) +:extrafuns ((v5 Element)) +:formula +(let (?e6 (store v1 v4 v5)) +(let (?e7 (store ?e6 v4 v5)) +(let (?e8 (select v0 v3)) +(let (?e9 (select ?e6 v3)) +(let (?e10 (select v0 v3)) +(let (?e11 (store ?e7 v3 ?e8)) +(let (?e12 (select ?e7 v3)) +(let (?e13 (store ?e7 v3 ?e8)) +(let (?e14 (select v1 v3)) +(flet ($e15 (distinct ?e13 ?e13)) +(flet ($e16 (distinct v2 ?e6)) +(flet ($e17 (distinct v1 v2)) +(flet ($e18 (= v2 ?e7)) +(flet ($e19 (= v0 v0)) +(flet ($e20 (distinct ?e13 v2)) +(flet ($e21 (= ?e6 ?e6)) +(flet ($e22 (distinct ?e11 ?e13)) +(flet ($e23 (= v3 v3)) +(flet ($e24 (= v3 v3)) +(flet ($e25 (distinct v3 v3)) +(flet ($e26 (distinct v4 v3)) +(flet ($e27 (distinct ?e9 ?e14)) +(flet ($e28 (= ?e9 v5)) +(flet ($e29 (= ?e12 v5)) +(flet ($e30 (distinct ?e10 ?e10)) +(flet ($e31 (= ?e12 ?e9)) +(flet ($e32 (= ?e10 ?e10)) +(flet ($e33 (= ?e12 v5)) +(flet ($e34 (= ?e8 ?e8)) +(let (?e35 (ite $e24 ?e6 ?e11)) +(let (?e36 (ite $e17 ?e35 ?e6)) +(let (?e37 (ite $e23 v2 v2)) +(let (?e38 (ite $e31 ?e35 ?e36)) +(let (?e39 (ite $e16 ?e36 ?e38)) +(let (?e40 (ite $e15 v2 v2)) +(let (?e41 (ite $e28 ?e7 ?e36)) +(let (?e42 (ite $e22 ?e7 ?e13)) +(let (?e43 (ite $e34 ?e38 v1)) +(let (?e44 (ite $e33 v0 v1)) +(let (?e45 (ite $e21 ?e44 v1)) +(let (?e46 (ite $e18 ?e35 ?e11)) +(let (?e47 (ite $e19 ?e44 ?e43)) +(let (?e48 (ite $e27 ?e37 v1)) +(let (?e49 (ite $e17 v2 ?e48)) +(let (?e50 (ite $e28 ?e37 v2)) +(let (?e51 (ite $e29 ?e42 ?e41)) +(let (?e52 (ite $e23 ?e49 v2)) +(let (?e53 (ite $e16 ?e47 ?e35)) +(let (?e54 (ite $e25 ?e45 ?e41)) +(let (?e55 (ite $e23 ?e41 ?e45)) +(let (?e56 (ite $e32 ?e6 ?e51)) +(let (?e57 (ite $e34 ?e39 v2)) +(let (?e58 (ite $e27 ?e49 ?e13)) +(let (?e59 (ite $e26 ?e55 ?e53)) +(let (?e60 (ite $e22 ?e37 ?e36)) +(let (?e61 (ite $e26 ?e50 ?e46)) +(let (?e62 (ite $e29 ?e47 ?e61)) +(let (?e63 (ite $e16 ?e59 ?e53)) +(let (?e64 (ite $e20 ?e55 ?e56)) +(let (?e65 (ite $e30 ?e42 ?e52)) +(let (?e66 (ite $e21 v3 v3)) +(let (?e67 (ite $e26 v3 v3)) +(let (?e68 (ite $e28 v4 v4)) +(let (?e69 (ite $e33 ?e67 ?e66)) +(let (?e70 (ite $e18 v4 ?e69)) +(let (?e71 (ite $e17 v3 ?e67)) +(let (?e72 (ite $e23 v3 ?e71)) +(let (?e73 (ite $e27 ?e68 ?e67)) +(let (?e74 (ite $e29 v4 ?e73)) +(let (?e75 (ite $e24 ?e70 ?e72)) +(let (?e76 (ite $e32 ?e73 ?e75)) +(let (?e77 (ite $e17 ?e75 v4)) +(let (?e78 (ite $e25 ?e68 ?e72)) +(let (?e79 (ite $e30 v4 ?e77)) +(let (?e80 (ite $e19 v3 ?e70)) +(let (?e81 (ite $e15 ?e66 v3)) +(let (?e82 (ite $e16 ?e72 ?e76)) +(let (?e83 (ite $e21 ?e70 ?e75)) +(let (?e84 (ite $e23 ?e70 ?e66)) +(let (?e85 (ite $e31 ?e81 ?e74)) +(let (?e86 (ite $e22 ?e69 ?e84)) +(let (?e87 (ite $e34 ?e73 v3)) +(let (?e88 (ite $e20 ?e79 ?e67)) +(let (?e89 (ite $e28 ?e12 ?e9)) +(let (?e90 (ite $e17 ?e10 v5)) +(let (?e91 (ite $e21 ?e8 ?e14)) +(let (?e92 (ite $e23 ?e10 v5)) +(let (?e93 (ite $e24 ?e90 ?e9)) +(let (?e94 (ite $e16 ?e90 ?e10)) +(let (?e95 (ite $e32 ?e8 ?e14)) +(let (?e96 (ite $e18 ?e94 ?e92)) +(let (?e97 (ite $e34 ?e8 ?e14)) +(let (?e98 (ite $e25 ?e90 ?e91)) +(let (?e99 (ite $e15 v5 ?e10)) +(let (?e100 (ite $e31 ?e98 ?e94)) +(let (?e101 (ite $e21 ?e90 ?e14)) +(let (?e102 (ite $e20 ?e95 ?e10)) +(let (?e103 (ite $e22 ?e10 ?e92)) +(let (?e104 (ite $e17 ?e97 ?e94)) +(let (?e105 (ite $e27 ?e102 ?e97)) +(let (?e106 (ite $e29 ?e14 ?e8)) +(let (?e107 (ite $e33 ?e105 ?e95)) +(let (?e108 (ite $e19 ?e100 ?e100)) +(let (?e109 (ite $e19 ?e93 v5)) +(let (?e110 (ite $e30 ?e90 ?e95)) +(let (?e111 (ite $e26 ?e93 ?e108)) +(let (?e112 (store v2 ?e67 ?e100)) +(let (?e113 (store ?e57 ?e80 ?e92)) +(let (?e114 (store ?e52 ?e75 ?e97)) +(let (?e115 (select ?e54 ?e87)) +(let (?e116 (select ?e51 v3)) +(let (?e117 (select ?e13 ?e71)) +(let (?e118 (store ?e112 ?e85 ?e93)) +(let (?e119 (select ?e62 ?e75)) +(let (?e120 (store ?e45 ?e81 ?e91)) +(let (?e121 (select ?e56 ?e76)) +(flet ($e122 (= ?e58 ?e56)) +(flet ($e123 (distinct ?e60 ?e49)) +(flet ($e124 (= ?e62 ?e46)) +(flet ($e125 (= ?e54 ?e113)) +(flet ($e126 (= ?e61 ?e47)) +(flet ($e127 (distinct ?e36 ?e113)) +(flet ($e128 (= ?e40 ?e38)) +(flet ($e129 (= ?e62 ?e112)) +(flet ($e130 (distinct ?e56 ?e65)) +(flet ($e131 (distinct ?e35 ?e114)) +(flet ($e132 (= ?e35 ?e63)) +(flet ($e133 (distinct ?e53 ?e114)) +(flet ($e134 (distinct ?e36 ?e6)) +(flet ($e135 (= ?e51 ?e53)) +(flet ($e136 (= ?e118 ?e61)) +(flet ($e137 (= ?e120 ?e37)) +(flet ($e138 (= ?e35 ?e63)) +(flet ($e139 (= ?e13 ?e57)) +(flet ($e140 (= ?e46 ?e65)) +(flet ($e141 (= ?e120 ?e13)) +(flet ($e142 (= ?e45 ?e51)) +(flet ($e143 (distinct v0 ?e64)) +(flet ($e144 (distinct ?e41 ?e56)) +(flet ($e145 (distinct ?e46 ?e38)) +(flet ($e146 (= v0 ?e38)) +(flet ($e147 (= ?e47 v0)) +(flet ($e148 (distinct ?e47 ?e7)) +(flet ($e149 (distinct ?e56 ?e58)) +(flet ($e150 (= ?e58 ?e52)) +(flet ($e151 (distinct ?e11 ?e55)) +(flet ($e152 (distinct ?e60 ?e57)) +(flet ($e153 (= ?e44 ?e120)) +(flet ($e154 (distinct ?e48 ?e40)) +(flet ($e155 (= ?e46 ?e53)) +(flet ($e156 (distinct ?e44 ?e49)) +(flet ($e157 (distinct v0 ?e13)) +(flet ($e158 (distinct ?e51 ?e56)) +(flet ($e159 (distinct ?e62 ?e13)) +(flet ($e160 (= ?e61 ?e47)) +(flet ($e161 (distinct v2 ?e47)) +(flet ($e162 (distinct ?e52 ?e35)) +(flet ($e163 (= ?e43 ?e48)) +(flet ($e164 (= ?e47 ?e113)) +(flet ($e165 (= ?e112 ?e6)) +(flet ($e166 (distinct ?e52 ?e47)) +(flet ($e167 (distinct ?e41 ?e51)) +(flet ($e168 (= ?e45 ?e55)) +(flet ($e169 (distinct ?e48 ?e58)) +(flet ($e170 (= ?e58 ?e112)) +(flet ($e171 (= ?e58 ?e57)) +(flet ($e172 (= ?e11 ?e39)) +(flet ($e173 (distinct ?e114 ?e54)) +(flet ($e174 (= ?e58 ?e52)) +(flet ($e175 (distinct ?e58 ?e65)) +(flet ($e176 (= v0 ?e11)) +(flet ($e177 (distinct ?e118 ?e38)) +(flet ($e178 (distinct v1 ?e48)) +(flet ($e179 (distinct ?e53 ?e59)) +(flet ($e180 (= ?e11 ?e49)) +(flet ($e181 (= ?e120 ?e42)) +(flet ($e182 (= ?e61 ?e45)) +(flet ($e183 (= ?e42 ?e65)) +(flet ($e184 (= ?e58 ?e57)) +(flet ($e185 (distinct ?e46 ?e51)) +(flet ($e186 (= ?e42 ?e113)) +(flet ($e187 (distinct ?e37 ?e64)) +(flet ($e188 (distinct ?e63 ?e37)) +(flet ($e189 (distinct ?e43 v1)) +(flet ($e190 (distinct ?e62 ?e51)) +(flet ($e191 (= ?e50 ?e6)) +(flet ($e192 (distinct ?e73 ?e83)) +(flet ($e193 (distinct ?e83 ?e76)) +(flet ($e194 (distinct ?e81 ?e87)) +(flet ($e195 (= ?e76 ?e78)) +(flet ($e196 (distinct ?e81 ?e84)) +(flet ($e197 (distinct v4 ?e83)) +(flet ($e198 (= ?e73 ?e68)) +(flet ($e199 (= ?e81 ?e76)) +(flet ($e200 (distinct ?e77 ?e70)) +(flet ($e201 (distinct ?e88 ?e84)) +(flet ($e202 (= ?e79 ?e82)) +(flet ($e203 (= ?e69 ?e81)) +(flet ($e204 (= ?e74 ?e78)) +(flet ($e205 (= ?e87 ?e77)) +(flet ($e206 (distinct ?e80 ?e88)) +(flet ($e207 (distinct v4 ?e73)) +(flet ($e208 (distinct ?e84 ?e67)) +(flet ($e209 (= ?e76 ?e87)) +(flet ($e210 (distinct ?e84 ?e67)) +(flet ($e211 (distinct ?e88 ?e77)) +(flet ($e212 (distinct ?e79 ?e88)) +(flet ($e213 (= ?e78 v3)) +(flet ($e214 (distinct ?e84 ?e70)) +(flet ($e215 (= ?e86 ?e85)) +(flet ($e216 (= ?e75 ?e71)) +(flet ($e217 (= ?e76 ?e87)) +(flet ($e218 (distinct ?e85 ?e73)) +(flet ($e219 (= ?e67 ?e71)) +(flet ($e220 (distinct ?e74 ?e80)) +(flet ($e221 (distinct ?e67 ?e82)) +(flet ($e222 (= ?e76 ?e78)) +(flet ($e223 (distinct ?e70 ?e77)) +(flet ($e224 (= ?e81 ?e67)) +(flet ($e225 (= ?e75 ?e78)) +(flet ($e226 (distinct ?e72 ?e67)) +(flet ($e227 (= ?e80 ?e73)) +(flet ($e228 (= ?e71 ?e69)) +(flet ($e229 (distinct ?e87 ?e83)) +(flet ($e230 (distinct v4 ?e86)) +(flet ($e231 (distinct ?e81 ?e67)) +(flet ($e232 (distinct ?e75 ?e84)) +(flet ($e233 (= ?e70 ?e85)) +(flet ($e234 (distinct ?e83 v4)) +(flet ($e235 (distinct ?e80 ?e88)) +(flet ($e236 (= ?e79 ?e68)) +(flet ($e237 (distinct ?e87 ?e66)) +(flet ($e238 (= ?e98 ?e9)) +(flet ($e239 (= ?e106 ?e119)) +(flet ($e240 (= ?e104 ?e115)) +(flet ($e241 (distinct ?e10 ?e99)) +(flet ($e242 (= ?e99 ?e111)) +(flet ($e243 (= ?e89 ?e92)) +(flet ($e244 (= ?e101 v5)) +(flet ($e245 (distinct ?e106 ?e10)) +(flet ($e246 (distinct ?e14 ?e91)) +(flet ($e247 (= ?e111 ?e93)) +(flet ($e248 (distinct ?e9 ?e95)) +(flet ($e249 (distinct ?e10 ?e12)) +(flet ($e250 (= ?e97 ?e115)) +(flet ($e251 (= v5 ?e9)) +(flet ($e252 (= ?e95 ?e117)) +(flet ($e253 (distinct ?e9 ?e94)) +(flet ($e254 (distinct ?e9 ?e93)) +(flet ($e255 (distinct ?e121 ?e9)) +(flet ($e256 (distinct ?e117 ?e89)) +(flet ($e257 (= ?e96 ?e90)) +(flet ($e258 (= ?e108 ?e121)) +(flet ($e259 (distinct ?e14 ?e98)) +(flet ($e260 (distinct ?e95 v5)) +(flet ($e261 (distinct ?e108 ?e105)) +(flet ($e262 (= ?e107 ?e90)) +(flet ($e263 (distinct ?e119 ?e109)) +(flet ($e264 (= ?e107 ?e14)) +(flet ($e265 (distinct ?e109 ?e108)) +(flet ($e266 (distinct ?e117 ?e100)) +(flet ($e267 (= ?e101 ?e102)) +(flet ($e268 (distinct ?e92 ?e12)) +(flet ($e269 (distinct ?e9 ?e109)) +(flet ($e270 (= ?e90 ?e101)) +(flet ($e271 (distinct ?e12 ?e111)) +(flet ($e272 (= ?e106 ?e104)) +(flet ($e273 (= ?e115 ?e93)) +(flet ($e274 (distinct ?e104 ?e108)) +(flet ($e275 (distinct ?e8 ?e100)) +(flet ($e276 (distinct ?e97 ?e10)) +(flet ($e277 (distinct ?e100 ?e111)) +(flet ($e278 (distinct ?e89 ?e104)) +(flet ($e279 (= ?e8 ?e105)) +(flet ($e280 (distinct ?e110 ?e121)) +(flet ($e281 (= ?e89 ?e100)) +(flet ($e282 (distinct ?e93 ?e117)) +(flet ($e283 (distinct ?e121 ?e116)) +(flet ($e284 (= ?e107 ?e104)) +(flet ($e285 (distinct ?e10 v5)) +(flet ($e286 (distinct ?e116 ?e9)) +(flet ($e287 (= ?e103 ?e98)) +(flet ($e288 (implies $e272 $e127)) +(flet ($e289 (implies $e275 $e25)) +(flet ($e290 (if_then_else $e204 $e223 $e241)) +(flet ($e291 (if_then_else $e226 $e209 $e280)) +(flet ($e292 (and $e243 $e218)) +(flet ($e293 (xor $e230 $e191)) +(flet ($e294 (and $e27 $e32)) +(flet ($e295 (iff $e15 $e163)) +(flet ($e296 (implies $e124 $e270)) +(flet ($e297 (xor $e150 $e200)) +(flet ($e298 (not $e221)) +(flet ($e299 (implies $e211 $e211)) +(flet ($e300 (and $e145 $e251)) +(flet ($e301 (implies $e278 $e22)) +(flet ($e302 (and $e215 $e153)) +(flet ($e303 (and $e300 $e228)) +(flet ($e304 (iff $e210 $e30)) +(flet ($e305 (if_then_else $e135 $e291 $e152)) +(flet ($e306 (not $e195)) +(flet ($e307 (not $e143)) +(flet ($e308 (or $e132 $e138)) +(flet ($e309 (or $e253 $e307)) +(flet ($e310 (iff $e229 $e294)) +(flet ($e311 (or $e182 $e173)) +(flet ($e312 (and $e233 $e188)) +(flet ($e313 (iff $e246 $e130)) +(flet ($e314 (xor $e212 $e126)) +(flet ($e315 (implies $e168 $e18)) +(flet ($e316 (or $e21 $e287)) +(flet ($e317 (or $e183 $e203)) +(flet ($e318 (or $e159 $e277)) +(flet ($e319 (if_then_else $e258 $e238 $e224)) +(flet ($e320 (implies $e262 $e312)) +(flet ($e321 (not $e271)) +(flet ($e322 (xor $e167 $e193)) +(flet ($e323 (xor $e304 $e290)) +(flet ($e324 (iff $e125 $e199)) +(flet ($e325 (and $e19 $e186)) +(flet ($e326 (implies $e279 $e321)) +(flet ($e327 (or $e139 $e263)) +(flet ($e328 (not $e137)) +(flet ($e329 (or $e136 $e319)) +(flet ($e330 (and $e318 $e234)) +(flet ($e331 (or $e24 $e299)) +(flet ($e332 (or $e33 $e254)) +(flet ($e333 (or $e295 $e206)) +(flet ($e334 (iff $e283 $e236)) +(flet ($e335 (and $e252 $e123)) +(flet ($e336 (or $e141 $e317)) +(flet ($e337 (and $e166 $e249)) +(flet ($e338 (implies $e198 $e160)) +(flet ($e339 (not $e242)) +(flet ($e340 (or $e324 $e217)) +(flet ($e341 (implies $e265 $e185)) +(flet ($e342 (or $e245 $e171)) +(flet ($e343 (implies $e337 $e296)) +(flet ($e344 (if_then_else $e292 $e161 $e220)) +(flet ($e345 (implies $e122 $e335)) +(flet ($e346 (if_then_else $e176 $e261 $e257)) +(flet ($e347 (xor $e187 $e256)) +(flet ($e348 (if_then_else $e344 $e284 $e327)) +(flet ($e349 (xor $e293 $e31)) +(flet ($e350 (xor $e336 $e142)) +(flet ($e351 (iff $e302 $e313)) +(flet ($e352 (if_then_else $e154 $e174 $e285)) +(flet ($e353 (iff $e316 $e208)) +(flet ($e354 (if_then_else $e309 $e133 $e158)) +(flet ($e355 (not $e348)) +(flet ($e356 (or $e140 $e255)) +(flet ($e357 (iff $e216 $e219)) +(flet ($e358 (if_then_else $e169 $e129 $e331)) +(flet ($e359 (and $e164 $e147)) +(flet ($e360 (if_then_else $e311 $e250 $e181)) +(flet ($e361 (not $e332)) +(flet ($e362 (not $e320)) +(flet ($e363 (iff $e205 $e175)) +(flet ($e364 (and $e247 $e194)) +(flet ($e365 (not $e148)) +(flet ($e366 (not $e346)) +(flet ($e367 (or $e269 $e297)) +(flet ($e368 (iff $e322 $e180)) +(flet ($e369 (if_then_else $e131 $e259 $e367)) +(flet ($e370 (iff $e298 $e239)) +(flet ($e371 (iff $e352 $e306)) +(flet ($e372 (not $e202)) +(flet ($e373 (implies $e315 $e264)) +(flet ($e374 (or $e357 $e192)) +(flet ($e375 (iff $e214 $e281)) +(flet ($e376 (and $e26 $e156)) +(flet ($e377 (xor $e308 $e17)) +(flet ($e378 (or $e268 $e162)) +(flet ($e379 (if_then_else $e353 $e333 $e177)) +(flet ($e380 (not $e377)) +(flet ($e381 (xor $e235 $e235)) +(flet ($e382 (not $e338)) +(flet ($e383 (and $e360 $e144)) +(flet ($e384 (if_then_else $e345 $e149 $e170)) +(flet ($e385 (or $e362 $e323)) +(flet ($e386 (not $e369)) +(flet ($e387 (iff $e289 $e273)) +(flet ($e388 (xor $e222 $e213)) +(flet ($e389 (iff $e178 $e356)) +(flet ($e390 (xor $e165 $e248)) +(flet ($e391 (if_then_else $e379 $e34 $e288)) +(flet ($e392 (iff $e301 $e155)) +(flet ($e393 (implies $e370 $e260)) +(flet ($e394 (implies $e392 $e373)) +(flet ($e395 (xor $e378 $e310)) +(flet ($e396 (or $e359 $e276)) +(flet ($e397 (iff $e387 $e244)) +(flet ($e398 (if_then_else $e266 $e267 $e394)) +(flet ($e399 (implies $e366 $e365)) +(flet ($e400 (implies $e397 $e350)) +(flet ($e401 (and $e314 $e343)) +(flet ($e402 (not $e134)) +(flet ($e403 (and $e382 $e157)) +(flet ($e404 (if_then_else $e363 $e151 $e190)) +(flet ($e405 (implies $e381 $e231)) +(flet ($e406 (xor $e179 $e20)) +(flet ($e407 (xor $e325 $e282)) +(flet ($e408 (and $e396 $e384)) +(flet ($e409 (not $e407)) +(flet ($e410 (not $e375)) +(flet ($e411 (not $e358)) +(flet ($e412 (and $e16 $e286)) +(flet ($e413 (implies $e364 $e172)) +(flet ($e414 (iff $e406 $e404)) +(flet ($e415 (or $e342 $e334)) +(flet ($e416 (if_then_else $e349 $e400 $e413)) +(flet ($e417 (xor $e398 $e414)) +(flet ($e418 (not $e399)) +(flet ($e419 (and $e380 $e374)) +(flet ($e420 (xor $e128 $e393)) +(flet ($e421 (not $e385)) +(flet ($e422 (implies $e326 $e303)) +(flet ($e423 (if_then_else $e405 $e412 $e412)) +(flet ($e424 (implies $e395 $e423)) +(flet ($e425 (if_then_else $e386 $e355 $e227)) +(flet ($e426 (xor $e383 $e237)) +(flet ($e427 (xor $e146 $e402)) +(flet ($e428 (or $e420 $e418)) +(flet ($e429 (if_then_else $e376 $e354 $e371)) +(flet ($e430 (or $e409 $e424)) +(flet ($e431 (if_then_else $e361 $e429 $e225)) +(flet ($e432 (or $e330 $e329)) +(flet ($e433 (not $e232)) +(flet ($e434 (if_then_else $e340 $e184 $e432)) +(flet ($e435 (or $e197 $e389)) +(flet ($e436 (not $e426)) +(flet ($e437 (if_then_else $e207 $e347 $e339)) +(flet ($e438 (if_then_else $e427 $e391 $e411)) +(flet ($e439 (xor $e430 $e410)) +(flet ($e440 (or $e390 $e437)) +(flet ($e441 (implies $e368 $e240)) +(flet ($e442 (and $e441 $e408)) +(flet ($e443 (xor $e201 $e434)) +(flet ($e444 (if_then_else $e305 $e23 $e328)) +(flet ($e445 (xor $e415 $e419)) +(flet ($e446 (implies $e444 $e417)) +(flet ($e447 (if_then_else $e351 $e416 $e29)) +(flet ($e448 (implies $e431 $e446)) +(flet ($e449 (if_then_else $e439 $e388 $e440)) +(flet ($e450 (and $e403 $e442)) +(flet ($e451 (implies $e448 $e448)) +(flet ($e452 (not $e189)) +(flet ($e453 (and $e451 $e449)) +(flet ($e454 (or $e425 $e28)) +(flet ($e455 (if_then_else $e372 $e454 $e447)) +(flet ($e456 (not $e428)) +(flet ($e457 (or $e341 $e421)) +(flet ($e458 (or $e452 $e433)) +(flet ($e459 (iff $e455 $e453)) +(flet ($e460 (or $e445 $e459)) +(flet ($e461 (and $e457 $e450)) +(flet ($e462 (or $e438 $e456)) +(flet ($e463 (not $e461)) +(flet ($e464 (xor $e443 $e274)) +(flet ($e465 (xor $e460 $e462)) +(flet ($e466 (xor $e401 $e401)) +(flet ($e467 (not $e436)) +(flet ($e468 (or $e464 $e464)) +(flet ($e469 (iff $e196 $e196)) +(flet ($e470 (not $e467)) +(flet ($e471 (not $e470)) +(flet ($e472 (or $e466 $e465)) +(flet ($e473 (implies $e435 $e472)) +(flet ($e474 (not $e463)) +(flet ($e475 (not $e458)) +(flet ($e476 (iff $e422 $e475)) +(flet ($e477 (and $e473 $e468)) +(flet ($e478 (iff $e471 $e474)) +(flet ($e479 (or $e476 $e469)) +(flet ($e480 (iff $e479 $e479)) +(flet ($e481 (not $e477)) +(flet ($e482 (or $e481 $e480)) +(flet ($e483 (xor $e478 $e482)) +$e483 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/arrays/incorrect9.smt b/test/regress/regress0/arrays/incorrect9.smt new file mode 100644 index 000000000..36bf7a22c --- /dev/null +++ b/test/regress/regress0/arrays/incorrect9.smt @@ -0,0 +1,189 @@ +(benchmark fuzzsmt +:logic QF_AX +:status unsat +:extrafuns ((v0 Array)) +:extrafuns ((v1 Index)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Element)) +:extrafuns ((v4 Element)) +:extrafuns ((v5 Element)) +:extrafuns ((v6 Element)) +:extrafuns ((v7 Element)) +:formula +(let (?e8 (store v0 v2 v7)) +(let (?e9 (select ?e8 v1)) +(flet ($e10 (= v0 ?e8)) +(flet ($e11 (distinct v2 v1)) +(flet ($e12 (distinct v6 ?e9)) +(flet ($e13 (distinct v4 v3)) +(flet ($e14 (= v6 v4)) +(flet ($e15 (distinct v4 v4)) +(flet ($e16 (= v6 v7)) +(flet ($e17 (= v5 v6)) +(let (?e18 (ite $e10 v0 ?e8)) +(let (?e19 (ite $e13 v0 v0)) +(let (?e20 (ite $e13 v0 v0)) +(let (?e21 (ite $e11 ?e19 v0)) +(let (?e22 (ite $e14 ?e18 ?e20)) +(let (?e23 (ite $e10 v0 ?e21)) +(let (?e24 (ite $e13 ?e21 ?e21)) +(let (?e25 (ite $e13 ?e22 ?e21)) +(let (?e26 (ite $e15 ?e23 ?e18)) +(let (?e27 (ite $e12 ?e23 ?e26)) +(let (?e28 (ite $e16 ?e26 ?e23)) +(let (?e29 (ite $e17 ?e27 ?e26)) +(let (?e30 (ite $e10 v1 v1)) +(let (?e31 (ite $e12 v2 v1)) +(let (?e32 (ite $e17 v2 v1)) +(let (?e33 (ite $e15 v1 v2)) +(let (?e34 (ite $e14 ?e30 ?e32)) +(let (?e35 (ite $e11 ?e33 ?e34)) +(let (?e36 (ite $e16 ?e32 ?e31)) +(let (?e37 (ite $e11 ?e35 v1)) +(let (?e38 (ite $e13 v1 ?e37)) +(let (?e39 (ite $e15 v4 v6)) +(let (?e40 (ite $e13 v5 v6)) +(let (?e41 (ite $e16 ?e9 v3)) +(let (?e42 (ite $e12 ?e40 v3)) +(let (?e43 (ite $e11 v5 v7)) +(let (?e44 (ite $e10 ?e40 ?e43)) +(let (?e45 (ite $e14 v4 ?e44)) +(let (?e46 (ite $e17 ?e39 v4)) +(let (?e47 (store ?e8 ?e38 v7)) +(let (?e48 (select ?e18 ?e33)) +(flet ($e49 (= ?e18 ?e18)) +(flet ($e50 (distinct ?e23 ?e26)) +(flet ($e51 (distinct ?e28 ?e19)) +(flet ($e52 (distinct ?e47 ?e18)) +(flet ($e53 (= ?e27 ?e18)) +(flet ($e54 (distinct ?e19 ?e26)) +(flet ($e55 (distinct ?e47 v0)) +(flet ($e56 (distinct ?e19 ?e24)) +(flet ($e57 (= ?e8 ?e26)) +(flet ($e58 (distinct ?e18 ?e8)) +(flet ($e59 (distinct ?e26 ?e29)) +(flet ($e60 (= ?e19 ?e25)) +(flet ($e61 (distinct ?e29 ?e22)) +(flet ($e62 (distinct ?e22 v0)) +(flet ($e63 (distinct ?e29 ?e18)) +(flet ($e64 (distinct v0 ?e26)) +(flet ($e65 (= ?e24 ?e47)) +(flet ($e66 (distinct ?e29 ?e23)) +(flet ($e67 (distinct ?e27 ?e27)) +(flet ($e68 (distinct ?e27 ?e24)) +(flet ($e69 (= ?e29 ?e23)) +(flet ($e70 (distinct ?e8 ?e20)) +(flet ($e71 (= ?e25 ?e8)) +(flet ($e72 (= ?e18 ?e47)) +(flet ($e73 (distinct ?e22 ?e24)) +(flet ($e74 (distinct ?e21 ?e24)) +(flet ($e75 (distinct ?e38 v2)) +(flet ($e76 (distinct ?e30 ?e34)) +(flet ($e77 (distinct ?e34 ?e34)) +(flet ($e78 (distinct ?e35 ?e33)) +(flet ($e79 (distinct ?e33 ?e36)) +(flet ($e80 (distinct ?e38 ?e30)) +(flet ($e81 (= ?e35 ?e35)) +(flet ($e82 (distinct v2 ?e33)) +(flet ($e83 (= ?e34 ?e34)) +(flet ($e84 (distinct ?e37 ?e33)) +(flet ($e85 (distinct ?e30 ?e35)) +(flet ($e86 (distinct ?e37 v2)) +(flet ($e87 (distinct ?e31 v1)) +(flet ($e88 (distinct ?e32 ?e30)) +(flet ($e89 (distinct ?e40 v5)) +(flet ($e90 (distinct ?e44 v4)) +(flet ($e91 (distinct ?e9 ?e46)) +(flet ($e92 (= ?e40 ?e46)) +(flet ($e93 (= ?e46 v3)) +(flet ($e94 (distinct ?e43 v6)) +(flet ($e95 (distinct v6 v4)) +(flet ($e96 (= v4 ?e43)) +(flet ($e97 (= ?e44 ?e9)) +(flet ($e98 (distinct ?e42 ?e41)) +(flet ($e99 (distinct v4 ?e48)) +(flet ($e100 (distinct v4 ?e9)) +(flet ($e101 (distinct ?e44 v7)) +(flet ($e102 (distinct v3 ?e45)) +(flet ($e103 (= v7 ?e46)) +(flet ($e104 (distinct ?e40 v6)) +(flet ($e105 (= v4 ?e41)) +(flet ($e106 (distinct ?e45 ?e40)) +(flet ($e107 (distinct v7 v4)) +(flet ($e108 (= v6 v3)) +(flet ($e109 (distinct ?e39 v3)) +(flet ($e110 (or $e81 $e90)) +(flet ($e111 (xor $e92 $e10)) +(flet ($e112 (iff $e11 $e57)) +(flet ($e113 (iff $e50 $e49)) +(flet ($e114 (not $e91)) +(flet ($e115 (if_then_else $e69 $e51 $e64)) +(flet ($e116 (if_then_else $e98 $e97 $e82)) +(flet ($e117 (xor $e67 $e71)) +(flet ($e118 (if_then_else $e61 $e88 $e55)) +(flet ($e119 (implies $e59 $e99)) +(flet ($e120 (or $e13 $e117)) +(flet ($e121 (iff $e73 $e112)) +(flet ($e122 (and $e94 $e68)) +(flet ($e123 (not $e60)) +(flet ($e124 (and $e100 $e15)) +(flet ($e125 (or $e70 $e111)) +(flet ($e126 (or $e75 $e119)) +(flet ($e127 (xor $e121 $e17)) +(flet ($e128 (iff $e127 $e76)) +(flet ($e129 (if_then_else $e72 $e16 $e115)) +(flet ($e130 (not $e65)) +(flet ($e131 (xor $e85 $e93)) +(flet ($e132 (and $e103 $e89)) +(flet ($e133 (if_then_else $e128 $e14 $e79)) +(flet ($e134 (implies $e114 $e12)) +(flet ($e135 (not $e133)) +(flet ($e136 (iff $e129 $e105)) +(flet ($e137 (xor $e87 $e135)) +(flet ($e138 (and $e137 $e118)) +(flet ($e139 (implies $e131 $e74)) +(flet ($e140 (iff $e126 $e116)) +(flet ($e141 (or $e120 $e120)) +(flet ($e142 (if_then_else $e101 $e113 $e134)) +(flet ($e143 (and $e52 $e140)) +(flet ($e144 (iff $e139 $e122)) +(flet ($e145 (or $e136 $e104)) +(flet ($e146 (not $e54)) +(flet ($e147 (if_then_else $e96 $e95 $e109)) +(flet ($e148 (iff $e123 $e78)) +(flet ($e149 (and $e146 $e146)) +(flet ($e150 (implies $e108 $e107)) +(flet ($e151 (xor $e62 $e147)) +(flet ($e152 (not $e77)) +(flet ($e153 (if_then_else $e150 $e145 $e102)) +(flet ($e154 (iff $e142 $e130)) +(flet ($e155 (and $e86 $e138)) +(flet ($e156 (and $e149 $e155)) +(flet ($e157 (implies $e80 $e66)) +(flet ($e158 (implies $e156 $e143)) +(flet ($e159 (iff $e154 $e157)) +(flet ($e160 (not $e56)) +(flet ($e161 (xor $e63 $e141)) +(flet ($e162 (or $e125 $e151)) +(flet ($e163 (iff $e58 $e83)) +(flet ($e164 (or $e110 $e132)) +(flet ($e165 (or $e163 $e153)) +(flet ($e166 (and $e53 $e159)) +(flet ($e167 (and $e152 $e165)) +(flet ($e168 (not $e160)) +(flet ($e169 (iff $e164 $e166)) +(flet ($e170 (not $e106)) +(flet ($e171 (and $e124 $e169)) +(flet ($e172 (if_then_else $e167 $e144 $e167)) +(flet ($e173 (iff $e162 $e170)) +(flet ($e174 (and $e172 $e171)) +(flet ($e175 (iff $e161 $e168)) +(flet ($e176 (and $e173 $e175)) +(flet ($e177 (implies $e174 $e176)) +(flet ($e178 (iff $e148 $e158)) +(flet ($e179 (iff $e177 $e84)) +(flet ($e180 (iff $e178 $e178)) +(flet ($e181 (implies $e180 $e179)) +$e181 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +