diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-18 12:02:37 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-18 12:02:37 -0400 |
commit | 5d59ca8bbb1bfc557971c24a87e8ef9db9b69c33 (patch) | |
tree | e8c112b78e852b8fc7cc34e83cf89fa2d58b1a6b | |
parent | e77ded9307cd64aaaa8fe79a28f9c715ece3794e (diff) |
Better error for invalid concrete syntax of sorts with too many parens, like (Int). Thanks to Dan Liew for the report.
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 3 insertions, 1 deletions
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."); |