diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a79416b76..a0066f9ff 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3835,6 +3835,8 @@ void SmtEnginePrivate::processAssertions() { // Add dummy assertion in last position - to be used as a // placeholder for any new assertions to get added + PROOF(ProofManager::currentPM()->addCoreAssertion( + NodeManager::currentNM()->mkConst<bool>(true).toExpr())); d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true)); // any assertions added beyond realAssertionsEnd must NOT affect the // equisatisfiability @@ -3856,14 +3858,6 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl; dumpAssertions("post-definition-expansion", d_assertions); - // save the assertions now - THEORY_PROOF - ( - for (unsigned i = 0; i < d_assertions.size(); ++i) { - ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr()); - } - ); - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if( options::ceGuidedInst() ){ |