diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-30 18:11:54 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-01 00:11:54 +0000 |
| commit | 0ca4a8043609a4e65adb9fcbcd79ecd8cd6e93a4 (patch) | |
| tree | 8e7af7f8adeb3e8dbcd3b236728ebc5e6f504b32 | |
| parent | 30f91833dea7f31156dafa401d17522b7fd87bc7 (diff) | |
Define sort undeclared (#7714)
Fixes cvc5/cvc5-projects#369.
Now gives:
(error "Parse Error: proj-369.smt2:3.22: Symbol 'Bool' previously declared as a type
(define-sort _s0 (Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
^
")
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index dbc65d90f..bdc5b32d4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -248,7 +248,7 @@ command [std::unique_ptr<cvc5::Command>* cmd] DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_SORT] { PARSER_STATE->checkUserSymbol(name); } - LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK + LPAREN_TOK symbolList[names,CHECK_UNDECLARED,SYM_SORT] RPAREN_TOK { PARSER_STATE->pushScope(); for(std::vector<std::string>::const_iterator i = names.begin(), iend = names.end(); |