diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index cf7611dab..c21aa5445 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -582,6 +582,10 @@ void TheoryEngine::check(Theory::Effort effort) { // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) { + Trace("theory::assertions-model") << endl; + if (Trace.isOn("theory::assertions-model")) { + printAssertions("theory::assertions-model"); + } //checks for theories requiring the model go at last call bool builtModel = false; for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { @@ -607,10 +611,6 @@ void TheoryEngine::check(Theory::Effort effort) { // must build model at this point d_curr_model_builder->buildModel(d_curr_model, true); } - Trace("theory::assertions-model") << endl; - if (Trace.isOn("theory::assertions-model")) { - printAssertions("theory::assertions-model"); - } } } |