first working version of new inst-gen-style quantifier instantiation technique for fmf (--fmf-new-inst-gen), minor cleanup

1 files changed, 7 insertions, 7 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9d7c8e315..4ba5c39e6 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -97,17 +97,17 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
   d_hasAddedLemma = false;
   if( e==Theory::EFFORT_LAST_CALL ){
+    //if effort is last call, try to minimize model first
+    if( options::finiteModelFind() ){
+      //first, check if we can minimize the model further
+      if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
+        return;
+      }
+    }
     ++(d_statistics.d_instantiation_rounds_lc);
   }else if( e==Theory::EFFORT_FULL ){
     ++(d_statistics.d_instantiation_rounds);
   }
-  //if effort is last call, try to minimize model first
-  if( e==Theory::EFFORT_LAST_CALL && options::finiteModelFind() ){
-    //first, check if we can minimize the model further
-    if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
-      return;
-    }
-  }
   for( int i=0; i<(int)d_modules.size(); i++ ){
     d_modules[i]->check( e );
   }