More fixes

2 files changed, 12 insertions, 4 deletions

diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g
index 47cebbbb0..863b15a95 100644
--- a/src/parser/cvc/cvc_lexer.g
+++ b/src/parser/cvc/cvc_lexer.g
@@ -71,6 +71,13 @@ COLON options{ paraphrase = "a colon"; }
   ;
 
 /**
+ * Matches the 'l'
+ */
+SEMICOLON options{ paraphrase = "a semicolon"; } 
+  : ';'
+  ;
+
+/**
  * Matches the ','
  */
 COMMA options{ paraphrase = "a comma"; } 
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index c7f932a0c..a22ce64e7 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -54,15 +54,16 @@ command returns [CVC4::Command* cmd = 0]
   Expr f;
   vector<string> ids;
 }
-  : ASSERT   f = formula  { cmd = new AssertCommand(f);   }
-  | QUERY    f = formula  { cmd = new QueryCommand(f);    }
-  | CHECKSAT f = formula  { cmd = new CheckSatCommand(f); }
-  | CHECKSAT              { cmd = new CheckSatCommand();  }
+  : ASSERT   f = formula  SEMICOLON { cmd = new AssertCommand(f);   }
+  | QUERY    f = formula  SEMICOLON { cmd = new QueryCommand(f);    }
+  | CHECKSAT f = formula  SEMICOLON { cmd = new CheckSatCommand(f); }
+  | CHECKSAT              SEMICOLON { cmd = new CheckSatCommand();  }
   | identifierList[ids, CHECK_UNDECLARED] COLON type { 
       // [chris 12/15/2009] FIXME: decls may not be BOOLEAN
       newPredicates(ids); 
       cmd = new DeclarationCommand(ids); 
     }
+    SEMICOLON
   | EOF 
   ;