Strings: Always unescape the String first when creating a new String constant.

This is needed even for solvers like CVC4+5 or Z3 that expect Unicode characters to be escaped. We first need to unescape the String to resolve any escape sequences from the user, and then apply escape again before sending the String to the solver.

Author: daniel-raffler

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java

@@ -29,8 +29,8 @@ class CVC4StringFormulaManager extends AbstractStringFormulaManager<Expr, Type,
 
   @Override
   protected Expr makeStringImpl(String pValue) {
-    // The boolean enables escape characters!
-    return exprManager.mkConst(new CVC4String(escapeUnicodeForSmtlib(pValue), true));
+    String str = escapeUnicodeForSmtlib(unescapeUnicodeForSmtlib(pValue));
+    return exprManager.mkConst(new CVC4String(str, true));
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java

@@ -27,7 +27,8 @@ class CVC5StringFormulaManager extends AbstractStringFormulaManager<Term, Sort,
 
   @Override
   protected Term makeStringImpl(String pValue) {
-    return solver.mkString(escapeUnicodeForSmtlib(pValue), true);
+    String str = escapeUnicodeForSmtlib(unescapeUnicodeForSmtlib(pValue));
+    return solver.mkString(str, true);
   }
 
   @Override

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

@@ -25,7 +25,8 @@ class Z3StringFormulaManager extends AbstractStringFormulaManager<Long, Long, Lo
 
   @Override
   protected Long makeStringImpl(String pValue) {
-    return Native.mkString(z3context, escapeUnicodeForSmtlib(pValue));
+    String str = escapeUnicodeForSmtlib(unescapeUnicodeForSmtlib(pValue));
+    return Native.mkString(z3context, str);
   }
 
   @Override