Add regression test for 2byte char

Author: yumibagge

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.class

@@ -0,0 +1,9 @@
+public class Main {
+  public void test() {
+    String s1 = "ディフ";
+    String s2 = "ブルー";
+    String s3 = s1 + s2;
+    assert s3.length() == 6;
+    assert s3.startsWith("ディフブルー");
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.java

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--