diff options
| author | Tim King <taking@google.com> | 2016-11-13 00:33:40 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-11-13 00:33:40 -0800 |
| commit | d8ce5358ad4d40eb2d86fe17fead9dc258d155b5 (patch) | |
| tree | 2336fd6ce993190bd7526592811164d11989dae7 /test/unit | |
| parent | f2cb814468472e533163f1d31cb08dfe3eacbe32 (diff) | |
Deleting a parsed Command in the interactive_shell_black test.
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/main/interactive_shell_black.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index 9ac81781c..5e9d43dd4 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -26,6 +26,7 @@ #include "options/language.h" #include "options/options.h" #include "parser/parser_builder.h" +#include "smt/command.h" using namespace CVC4; using namespace std; @@ -97,9 +98,10 @@ private: InteractiveShell shell(*d_exprManager, d_options); /* readCommand may return a sequence, see above. */ *d_sin << "x : REAL;\n" << flush; - shell.readCommand(); + Command* tmp = shell.readCommand(); *d_sin << "ASSERT x > 0;\n" << flush; countCommands( shell, 1, 1 ); + delete tmp; } void testEmptyLine() { |