Activate tests fixed by getChar models

Author: romainbrenguier

jbmc/regression/jbmc-strings/StringBuilderChars01/test.desc

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 StringBuilderChars01.class
---max-nondet-string-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 StringBuilderChars04.class
---max-nondet-string-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 StringMiscellaneous01.class
---max-nondet-string-length 1000 --unwind 30
+--max-nondet-string-length 1000 --unwind 30 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$