diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/system/ouroborous.cpp | 1 | ||||
| -rw-r--r-- | test/unit/parser/parser_black.h | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index abce24751..ac864d16b 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -127,6 +127,7 @@ int runTest() { runTestString("(= (f (f y)) x)"); runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4); + runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", input::LANG_CVC4); runTestString("a[x][y] = a[y][x]", input::LANG_CVC4); delete psr; 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"); |