Strings: Add a separate case for the escape sequence "\u{5c}" in unescapeUnicodeForSmtlib() as backslashes (= codepoint 5c) are considered special characters by Matcher.appendReplacement()

Author: daniel-raffler

src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java

@@ -104,7 +104,13 @@ public static String unescapeUnicodeForSmtlib(String input) {
       checkArgument(
           isCodePointInRange(codePoint),
           "SMTLIB does only specify Unicode letters from Planes 0-2");
-      matcher.appendReplacement(sb, Character.toString(codePoint));
+      String replacement = Character.toString(codePoint);
+      if (replacement.equals("\\")) {
+        // Matcher.appendReplacement considers '\' as special character.
+        // Substitute with '\\' instead
+        replacement = "\\\\";
+      }
+      matcher.appendReplacement(sb, replacement);
     }
     matcher.appendTail(sb);
     return sb.toString();