Incorrect handling of SMT-LIB double-quote escape sequence in strings

[Calvin-L]

(I am using Boolector 3.2.1, the latest release. I have not checked if this issue is fixed in more recent commits.)

The SMT-LIB standard specifies (since version 2.5) that "" represents a single double quote inside a double-quoted string. Boolector mishandles this:

$ boolector --smt2 <<<'(echo "str""ing") (echo "hi")'
"str""hi"

The text "str""ing" is a single literal representing the string str"ing. Boolector's output should be

"str""ing"
"hi"

Since version 2.5, the SMT-LIB standard also does not include any backslash escape sequences. That is, inside a string literal, \ represents a single backslash and not the start of a two-character escape sequence. \\ represents two backslashes. This is an unfortunate difference from the 2.0 standard, which specified that \\ and \" represented backslash and double-quote, respectively.

There is also a second, more subtle related issue: Boolector does not output any characters (not even newline) following the terminating " in "hi". To a tool consuming output, this is ambiguous: the terminating " may be the end of the string or the start of the double-quote escape sequence, depending on the next character in the output.

[aniemetz]

Thanks for catching this! Fixed in https://github.com/Boolector/boolector/commit/e34ac0416ef318233458fc3ce52f0039b304abeb and https://github.com/Boolector/boolector/commit/973232c4e83cd73c23f2f6926c6b642a9dbb3fb3.