summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp6
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);
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback