summaryrefslogtreecommitdiff
path: root/src/smt/command.h
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-11-15 02:58:30 -0800
committerAndres Noetzli <andres.noetzli@gmail.com>2017-11-15 02:58:30 -0800
commit3c130b44fdecc62b1ace2a739e77f913cd606aa0 (patch)
tree6abfb806dd45c83606c04dda5c26e9c410ac2ee1 /src/smt/command.h
parent85df7998e4362e0a9c796146d07d7b9e91045a31 (diff)
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/smt/command.h')
-rw-r--r--src/smt/command.h5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/smt/command.h b/src/smt/command.h
index a60c85a3c..33f58aa99 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -637,7 +637,7 @@ class CVC4_PUBLIC GetProofCommand : public Command {
GetProofCommand() throw();
~GetProofCommand() throw() {}
void invoke(SmtEngine* smtEngine);
- Proof* getResult() const throw();
+ const Proof& getResult() const throw();
void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap);
@@ -645,8 +645,9 @@ class CVC4_PUBLIC GetProofCommand : public Command {
std::string getCommandName() const throw();
protected:
- Proof* d_result;
SmtEngine* d_smtEngine;
+ // d_result is owned by d_smtEngine.
+ const Proof* d_result;
}; /* class GetProofCommand */
class CVC4_PUBLIC GetInstantiationsCommand : public Command {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback