From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 18 Jun 2014 16:02:37 +0000 (-0400)
Subject: Better error for invalid concrete syntax of sorts with too many parens, like (Int... 
X-Git-Tag: cvc5-1.0.0~6758^2~8
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5d59ca8bbb1bfc557971c24a87e8ef9db9b69c33;p=cvc5.git

Better error for invalid concrete syntax of sorts with too many parens, like (Int).  Thanks to Dan Liew for the report.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 63179cf42..8590229a2 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1483,7 +1483,9 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
     }
   | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
     {
-      if(name == "Array" &&
+      if(args.empty()) {
+        PARSER_STATE->parseError("Extra parentheses around sort name not permitted in SMT-LIB");
+      } else if(name == "Array" &&
          PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) {
         if(args.size() != 2) {
           PARSER_STATE->parseError("Illegal array type.");