summaryrefslogtreecommitdiff
path: root/test/unit/main
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/main')
-rw-r--r--test/unit/main/interactive_shell_black.h4
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() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback