From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 22 Jun 2014 06:56:37 +0000 (-0400)
Subject: Re-enable UNTERMINATED_QUOTED_SYMBOL rules.
X-Git-Tag: cvc5-1.0.0~6740
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b87a7546e15db91d39c7824390397e87eadc6d4;p=cvc5.git

Re-enable UNTERMINATED_QUOTED_SYMBOL rules.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8a2fa5225..8590229a2 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1557,12 +1557,12 @@ symbol[std::string& id,
         PARSER_STATE->checkDeclaration(id, check, type);
       }
     }
-  /*| UNTERMINATED_QUOTED_SYMBOL
+  | UNTERMINATED_QUOTED_SYMBOL
     ( EOF
       { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
     | '\\'
       { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| symbol"); }
-    )*/
+    )
   ;
 
 /**
@@ -1803,9 +1803,9 @@ EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
 QUOTED_SYMBOL
   : '|' ~('|' | '\\')* '|'
   ;
-/*UNTERMINATED_QUOTED_SYMBOL
+UNTERMINATED_QUOTED_SYMBOL
   : '|' ~('|' | '\\')*
-  ;*/
+  ;
 
 /**
  * Matches a keyword from the input. A keyword is a simple symbol prefixed