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 8bd29b16f037509e8265d08f07c659b6c1ea5c8a..2ffa0d7c1d9db86726586e5de43ff210231004a4 100644 (file)
--- 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 7c53e27affe8719f1fee19c15537e7e386a420c6..ffc92c20e811c4f195d83a13d06a03e071c88b96 100644 (file)
--- 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 (file)
index 0000000..d20f14a
--- /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))