From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 2 Nov 2021 00:17:38 +0000 (-0500)
Subject: Make quant elimination robust to presence of other quantified formulas (#7551)
X-Git-Tag: cvc5-1.0.0~911
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50687471628722439b1eafa7085c6d3ff2fe5e5c;p=cvc5.git

Make quant elimination robust to presence of other quantified formulas (#7551)

Fixes #4813
---

diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 8bd29b16f..2ffa0d7c1 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -92,11 +92,20 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
     // version of the input quantified formula q.
     std::vector<Node> inst_qs;
     qe->getInstantiatedQuantifiedFormulas(inst_qs);
-    Assert(inst_qs.size() <= 1);
+    Node topq;
+    // Find the quantified formula corresponding to the quantifier elimination
+    for (const Node& qinst : inst_qs)
+    {
+      // Should have the same attribute mark as above
+      if (qinst.getNumChildren() == 3 && qinst[2] == n_attr)
+      {
+        topq = qinst;
+        break;
+      }
+    }
     Node ret;
-    if (inst_qs.size() == 1)
+    if (!topq.isNull())
     {
-      Node topq = inst_qs[0];
       Assert(topq.getKind() == FORALL);
       Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
                       << topq << std::endl;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7c53e27af..ffc92c20e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1957,6 +1957,7 @@ set(regress_1_tests
   regress1/quantifiers/issue4433-nqe.smt2
   regress1/quantifiers/issue4620-erq-witness-unsound.smt2
   regress1/quantifiers/issue4685-wrewrite.smt2
+  regress1/quantifiers/issue4813-qe-quant.smt2
   regress1/quantifiers/issue4849-nqe.smt2
   regress1/quantifiers/issue5019-cegqi-i.smt2
   regress1/quantifiers/issue5279-nqe.smt2
diff --git a/test/regress/regress1/quantifiers/issue4813-qe-quant.smt2 b/test/regress/regress1/quantifiers/issue4813-qe-quant.smt2
new file mode 100644
index 000000000..d20f14a7c
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue4813-qe-quant.smt2
@@ -0,0 +1,6 @@
+; EXPECT: v24
+(set-logic LIA)
+(declare-const v8 Bool)
+(assert (not (exists ((q16 Bool)) (xor true q16 v8 q16))))
+(declare-const v24 Bool)
+(get-qe (exists ((q17 Bool) (q18 Int) (q19 Int) (q20 Int) (q21 Int) (q22 Bool)) v24))