"" escape sequence not supported in strings

[stevenmeker]

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