diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-30 22:22:24 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-30 22:22:24 -0600 |
| commit | 6489cf590b441aeb5e1bdf9800c9718d06842149 (patch) | |
| tree | 98eaa6adb49fea33593a770d37d2e89cc7c15bbb /test/regress/regress1 | |
| parent | acdffc72bd559fa4b64da2ee2b3373208354e7a1 (diff) | |
More fixes for quantifier elimination (#5533)
Fixes #5506, fixes #5507.
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5506-qe.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5507-qe.smt2 | 19 |
2 files changed, 25 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/issue5506-qe.smt2 b/test/regress/regress1/quantifiers/issue5506-qe.smt2 new file mode 100644 index 000000000..3839f2d75 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5506-qe.smt2 @@ -0,0 +1,6 @@ +; SCRUBBER: sed 's/(.*)/()/g' +; EXPECT: () +; EXIT: 0 +(set-logic LIA) +(declare-fun a () Int) +(get-qe (forall ((b Int)) (= a 0))) diff --git a/test/regress/regress1/quantifiers/issue5507-qe.smt2 b/test/regress/regress1/quantifiers/issue5507-qe.smt2 new file mode 100644 index 000000000..3b7ddbcf3 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5507-qe.smt2 @@ -0,0 +1,19 @@ +; EXPECT: false +; EXIT: 0 +(set-logic LIA) +(declare-fun v0 () Bool) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v5 () Bool) +(declare-fun v6 () Bool) +(declare-fun v9 () Bool) +(declare-fun v10 () Bool) +(declare-fun v15 () Bool) +(declare-fun v16 () Bool) +(declare-fun i0 () Int) +(declare-fun i2 () Int) +(declare-fun i9 () Int) +(declare-fun v26 () Bool) +(declare-fun v33 () Bool) +(get-qe (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (and (=> (distinct 309 i2) (or q157 v9 (distinct v16 v6 v5 v10) q159 (=> v15 v26))) (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (=> (xor q156 v3 v2 q156 q156 q159 (>= 217 826 149 i0 i9) v1 v5 q157 q157) (distinct q160 q160))) v33 (distinct v16 v6 v5 v10) v0))) |