Fix cegqi assertions for quantified non-linear cases. (#1999)

2 files changed, 14 insertions, 2 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index df51ace2d..72633e86f 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -707,7 +707,15 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
         && vinst->allowModelValue(this, sf, pv, d_effort))
     {
 #ifdef CVC4_ASSERTIONS
-      if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){
+      // the instantiation strategy for quantified linear integer/real
+      // arithmetic with arbitrary quantifier nesting is "monotonic" as a
+      // consequence of Lemmas 5, 9 and Theorem 4 of Reynolds et al, "Solving
+      // Quantified Linear Arithmetic by Counterexample Guided Instantiation",
+      // FMSD 2017. We throw an assertion failure if we detect a case where the
+      // strategy was not monotonic.
+      if (options::cbqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH)
+          && d_qe->getLogicInfo().isLinear())
+      {
         Trace("cbqi-warn") << "Had to resort to model value." << std::endl;
         Assert( false );
       }
diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
index a4599627d..203697fd7 100644
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -354,7 +354,11 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
               lhs_value = Rewriter::rewrite( lhs_value );
             }
             Trace("cegqi-arith-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
-            Assert( lhs_value!=rhs_value );
+            // it generally should be the case that lhs_value!=rhs_value
+            // however, this assertion is violated e.g. if non-linear is enabled
+            // since the quantifier-free arithmetic solver may pass full
+            // effort with no lemmas even when we are not guaranteed to have a
+            // model. By convention, we use GEQ to compare the values here.
             Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
             cmp = Rewriter::rewrite( cmp );
             Assert( cmp.isConst() );