SRI-CSL / yices2 / 29183493071

71%

Build Type

push

github

Committed by web-flow

Commit Message

Make the SMT-LIB 2.6 "" string escape the default (#417) (#653)

The "" escape (a double quote inside a string literal is written by
doubling it) was only accepted when a script declared
(set-info :smt-lib-version 2.5|2.6); otherwise Yices used the legacy
pre-2.5 escapes (\" and \\), so standard 2.6 input like (echo "foo""bar")
failed with a syntax error.

Since SMT-LIB 2.6 is the current standard, use its string syntax
unconditionally. This drops the legacy escapes, so the two string readers
collapse into one and the two_dot_five_variant flag / activation machinery
is removed. smt2_echo likewise always escapes with "".

- add regression test iss417
- update iss416 to use "" escapes (the legacy \" case no longer parses)
- update the brummayerbiere coverage benchmark's :source metadata to ""

Coverage Stats

4 of 4 new or added lines in 2 files covered. (100.0%)

7 existing lines in 1 file now uncovered.

95538 of 134173 relevant lines covered (71.21%)

1667019.91 hits per line