diff options
Diffstat (limited to 'test')
-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() { |