Disable some array optimizations when models are on

1 files changed, 5 insertions, 1 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d5c4998d4..a952c9ee6 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -563,7 +563,11 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
     TNode var = *it;
     hasValue = d_propEngine->hasValue(var, value);
     // TODO: Assert that hasValue is true?
-    m->assertPredicate(var, hasValue ? value : false);
+    if (!hasValue) {
+      value = false;
+    }
+    Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
+    m->assertPredicate(var, value);
   }
 }