From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Tue, 4 May 2010 21:57:53 +0000 (+0000)
Subject: Minor change to SMT v2 grammar
X-Git-Tag: cvc5-1.0.0~9081
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1571e73e83ecb5fec2f2ddd599bd3823e8f532e7;p=cvc5.git

Minor change to SMT v2 grammar
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 76ce91fd0..19997cdd0 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -137,8 +137,9 @@ command returns [CVC4::Command* cmd]
   SExpr sexpr;
 }
   : /* set the logic */
-    SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
-    { Debug("parser") << "set logic: '" << name << "' " << std::endl;
+    SET_LOGIC_TOK SYMBOL
+    { name = AntlrInput::tokenText($SYMBOL);
+      Debug("parser") << "set logic: '" << name << "' " << std::endl;
       setLogic(PARSER_STATE,name);
       $cmd = new SetBenchmarkLogicCommand(name); }
   | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
@@ -425,7 +426,7 @@ TILDE_TOK         : '~';
 XOR_TOK           : 'xor';
 
 /**
- * Matches a symbol from the input. A symbol is a "simple" symbole or a 
+ * Matches a symbol from the input. A symbol is a "simple" symbol or a 
  * sequence of printable ASCII characters that starts and ends with | and 
  * does not otherwise contain |.
  */
@@ -435,7 +436,7 @@ SYMBOL
   ;
 
 /**
- * Matches a keyword from the input. A keyword is a symbol symbol, prefixed
+ * Matches a keyword from the input. A keyword is a simple symbol prefixed
  * with a colon.
  */
 KEYWORD