diff options
| author | Tim King <taking@cs.nyu.edu> | 2017-11-15 02:58:30 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-11-15 02:58:30 -0800 |
| commit | 3c130b44fdecc62b1ace2a739e77f913cd606aa0 (patch) | |
| tree | 6abfb806dd45c83606c04dda5c26e9c410ac2ee1 /src/smt/smt_engine_check_proof.cpp | |
| parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) | |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/smt/smt_engine_check_proof.cpp')
| -rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index f48f6753d..76a30ef9b 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -32,6 +32,7 @@ #include "base/cvc4_assert.h" #include "base/output.h" #include "smt/smt_engine.h" +#include "util/proof.h" #include "util/statistics_registry.h" #if (IS_LFSC_BUILD && IS_PROOFS_BUILD) @@ -66,7 +67,7 @@ void SmtEngine::checkProof() { Chat() << "generating proof..." << endl; - Proof* pf = getProof(); + const Proof& pf = getProof(); Chat() << "checking proof..." << endl; @@ -112,7 +113,7 @@ void SmtEngine::checkProof() { ofstream pfStream(pfFile); pfStream << proof::plf_signatures << endl; - pf->toStream(pfStream); + pf.toStream(pfStream); pfStream.close(); lfscc_init(); lfscc_check_file(pfFile, false, false, false, false, false, false, false); |