From 6489cf590b441aeb5e1bdf9800c9718d06842149 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 30 Nov 2020 22:22:24 -0600
Subject: More fixes for quantifier elimination (#5533)

Fixes #5506, fixes #5507.
---
 test/regress/regress1/quantifiers/issue5506-qe.smt2 |  6 ++++++
 test/regress/regress1/quantifiers/issue5507-qe.smt2 | 19 +++++++++++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 test/regress/regress1/quantifiers/issue5506-qe.smt2
 create mode 100644 test/regress/regress1/quantifiers/issue5507-qe.smt2

(limited to 'test/regress/regress1')

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)))
-- 
cgit v1.2.3