Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"" escape sequence not supported in strings #417

Open
stevenmeker opened this issue Nov 5, 2022 · 0 comments
Open

"" escape sequence not supported in strings #417

stevenmeker opened this issue Nov 5, 2022 · 0 comments

Comments

@stevenmeker
Copy link

https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
Page 22: The character " can itself occur within a string literal only if duplicated.
In other words, after an initial " that starts a literal, a lexer should treat the
sequence "" as an escape sequence denoting a single occurrence of " within the literal.

./yices_smt2 --version
Yices 2.6.4
Copyright SRI International.
Linked with GMP 6.2.0
Copyright Free Software Foundation, Inc.
Build date: 2022-11-03
Platform: x86_64-pc-linux-gnu (release)
Revision: unknown

(echo "foo""bar")
(error "at line 1, column 17: syntax error: ) expected")

(set-option :diagnostic-output-channel "foo""bar")
(error "at line 1, column 50: syntax error: ) expected")

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant