diff options
author | Tim King <taking@google.com> | 2016-11-11 16:04:51 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-11-11 16:04:51 -0800 |
commit | 7e84a5e76ba83b5f73760589efb051970d58172f (patch) | |
tree | 7a5d51b1eea6594bf60faf4c9ec9ccbf80c3aed5 /src/parser/parser.h | |
parent | 17d74f82f0407db60d65d4bd24d35b383f1712ca (diff) |
Deleting the remaining commands in the Parser's queue within ~Parser().
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 351aa858a..b310456bd 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -230,6 +230,8 @@ class CVC4_PUBLIC Parser { * "Preemption commands": extra commands implied by subterms that * should be issued before the currently-being-parsed command is * issued. Used to support SMT-LIBv2 ":named" attribute on terms. + * + * Owns the memory of the Commands in the queue. */ std::list<Command*> d_commandQueue; @@ -254,9 +256,7 @@ protected: public: - virtual ~Parser() { - delete d_input; - } + virtual ~Parser(); /** Get the associated <code>ExprManager</code>. */ inline ExprManager* getExprManager() const { |