Make collect model info return a Bool (#1421)

1 files changed, 30 insertions, 13 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 944185b31..4e2062c43 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -605,8 +605,6 @@ void TheoryEngine::check(Theory::Effort effort) {
             if( theory->needsCheckLastEffort() ){
               if( !d_curr_model->isBuilt() ){
                 if( !d_curr_model_builder->buildModel(d_curr_model) ){
-                  //model building should fail only if the model builder adds lemmas
-                  Assert( needCheck() );
                   break;
                 }
               }
@@ -617,10 +615,14 @@ void TheoryEngine::check(Theory::Effort effort) {
       }
       if( ! d_inConflict && ! needCheck() ){
         if(d_logicInfo.isQuantified()) {
-          // quantifiers engine must pass effort last call check
+          // quantifiers engine must check at last call effort
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
-          // if returning incomplete or SAT, we have ensured that d_curr_model has been built
-        } else if(options::produceModels() && !d_curr_model->isBuilt()) {
+        }
+      }
+      if (!d_inConflict && !needCheck())
+      {
+        if (options::produceModels() && !d_curr_model->isBuilt())
+        {
           // must build model at this point
           d_curr_model_builder->buildModel(d_curr_model);
         }
@@ -631,14 +633,21 @@ void TheoryEngine::check(Theory::Effort effort) {
     Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
 
     if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
-      //we will answer SAT
+      // case where we are about to answer SAT
       if( d_masterEqualityEngine != NULL ){
         AlwaysAssert(d_masterEqualityEngine->consistent());
       }
-      if( options::produceModels() ){
-        d_curr_model_builder->debugCheckModel(d_curr_model);  
-        // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model)
-        postProcessModel(d_curr_model);
+      if (d_curr_model->isBuilt())
+      {
+        // model construction should always succeed unless lemmas were added
+        AlwaysAssert(d_curr_model->isBuiltSuccess());
+        if (options::produceModels())
+        {
+          d_curr_model_builder->debugCheckModel(d_curr_model);
+          // Do post-processing of model from the theories (used for THEORY_SEP
+          // to construct heap model)
+          postProcessModel(d_curr_model);
+        }
       }
     }
   } catch(const theory::Interrupted&) {
@@ -846,7 +855,8 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
   return true;
 }
 
-void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
+bool TheoryEngine::collectModelInfo(theory::TheoryModel* m)
+{
   //have shared term engine collectModelInfo
   //  d_sharedTerms.collectModelInfo( m );
   // Consult each active theory to get all relevant information
@@ -854,7 +864,10 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
     if(d_logicInfo.isTheoryEnabled(theoryId)) {
       Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId << endl;
-      d_theoryTable[theoryId]->collectModelInfo( m );
+      if (!d_theoryTable[theoryId]->collectModelInfo(m))
+      {
+        return false;
+      }
     }
   }
   // Get the Boolean variables
@@ -870,8 +883,12 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
       value = false;
     }
     Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
-    m->assertPredicate(var, value);
+    if (!m->assertPredicate(var, value))
+    {
+      return false;
+    }
   }
+  return true;
 }
 
 void TheoryEngine::postProcessModel( theory::TheoryModel* m ){