diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-08 17:55:23 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-08 17:55:23 -0400 |
| commit | 7bf6c4aa1dabef2f3abd14124b16cbf1900cf3de (patch) | |
| tree | 5ef28fe85e5d7b5a7decebd435c865dd320a2bfb /src | |
| parent | aee4775c89adf56df6b9a177f3666d79899863dd (diff) | |
Better error when there are \backslashes in |quoted symbols|.
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 39f746244..8fa047885 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1551,8 +1551,12 @@ symbol[std::string& id, PARSER_STATE->checkDeclaration(id, check, type); } } - | UNTERMINATED_QUOTED_SYMBOL EOF - { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); } + | UNTERMINATED_QUOTED_SYMBOL + ( EOF + { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); } + | '\\' + { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| symbol"); } + ) ; /** |