diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress0/sets/fuzz15201.smt2 | |
parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress0/sets/fuzz15201.smt2')
-rw-r--r-- | test/regress/regress0/sets/fuzz15201.smt2 | 269 |
1 files changed, 0 insertions, 269 deletions
diff --git a/test/regress/regress0/sets/fuzz15201.smt2 b/test/regress/regress0/sets/fuzz15201.smt2 deleted file mode 100644 index e12b74d18..000000000 --- a/test/regress/regress0/sets/fuzz15201.smt2 +++ /dev/null @@ -1,269 +0,0 @@ -; symptom: unsat instead of sat -; issue/fix: buggy rewriter for setminus -(set-info :source |fuzzsmt|) -(set-info :smt-lib-version 2.0) -(set-info :category "random") -(set-info :status sat) -(set-logic QF_UFLIAFS) -(define-sort Element () Int) -(declare-fun f0 ( Int) Int) -(declare-fun f1 ( (Set Element)) (Set Element)) -(declare-fun p0 ( Int) Bool) -(declare-fun p1 ( (Set Element) (Set Element) (Set Element)) Bool) -(declare-fun v0 () Int) -(declare-fun v1 () (Set Element)) -(declare-fun v2 () (Set Element)) -(assert (let ((e3 0)) -(let ((e4 (+ v0 v0))) -(let ((e5 (+ v0 e4))) -(let ((e6 (* (- e3) e4))) -(let ((e7 (- e4 e6))) -(let ((e8 (+ e7 e5))) -(let ((e9 (- v0))) -(let ((e10 (* e6 e3))) -(let ((e11 (- e8 e5))) -(let ((e12 (- e5))) -(let ((e13 (* e7 (- e3)))) -(let ((e14 (f0 e7))) -(let ((e15 (ite (p0 e9) 1 0))) -(let ((e16 (setminus v2 v1))) -(let ((e17 (setminus v1 v2))) -(let ((e18 (union e17 e17))) -(let ((e19 (intersection e17 v1))) -(let ((e20 (intersection e17 e18))) -(let ((e21 (intersection v1 e16))) -(let ((e22 (setminus e20 e16))) -(let ((e23 (ite (p1 v2 e18 e21) (singleton 1) (singleton 0)))) -(let ((e24 (setminus e17 e23))) -(let ((e25 (union v2 e22))) -(let ((e26 (union e24 e18))) -(let ((e27 (ite (p1 e20 e19 e25) (singleton 1) (singleton 0)))) -(let ((e28 (f1 e20))) -(let ((e29 (member e14 e17))) -(let ((e30 (member e13 e23))) -(let ((e31 (member e11 e25))) -(let ((e32 (member e6 v1))) -(let ((e33 (member e9 v1))) -(let ((e34 (member v0 e28))) -(let ((e35 (member e9 e16))) -(let ((e36 (member e4 e17))) -(let ((e37 (member e9 e18))) -(let ((e38 (member e14 e25))) -(let ((e39 (member e14 v2))) -(let ((e40 (member v0 v1))) -(let ((e41 (member e4 e16))) -(let ((e42 (member e15 e21))) -(let ((e43 (member e7 e22))) -(let ((e44 (member e11 v2))) -(let ((e45 (member e14 e22))) -(let ((e46 (member e11 e16))) -(let ((e47 (member e15 e22))) -(let ((e48 (member e10 e23))) -(let ((e49 (member e4 e21))) -(let ((e50 (member e5 e28))) -(let ((e51 (member e6 e28))) -(let ((e52 (member v0 e22))) -(let ((e53 (member e14 e20))) -(let ((e54 (f1 e21))) -(let ((e55 (f1 e28))) -(let ((e56 (f1 e27))) -(let ((e57 (f1 e17))) -(let ((e58 (f1 e22))) -(let ((e59 (f1 e26))) -(let ((e60 (f1 e19))) -(let ((e61 (f1 v1))) -(let ((e62 (f1 e24))) -(let ((e63 (f1 e20))) -(let ((e64 (f1 e23))) -(let ((e65 (f1 v2))) -(let ((e66 (f1 e25))) -(let ((e67 (f1 e62))) -(let ((e68 (f1 e18))) -(let ((e69 (f1 e18))) -(let ((e70 (f1 e23))) -(let ((e71 (f1 e55))) -(let ((e72 (f1 e26))) -(let ((e73 (f1 e16))) -(let ((e74 (= e13 e13))) -(let ((e75 (p0 e11))) -(let ((e76 (distinct e15 e4))) -(let ((e77 (> e14 e10))) -(let ((e78 (= e4 e15))) -(let ((e79 (distinct v0 e9))) -(let ((e80 (= e15 e14))) -(let ((e81 (>= e10 e11))) -(let ((e82 (distinct e9 e8))) -(let ((e83 (p0 v0))) -(let ((e84 (>= e12 e14))) -(let ((e85 (distinct e7 e13))) -(let ((e86 (<= e6 e11))) -(let ((e87 (= e13 e10))) -(let ((e88 (>= e7 e8))) -(let ((e89 (<= v0 e10))) -(let ((e90 (>= e5 e15))) -(let ((e91 (ite e33 e66 e26))) -(let ((e92 (ite e88 e54 v1))) -(let ((e93 (ite e76 e70 e16))) -(let ((e94 (ite e85 e19 e24))) -(let ((e95 (ite e88 e68 e20))) -(let ((e96 (ite e86 e25 e65))) -(let ((e97 (ite e83 v2 e23))) -(let ((e98 (ite e50 e63 e63))) -(let ((e99 (ite e48 e56 e93))) -(let ((e100 (ite e38 e60 v2))) -(let ((e101 (ite e30 e61 e61))) -(let ((e102 (ite e85 e69 e57))) -(let ((e103 (ite e83 e18 e102))) -(let ((e104 (ite e43 e62 e97))) -(let ((e105 (ite e76 e27 e21))) -(let ((e106 (ite e89 e92 e55))) -(let ((e107 (ite e46 e72 e65))) -(let ((e108 (ite e79 e71 e97))) -(let ((e109 (ite e44 e64 e21))) -(let ((e110 (ite e33 e70 e25))) -(let ((e111 (ite e43 e63 e105))) -(let ((e112 (ite e39 e56 e108))) -(let ((e113 (ite e49 e17 e107))) -(let ((e114 (ite e74 e63 e113))) -(let ((e115 (ite e84 e28 v1))) -(let ((e116 (ite e82 e68 e67))) -(let ((e117 (ite e75 e73 e21))) -(let ((e118 (ite e36 e59 e16))) -(let ((e119 (ite e48 e118 e61))) -(let ((e120 (ite e90 e56 e100))) -(let ((e121 (ite e80 e24 e25))) -(let ((e122 (ite e31 e22 v2))) -(let ((e123 (ite e45 e107 e16))) -(let ((e124 (ite e40 e70 e73))) -(let ((e125 (ite e52 e58 e118))) -(let ((e126 (ite e88 e72 e72))) -(let ((e127 (ite e35 e58 e27))) -(let ((e128 (ite e42 e59 e21))) -(let ((e129 (ite e44 e127 e103))) -(let ((e130 (ite e51 e118 e69))) -(let ((e131 (ite e37 e16 e24))) -(let ((e132 (ite e83 e105 e28))) -(let ((e133 (ite e48 e107 e60))) -(let ((e134 (ite e34 e101 e22))) -(let ((e135 (ite e86 e97 e57))) -(let ((e136 (ite e47 e94 e100))) -(let ((e137 (ite e78 e104 e95))) -(let ((e138 (ite e75 e26 e96))) -(let ((e139 (ite e35 e97 e121))) -(let ((e140 (ite e44 e112 e118))) -(let ((e141 (ite e77 e107 e56))) -(let ((e142 (ite e53 e64 e129))) -(let ((e143 (ite e48 e128 e23))) -(let ((e144 (ite e50 e73 e17))) -(let ((e145 (ite e33 e98 e114))) -(let ((e146 (ite e32 e137 e105))) -(let ((e147 (ite e41 e98 e96))) -(let ((e148 (ite e29 e93 e121))) -(let ((e149 (ite e87 e104 e21))) -(let ((e150 (ite e46 e131 e110))) -(let ((e151 (ite e81 e25 e65))) -(let ((e152 (ite e34 e10 e10))) -(let ((e153 (ite e36 e7 e13))) -(let ((e154 (ite e43 e12 e10))) -(let ((e155 (ite e50 e14 e7))) -(let ((e156 (ite e34 e9 e6))) -(let ((e157 (ite e33 e7 v0))) -(let ((e158 (ite e50 e157 e10))) -(let ((e159 (ite e51 e8 e11))) -(let ((e160 (ite e32 v0 e157))) -(let ((e161 (ite e85 e15 e158))) -(let ((e162 (ite e43 e5 e11))) -(let ((e163 (ite e76 e4 v0))) -(let ((e164 (ite e53 e10 e159))) -(let ((e165 (ite e80 e161 e163))) -(let ((e166 (ite e78 e13 e11))) -(let ((e167 (ite e49 e4 e8))) -(let ((e168 (ite e45 e11 e155))) -(let ((e169 (ite e81 e155 e166))) -(let ((e170 (ite e87 e169 e161))) -(let ((e171 (ite e53 e165 e13))) -(let ((e172 (ite e83 e12 e160))) -(let ((e173 (ite e80 e168 e159))) -(let ((e174 (ite e46 e171 e168))) -(let ((e175 (ite e74 e5 e155))) -(let ((e176 (ite e89 e159 e4))) -(let ((e177 (ite e29 e159 e172))) -(let ((e178 (ite e79 e165 e162))) -(let ((e179 (ite e88 e166 e168))) -(let ((e180 (ite e77 e175 e167))) -(let ((e181 (ite e47 e157 e165))) -(let ((e182 (ite e84 e172 e7))) -(let ((e183 (ite e30 e174 e157))) -(let ((e184 (ite e90 e4 e14))) -(let ((e185 (ite e38 e178 e14))) -(let ((e186 (ite e44 e166 e154))) -(let ((e187 (ite e42 e162 e186))) -(let ((e188 (ite e86 e187 e10))) -(let ((e189 (ite e29 e171 e182))) -(let ((e190 (ite e77 e185 e165))) -(let ((e191 (ite e75 e171 e9))) -(let ((e192 (ite e39 e161 e181))) -(let ((e193 (ite e82 e166 e10))) -(let ((e194 (ite e31 e183 e179))) -(let ((e195 (ite e44 e191 e169))) -(let ((e196 (ite e35 e171 e156))) -(let ((e197 (ite e86 e179 e164))) -(let ((e198 (ite e41 e5 e5))) -(let ((e199 (ite e85 e160 e161))) -(let ((e200 (ite e52 e173 e157))) -(let ((e201 (ite e47 e161 e4))) -(let ((e202 (ite e52 e6 e186))) -(let ((e203 (ite e45 e162 e198))) -(let ((e204 (ite e48 e194 e11))) -(let ((e205 (ite e37 e197 e157))) -(let ((e206 (ite e35 e153 e176))) -(let ((e207 (ite e40 e185 e188))) -(let ((e208 (= e53 e41))) -(let ((e209 (not e79))) -(let ((e210 (= e30 e87))) -(let ((e211 (or e34 e48))) -(let ((e212 (=> e82 e29))) -(let ((e213 (xor e77 e211))) -(let ((e214 (and e31 e78))) -(let ((e215 (ite e36 e76 e37))) -(let ((e216 (= e84 e45))) -(let ((e217 (or e43 e46))) -(let ((e218 (and e88 e40))) -(let ((e219 (not e89))) -(let ((e220 (not e35))) -(let ((e221 (or e218 e213))) -(let ((e222 (xor e216 e75))) -(let ((e223 (ite e85 e90 e219))) -(let ((e224 (= e32 e217))) -(let ((e225 (not e39))) -(let ((e226 (xor e212 e49))) -(let ((e227 (and e222 e81))) -(let ((e228 (or e33 e210))) -(let ((e229 (xor e225 e226))) -(let ((e230 (xor e74 e47))) -(let ((e231 (= e220 e38))) -(let ((e232 (xor e231 e229))) -(let ((e233 (and e50 e221))) -(let ((e234 (and e42 e224))) -(let ((e235 (xor e223 e214))) -(let ((e236 (= e234 e228))) -(let ((e237 (and e227 e235))) -(let ((e238 (not e51))) -(let ((e239 (= e80 e232))) -(let ((e240 (or e230 e86))) -(let ((e241 (not e238))) -(let ((e242 (xor e44 e237))) -(let ((e243 (= e236 e242))) -(let ((e244 (= e209 e240))) -(let ((e245 (and e239 e83))) -(let ((e246 (or e208 e245))) -(let ((e247 (=> e215 e246))) -(let ((e248 (ite e233 e247 e244))) -(let ((e249 (and e248 e241))) -(let ((e250 (=> e243 e249))) -(let ((e251 (and e52 e250))) -e251 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - -(check-sat) -;(get-model) |