Add regression test for bug of char to string conversion

After converting '\uFFFF' to string the result differs from "\uFFFF" for a check
with `equals()`.

Author: danpoe

jbmc/regression/jbmc-strings/CharToString/Test.class

@@ -0,0 +1,13 @@
+public class Test {
+  public void test1() {
+    char c = '\uFFFF';
+    String s = String.valueOf(c);
+    assert s.equals("\uFFFF");
+  }
+
+  public void test2() {
+    char c = '\uFFFE';
+    String s = String.valueOf(c);
+    assert s.equals("\uFFFE");
+  }
+}

jbmc/regression/jbmc-strings/CharToString/Test.java

@@ -0,0 +1,6 @@
+KNOWNBUG
+Test.class
+--function Test.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/CharToString/test1.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$