diff options
author | lianah <lianahady@gmail.com> | 2013-10-09 15:48:42 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-09 15:48:42 -0400 |
commit | 44485520fae92b34e4385d4d2c4774c9dd7d0dc0 (patch) | |
tree | 6a3608afa6276e11e1a72504c439a4991e9dea41 /src/smt | |
parent | 08c8433e4ab849024930a8c4dbe8756e13d08099 (diff) |
cleaned up proof code
Diffstat (limited to 'src/smt')
-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); |