diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 160a16652..352db6789 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3107,7 +3107,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc Assert(ex.isNull() || ex.getExprManager() == d_exprManager); #ifdef CVC4_PROOF // if (options::proof()) { <-- SEGFAULT!! - ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); + ProofManager::currentPM()->addAssertion(ex); //} #endif SmtScope smts(this); @@ -3255,7 +3255,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log Assert(ex.getExprManager() == d_exprManager); #ifdef CVC4_PROOF // if (options::proof()) { <-- SEGFAULT!!! - ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); + ProofManager::currentPM()->addAssertion(ex); // } #endif SmtScope smts(this); |