3 files changed, 17 insertions, 6 deletions
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index b4821cfd6..096e0933d 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -603,7 +603,7 @@ FullSaturation::FullSaturation( QuantifiersEngine* qe ) : QuantifiersModule( qe
 }
 
 bool FullSaturation::needsCheck( Theory::Effort e ){
-  if( options::fullSaturateInst() ){
+  if( options::fullSaturateInterleave() ){
     if( d_quantEngine->getInstWhenNeedsCheck( e ) ){
       return true;
     }
@@ -623,7 +623,7 @@ void FullSaturation::reset_round( Theory::Effort e ) {
 void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
   bool doCheck = false;
   bool fullEffort = false;
-  if( options::fullSaturateInst() ){
+  if( options::fullSaturateInterleave() ){
     //we only add when interleaved with other strategies
     doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
   }
@@ -653,7 +653,7 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
     if( Trace.isOn("fs-engine") ){
       Trace("fs-engine") << "Added lemmas = " << addedLemmas  << std::endl;
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("fs-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
+      Trace("fs-engine") << "Finished full saturation engine, time = " << (clSet2-clSet) << std::endl;
     }
   }
 }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index c43187163..24c2d1254 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -53,7 +53,11 @@ bool ModelEngine::needsCheck( Theory::Effort e ) {
 }
 
 unsigned ModelEngine::needsModel( Theory::Effort e ) {
-  return QuantifiersEngine::QEFFORT_MODEL;
+  if( options::mbqiInterleave() ){
+    return QuantifiersEngine::QEFFORT_STANDARD;
+  }else{
+    return QuantifiersEngine::QEFFORT_MODEL;
+  }
 }
 
 void ModelEngine::reset_round( Theory::Effort e ) {
@@ -61,7 +65,14 @@ void ModelEngine::reset_round( Theory::Effort e ) {
 }
 
 void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
-  if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
+  bool doCheck = false;
+  if( options::mbqiInterleave() ){
+    doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
+  }
+  if( !doCheck ){
+    doCheck = quant_e==QuantifiersEngine::QEFFORT_MODEL;
+  }
+  if( doCheck ){
     Assert( !d_quantEngine->inConflict() );
     int addedLemmas = 0;
     FirstOrderModel* fm = d_quantEngine->getModel();
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index fa1394f39..fd831001f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -265,7 +265,7 @@ void QuantifiersEngine::finishInit(){
     d_modules.push_back( d_uee );
   }
   //full saturation : instantiate from relevant domain, then arbitrary terms
-  if( options::fullSaturateQuant() || options::fullSaturateInst() ){
+  if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
     d_fs = new quantifiers::FullSaturation( this );
     d_modules.push_back( d_fs );
     needsRelDom = true;