Changing some deatils on the parser. Now we know we are done if command is null, or expression is null.

3 files changed, 9 insertions, 15 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 595915100..4731c536e 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -108,15 +108,13 @@ int main(int argc, char *argv[]) {
     }
 
     // Parse and execute commands until we are done
-    while(!parser->done()) {
-      // Parse the next command
-      Command *cmd = parser->parseNextCommand();
-      if(cmd) {
-        if(options.verbosity > 0)
-          cout << "Invoking: " << *cmd << endl;
-        cmd->invoke(&smt);
-        delete cmd;
+    Command* cmd;
+    while((cmd = parser->parseNextCommand())) {
+      if(options.verbosity > 0) {
+        cout << "Invoking: " << *cmd << endl;
       }
+      cmd->invoke(&smt);
+      delete cmd;
     }
 
     // Remove the parser
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 0a4b180ec..7b4810abb 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -42,14 +42,10 @@ bool Parser::done() const {
 }
 
 Command* Parser::parseNextCommand() throw(ParserException, AssertionException) {
-  Command* cmd = 0;
+  Command* cmd = NULL;
   if(!done()) {
     try {
       cmd = d_antlrParser->parseCommand();
-      if(cmd == 0) {
-        setDone();
-        cmd = new EmptyCommand("EOF");
-      }
     } catch(antlr::ANTLRException& e) {
       setDone();
       throw ParserException(e.toString());
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 645882724..1d4afbb7c 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -81,13 +81,13 @@ const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string);
 
 const string goodSmtInputs[] = {
     "", // empty string is OK
-    "(benchmark foo :assume true)",
+    "(benchmark foo :assumption true)",
     "(benchmark bar :formula true)",
     "(benchmark qux :formula false)",
     "(benchmark baz :extrapreds ( (a) (b) ) )",
     "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))",
     ";; nothing but a comment",
-    "; a comment\n)(benchmark foo ; hello\n  :formula true; goodbye\n)"
+    "; a comment\n(benchmark foo ; hello\n  :formula true; goodbye\n)"
   };
 
 const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string);