1 files changed, 9 insertions, 1 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 );
       }