From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 19 Aug 2014 20:39:06 +0000 (-0400)
Subject: Produce error for bad indexed function names in SMT-LIB, remove antlr warning.
X-Git-Tag: cvc5-1.0.0~6509^2~36
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d69a876f0701441f7115828a5044c628e53abdd5;p=cvc5.git

Produce error for bad indexed function names in SMT-LIB, remove antlr warning.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 085cc11c8..e05ffaebe 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1236,8 +1236,8 @@ badIndexedFunctionName
 @declarations {
   std::string name;
 }
-  : symbol[name,CHECK_NONE,SYM_VARIABLE] INTEGER_LITERAL+
-      { PARSER_STATE->parseError(std::string("Unknown indexed function `") + name + "'"); }
+  : id=(SIMPLE_SYMBOL | QUOTED_SYMBOL | UNTERMINATED_QUOTED_SYMBOL)
+      { PARSER_STATE->parseError(std::string("Unknown indexed function `") + AntlrInput::tokenText($id) + "'"); }
   ;
 
 /**