Remove assertion related to CEGQI dependency lemmas (#5559)

This assertion does not hold when we mix --sygus-inst with normal CEGQI.

Should fix the nightlies.

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 1a67a2b161c5635857f7d297b13979870b8080cf..1d917b8f4095b82dfb99be929f012e7415a43da5 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -156,7 +156,11 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
         {
           d_parent_quant[q].push_back(qi);
           d_children_quant[qi].push_back(q);
-          Assert(hasAddedCbqiLemma(qi));
+          // may not have added the CEX lemma, but the literal is created by
+          // the following call regardless. One rare case where this can happen
+          // is if both sygus-inst and CEGQI are being run in parallel, and
+          // a parent quantified formula is not handled by CEGQI, but a child
+          // is.
           Node qicel = getCounterexampleLiteral(qi);
           dep.push_back(qi);
           dep.push_back(qicel);
@@ -164,6 +168,9 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       }
       if (!dep.empty())
       {
+        // This lemma states that if the child is active, then the parent must
+        // be asserted, in particular G => Q where G is the CEX literal for the
+        // child and Q is the parent.
         Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
         Trace("cegqi-lemma")
             << "Counterexample dependency lemma : " << dep_lemma << std::endl;