summaryrefslogtreecommitdiff
path: root/test/unit/parser/parser_black.h
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/parser/parser_black.h')
-rw-r--r--test/unit/parser/parser_black.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index f288f6b1a..632db2b91 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -200,6 +200,7 @@ public:
void testGoodCvc4Inputs() {
tryGoodInput(""); // empty string is OK
+ tryGoodInput(";"); // no command is OK
tryGoodInput("ASSERT TRUE;");
tryGoodInput("QUERY TRUE;");
tryGoodInput("CHECKSAT FALSE;");
@@ -219,7 +220,6 @@ public:
}
void testBadCvc4Inputs() {
- tryBadInput(";"); // no command
tryBadInput("ASSERT;"); // no args
tryBadInput("QUERY");
tryBadInput("CHECKSAT");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback