Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)

3 files changed, 4 insertions, 6 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 358efede7..6e59363e2 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -878,10 +878,6 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
 }
   
 bool CegInstantiator::check() {
-  if( d_qe->getTheoryEngine()->needCheck() ){
-    Trace("cbqi-engine") << "  CEGQI instantiator : wait until all ground theories are finished." << std::endl;
-    return false;
-  }
   processAssertions();
   for( unsigned r=0; r<2; r++ ){
     d_effort = r == 0 ? CEG_INST_EFFORT_STANDARD : CEG_INST_EFFORT_FULL;
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 125682e8c..86f5abf61 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -39,7 +39,8 @@ CegInstantiation::~CegInstantiation(){
 }
 
 bool CegInstantiation::needsCheck( Theory::Effort e ) {
-  return e>=Theory::EFFORT_LAST_CALL;
+  return !d_quantEngine->getTheoryEngine()->needCheck()
+         && e >= Theory::EFFORT_LAST_CALL;
 }
 
 QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e)
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 885c36bb5..edea22fbf 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -612,7 +612,8 @@ void TheoryEngine::check(Theory::Effort effort) {
           }
         }
       }
-      if( ! d_inConflict && ! needCheck() ){
+      if (!d_inConflict)
+      {
         if(d_logicInfo.isQuantified()) {
           // quantifiers engine must check at last call effort
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);