Strings: Escape backslashes in Strings for Z3 when solver.useUnicodeStrings is set to false

Author: daniel-raffler

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -923,9 +923,11 @@ public Object convertValue(Long value) {
         return ratValue.isIntegral() ? ratValue.getNum() : ratValue;
       } else if (type.isStringType()) {
         String str = Native.getString(environment, value);
-        return isUnicodeEnabled()
-            ? AbstractStringFormulaManager.unescapeUnicodeForSmtlib(str)
-            : str;
+        // Calling `unescape` followed by ` escape` has the effect of escaping all backslashes
+        // that are not part of a valid escape sequence
+        String unicode = AbstractStringFormulaManager.unescapeUnicodeForSmtlib(str);
+        String escaped = AbstractStringFormulaManager.escapeUnicodeForSmtlib(unicode);
+        return isUnicodeEnabled() ? unicode : escaped;
       } else if (type.isBitvectorType()) {
         return new BigInteger(Native.getNumeralString(environment, value));
       } else if (type.isFloatingPointType()) {