Add quant elim regression (#6103)

Fixes #5658.

This was fixed by recent refactoring to quantifier elimination, adding the regression to close the issue.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8a1136ca471645b5cb9344f05e84fc92e9096b52..14701910851bafbbe586c2047125dd85331248dd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1773,6 +1773,7 @@ set(regress_1_tests
   regress1/quantifiers/issue5484b-qe.smt2
   regress1/quantifiers/issue5506-qe.smt2
   regress1/quantifiers/issue5507-qe.smt2
+  regress1/quantifiers/issue5658-qe.smt2
   regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2

diff --git a/test/regress/regress1/quantifiers/issue5658-qe.smt2 b/test/regress/regress1/quantifiers/issue5658-qe.smt2
new file mode 100644 (file)
index 0000000..d2e5f7a
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5658-qe.smt2
@@ -0,0 +1,6 @@
+; SCRUBBER: sed 's/(.*)/()/g'
+; EXPECT: ()
+; EXIT: 0
+(set-logic LIA)
+(declare-fun a () Int)
+(get-qe (exists ((b Int)) (= a 0)))