1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0db71aba4..61b66ba3e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -590,6 +590,17 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
       d_theoryTable[theoryId]->collectModelInfo( m, fullModel );
     }
   }
+  // Get the Boolean variables
+  vector<TNode> boolVars;
+  d_propEngine->getBooleanVariables(boolVars);
+  vector<TNode>::iterator it, iend = boolVars.end();
+  bool hasValue, value;
+  for (it = boolVars.begin(); it != iend; ++it) {
+    TNode var = *it;
+    hasValue = d_propEngine->hasValue(var, value);
+    // TODO: Assert that hasValue is true?
+    m->assertPredicate(var, hasValue ? value : false);
+  }
 }
 
 /* get model */