numerous bugfixes

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");