diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-29 13:50:34 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-29 13:50:34 +0000 |
commit | a42d1d31d9f73a1d9fdce404153598c5b94ed241 (patch) | |
tree | 9ad1a041dfa18db999fc76dcb90d59fbc6a0f241 /src/theory/theory_engine.cpp | |
parent | 572f874ba8d6275c6f7ad5dfbfd7ea26d0bb9e5f (diff) |
Disable some array optimizations when models are on
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 6 |
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); } } |