Add a regression test with Character type

Author: yumibagge

jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Charactor/Main.class

@@ -0,0 +1,10 @@
+public class Main {
+    public void constantIndexOf() {
+        String s1 = "abcabc";
+        Character b = 'b';
+        assert s1.indexOf(b) == 1;
+        assert s1.indexOf(b, -10) == 1;
+        assert s1.indexOf(b, 3) == 4;
+        assert s1.indexOf(b, 10) == -1;
+    }
+}

jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Charactor/Main.java

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Charactor/test-models-library.desc

@@ -0,0 +1,12 @@
+KNOWNBUG symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This is tentatively set to KNOWNBUG as it will fail verification and root cause
+not yet found out why verification failed without models-library and with
+Character.