Add test for string literals length

Author: romainbrenguier

regression/jbmc-strings/literal-length/Test.class

@@ -0,0 +1,12 @@
+public class Test {
+    public static int check(int i) {
+        String s = "\u0000";
+
+        if (i == 0)
+            assert(s.length() == 1);
+        else if (i == 1)
+            assert(s.length() != 1);
+
+        return s.length();
+    }
+}

regression/jbmc-strings/literal-length/Test.java

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--refine-strings  --function Test.check
+assertion at file Test.java line 6 .* SUCCESS
+assertion at file Test.java line 8 .* FAILURE
+^EXIT=10$
+^SIGNAL=0$