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
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")