When the syntax was updated to the new SMT-LIB standard for the theory
of strings, not all of the escape characters were converted. In
particular, some of the benchmarks contained escape characters such as
\n, \t, etc. that were ommitted. Since there was no standard before,
there is some ambiguity in how those escape characters should be
translated. However, a lot of benchmarks have constraints such as (= (str.charat ...) "\n") which only really make sense when interpreting
"\n" as a single character. This commit replaces \\, \t, \n,
\v, \f, and \r by the corresponding new escape sequences.
As a sanity check, I did the following:
- I ran CVC4 1.7 on the benchmarks from SMT-COMP 2019
- I converted additional escape characters on all of the benchmarks from SMT-COMP 2020
- I ran a recent version of CVC4 on this version of the benchmarks and made sure that the status matched on all the benchmarks
For 47985 benchmarks, both versions of CVC4 computed the same status (and on the rest of the benchmarks one of the versions timed out). As an additional check, I ran a recent version of CVC4 on the current version of the benchmarks and confirmed that the status of 9788 benchmarks was different. Thus, this change should be an improvement over the current version of the benchmarks.