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/command.cpp | |
parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 3df2c4f41..aea6365b7 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1210,12 +1210,12 @@ std::string GetModelCommand::getCommandName() const throw() { /* class GetProofCommand */ GetProofCommand::GetProofCommand() throw() - : d_result(nullptr), d_smtEngine(nullptr) {} + : d_smtEngine(nullptr), d_result(nullptr) {} void GetProofCommand::invoke(SmtEngine* smtEngine) { try { d_smtEngine = smtEngine; - d_result = smtEngine->getProof(); + d_result = &smtEngine->getProof(); d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); @@ -1226,10 +1226,7 @@ void GetProofCommand::invoke(SmtEngine* smtEngine) { } } -Proof* GetProofCommand::getResult() const throw() { - return d_result; -} - +const Proof& GetProofCommand::getResult() const throw() { return *d_result; } void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const { if(! ok()) { this->Command::printResult(out, verbosity); |