diff --git a/regression/strings/Makefile b/regression/strings/Makefile
index 545b36925ac..f9aee8c563e 100644
--- a/regression/strings/Makefile
+++ b/regression/strings/Makefile
@@ -1,3 +1,6 @@
 
 test:
-	../test.pl -c ../../../src/cbmc/cbmc
+	@../test.pl -c ../../../src/cbmc/cbmc
+
+testfuture:
+	@../test.pl -c ../../../src/cbmc/cbmc -F
diff --git a/regression/strings/cprover-string-hack.h b/regression/strings/cprover-string-hack.h
index 9160e935529..1ec17bca535 100644
--- a/regression/strings/cprover-string-hack.h
+++ b/regression/strings/cprover-string-hack.h
@@ -56,7 +56,7 @@ typedef unsigned char __CPROVER_char;
  ******************************************************************************/
 extern __CPROVER_char __CPROVER_uninterpreted_string_char_at_func(__CPROVER_string str, int pos);
 extern __CPROVER_bool __CPROVER_uninterpreted_string_equal_func(__CPROVER_string str1, __CPROVER_string str2);
-extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func();
+extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func(char * str);
 extern __CPROVER_char __CPROVER_uninterpreted_char_literal_func();
 extern __CPROVER_string __CPROVER_uninterpreted_string_concat_func(__CPROVER_string str1, __CPROVER_string str2);
 extern int __CPROVER_uninterpreted_string_length_func(__CPROVER_string str);
@@ -68,5 +68,5 @@ extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __
 extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, __CPROVER_char c);
 extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, __CPROVER_char c);
 extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func(__CPROVER_string str);
-extern unsigned __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
-extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(unsigned i);
+extern int __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
+extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(int i);
diff --git a/regression/strings/java_case/test.desc b/regression/strings/java_case/test.desc
index 49ea16d56ff..9f48288c694 100644
--- a/regression/strings/java_case/test.desc
+++ b/regression/strings/java_case/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_case.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_case.java line 11: SUCCESS$
diff --git a/regression/strings/java_char_array/test.desc b/regression/strings/java_char_array/test.desc
new file mode 100644
index 00000000000..8282b808b84
--- /dev/null
+++ b/regression/strings/java_char_array/test.desc
@@ -0,0 +1,9 @@
+FUTURE
+test_char_array.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_char_array.java line 11: SUCCESS$
+^\[assertion.2\] assertion at file test_char_array.java line 12: SUCCESS$
+^\[assertion.3\] assertion at file test_char_array.java line 13: FAILURE$
+--
diff --git a/regression/strings/java_char_array/test_char_array.class b/regression/strings/java_char_array/test_char_array.class
new file mode 100644
index 00000000000..836942da134
Binary files /dev/null and b/regression/strings/java_char_array/test_char_array.class differ
diff --git a/regression/strings/java_char_array/test_char_array.java b/regression/strings/java_char_array/test_char_array.java
new file mode 100644
index 00000000000..3cfd4000d3a
--- /dev/null
+++ b/regression/strings/java_char_array/test_char_array.java
@@ -0,0 +1,15 @@
+public class test_char_array {
+
+    public static void main(String[] argv)
+    {
+        String s = "abc";
+        char [] str = s.toCharArray();
+        int[] test = new int[312];
+        char c = str[2];
+        String t = argv[0];
+        char d = t.charAt(0);
+        assert(str.length == 3);
+        assert(c == 'c');
+        assert(c == d || d < 'a' || d > 'z' );
+    }
+}
diff --git a/regression/strings/java_char_array_init/test.desc b/regression/strings/java_char_array_init/test.desc
new file mode 100644
index 00000000000..fe5ffae7238
--- /dev/null
+++ b/regression/strings/java_char_array_init/test.desc
@@ -0,0 +1,11 @@
+FUTURE
+test_init.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_init.java line 16: SUCCESS$
+^\[assertion.2\] assertion at file test_init.java line 17: SUCCESS$
+^\[assertion.3\] assertion at file test_init.java line 18: SUCCESS$
+^\[assertion.4\] assertion at file test_init.java line 20: SUCCESS$
+^\[assertion.5\] assertion at file test_init.java line 21: FAILURE$
+--
diff --git a/regression/strings/java_char_array_init/test_init.class b/regression/strings/java_char_array_init/test_init.class
new file mode 100644
index 00000000000..be3baee56bd
Binary files /dev/null and b/regression/strings/java_char_array_init/test_init.class differ
diff --git a/regression/strings/java_char_array_init/test_init.java b/regression/strings/java_char_array_init/test_init.java
new file mode 100644
index 00000000000..5f4e220844c
--- /dev/null
+++ b/regression/strings/java_char_array_init/test_init.java
@@ -0,0 +1,23 @@
+public class test_init {
+
+    public static void main(String[] argv)
+    {
+	char [] str = new char[10];
+	str[0] = 'H';
+	str[1] = 'e';
+	str[2] = 'l';
+	str[3] = 'l';
+	str[4] = 'o';
+	String s = new String(str);
+	String t = new String(str,1,2);
+
+	System.out.println(s);
+	System.out.println(s.length());
+	assert(s.startsWith("Hello"));
+	assert(s.length() == 10);
+	assert(t.equals("el"));
+	String u = String.valueOf(str,3,2);
+	assert(u.equals("lo"));
+	assert(s.equals("Hello") || !t.equals("el") || !u.equals("lo"));
+    }
+}
diff --git a/regression/strings/java_char_at/test.desc b/regression/strings/java_char_at/test.desc
index babcc395bcf..6f206a0f22f 100644
--- a/regression/strings/java_char_at/test.desc
+++ b/regression/strings/java_char_at/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_char_at.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_char_at.java line 11: SUCCESS$
diff --git a/regression/strings/java_code_point/test.desc b/regression/strings/java_code_point/test.desc
index 1543a327fa4..35ca0cd6f4b 100644
--- a/regression/strings/java_code_point/test.desc
+++ b/regression/strings/java_code_point/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_code_point.class
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_code_point.java line 5: SUCCESS$
diff --git a/regression/strings/java_compare/test.desc b/regression/strings/java_compare/test.desc
index c500900a21e..517b208c3e4 100644
--- a/regression/strings/java_compare/test.desc
+++ b/regression/strings/java_compare/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_compare.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_compare.java line 6: SUCCESS$
diff --git a/regression/strings/java_concat/test.desc b/regression/strings/java_concat/test.desc
index c6c0b193e5b..8ef2898e0d7 100644
--- a/regression/strings/java_concat/test.desc
+++ b/regression/strings/java_concat/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_concat.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_concat.java line 9: SUCCESS$
diff --git a/regression/strings/java_contains/test.desc b/regression/strings/java_contains/test.desc
index ade6b433bf1..4e7a3bd4f7d 100644
--- a/regression/strings/java_contains/test.desc
+++ b/regression/strings/java_contains/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test_contains.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_contains.java line 7: SUCCESS$
diff --git a/regression/strings/java_delete/test.desc b/regression/strings/java_delete/test.desc
index 377ada44770..c6c608c0955 100644
--- a/regression/strings/java_delete/test.desc
+++ b/regression/strings/java_delete/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test_delete.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_delete.java line 11: SUCCESS$
diff --git a/regression/strings/java_easychair/test.desc b/regression/strings/java_easychair/test.desc
index bd68fd1f60a..8680af72c5a 100644
--- a/regression/strings/java_easychair/test.desc
+++ b/regression/strings/java_easychair/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 easychair.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file easychair.java line 29: FAILURE$
diff --git a/regression/strings/java_empty/test.desc b/regression/strings/java_empty/test.desc
index 56b21e2041c..cab514b80b5 100644
--- a/regression/strings/java_empty/test.desc
+++ b/regression/strings/java_empty/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_empty.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_empty.java line 4: SUCCESS$
diff --git a/regression/strings/java_equal/test.desc b/regression/strings/java_equal/test.desc
index 6375cfdc3d8..d66c30b26fe 100644
--- a/regression/strings/java_equal/test.desc
+++ b/regression/strings/java_equal/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_equal.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_equal.java line 7: FAILURE$
diff --git a/regression/strings/java_float/test.desc b/regression/strings/java_float/test.desc
index 5edfd6eea22..955f0358eab 100644
--- a/regression/strings/java_float/test.desc
+++ b/regression/strings/java_float/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_float.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_float.java line 14: SUCCESS$
diff --git a/regression/strings/java_index_of/test.desc b/regression/strings/java_index_of/test.desc
index dd5c60464d5..daa6c32493b 100644
--- a/regression/strings/java_index_of/test.desc
+++ b/regression/strings/java_index_of/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_index_of.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_index_of.java line 13: SUCCESS$
diff --git a/regression/strings/java_int/test.desc b/regression/strings/java_int/test.desc
index 5211656c61b..ae60dd78af0 100644
--- a/regression/strings/java_int/test.desc
+++ b/regression/strings/java_int/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_int.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_int.java line 8: SUCCESS$
diff --git a/regression/strings/java_prefix/test.desc b/regression/strings/java_prefix/test.desc
index b234bba1788..175f934ca1d 100644
--- a/regression/strings/java_prefix/test.desc
+++ b/regression/strings/java_prefix/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_prefix.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_prefix.java line 14: SUCCESS$
diff --git a/regression/strings/java_replace/test.desc b/regression/strings/java_replace/test.desc
index a5b15efd737..1e89ebe37b4 100644
--- a/regression/strings/java_replace/test.desc
+++ b/regression/strings/java_replace/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_replace.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_replace.java line 6: SUCCESS$
diff --git a/regression/strings/java_set_length/test.desc b/regression/strings/java_set_length/test.desc
index 66cf52835ac..43f82a648fd 100644
--- a/regression/strings/java_set_length/test.desc
+++ b/regression/strings/java_set_length/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_set_length.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_set_length.java line 8: SUCCESS$
diff --git a/regression/strings/java_string_builder/test.desc b/regression/strings/java_string_builder/test.desc
index c0b3b6a51ce..9712205b104 100644
--- a/regression/strings/java_string_builder/test.desc
+++ b/regression/strings/java_string_builder/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_string_builder.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_string_builder.java line 11: SUCCESS$
diff --git a/regression/strings/java_string_builder_insert/test.desc b/regression/strings/java_string_builder_insert/test.desc
new file mode 100644
index 00000000000..2655f846da1
--- /dev/null
+++ b/regression/strings/java_string_builder_insert/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+test_insert.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_insert.java line 17: SUCCESS$
+^\[assertion.2\] assertion at file test_insert.java line 18: FAILURE$
+--
diff --git a/regression/strings/java_string_builder_insert/test_insert.class b/regression/strings/java_string_builder_insert/test_insert.class
new file mode 100644
index 00000000000..69a32d7f93f
Binary files /dev/null and b/regression/strings/java_string_builder_insert/test_insert.class differ
diff --git a/regression/strings/java_string_builder_insert/test_insert.java b/regression/strings/java_string_builder_insert/test_insert.java
new file mode 100644
index 00000000000..1fac897c5ed
--- /dev/null
+++ b/regression/strings/java_string_builder_insert/test_insert.java
@@ -0,0 +1,20 @@
+public class test_insert {
+
+    public static void main(String[] argv)
+    {
+	char [] str = new char[5];
+	str[0] = 'H';
+	str[1] = 'e';
+	str[2] = 'l';
+	str[3] = 'l';
+	str[4] = 'o';
+
+
+	StringBuilder sb = new StringBuilder(" world");
+	sb.insert(0,str);
+	String s = sb.toString();
+	System.out.println(s);
+	assert(s.equals("Hello world"));
+	assert(!s.equals("Hello world"));
+    }
+}
diff --git a/regression/strings/java_string_builder_length/test.desc b/regression/strings/java_string_builder_length/test.desc
index a15660ee85b..c4720992571 100644
--- a/regression/strings/java_string_builder_length/test.desc
+++ b/regression/strings/java_string_builder_length/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_sb_length.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 \[assertion.1\] assertion at file test_sb_length.java line 6: SUCCESS$
diff --git a/regression/strings/java_strlen/test.desc b/regression/strings/java_strlen/test.desc
index 78007186493..b98e6f76f0a 100644
--- a/regression/strings/java_strlen/test.desc
+++ b/regression/strings/java_strlen/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_length.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_length.java line 10: SUCCESS$
diff --git a/regression/strings/java_substring/test.desc b/regression/strings/java_substring/test.desc
index 78a9bcca9cb..bd54a8204fe 100644
--- a/regression/strings/java_substring/test.desc
+++ b/regression/strings/java_substring/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_substring.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_substring.java line 12: SUCCESS$
diff --git a/regression/strings/java_suffix/test.desc b/regression/strings/java_suffix/test.desc
index f9472f03b47..2740e87d6e4 100644
--- a/regression/strings/java_suffix/test.desc
+++ b/regression/strings/java_suffix/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_suffix.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_suffix.java line 12: SUCCESS$
diff --git a/regression/strings/java_trim/test.desc b/regression/strings/java_trim/test.desc
index fa0e10a1ca7..7c0f1a87978 100644
--- a/regression/strings/java_trim/test.desc
+++ b/regression/strings/java_trim/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_trim.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_trim.java line 5: SUCCESS$
diff --git a/regression/strings/test1/test.c b/regression/strings/test1/test.c
index d3830e38a3f..c5e10eb1fc7 100644
--- a/regression/strings/test1/test.c
+++ b/regression/strings/test1/test.c
@@ -5,13 +5,13 @@
 int main()
 {
     __CPROVER_string s;
-    __CPROVER_char c1, c2;
+    char c1, c2;
     int i;
     int j;
     i = 2;
     s = __CPROVER_string_literal("pippo");
     c1 = __CPROVER_char_at(s, i);
-    c2 = __CPROVER_char_literal("p");
+    c2 = 'p';
     assert (c1 == c2);
     assert (c1 != c2);
     return 0;
diff --git a/regression/strings/test1/test.desc b/regression/strings/test1/test.desc
index f622390356d..b86ded86c18 100644
--- a/regression/strings/test1/test.desc
+++ b/regression/strings/test1/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion c1 == c2: SUCCESS$
diff --git a/regression/strings/test2/test.desc b/regression/strings/test2/test.desc
index d3054f813f1..b322a1d0d33 100644
--- a/regression/strings/test2/test.desc
+++ b/regression/strings/test2/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion n == 5: SUCCESS$
diff --git a/regression/strings/test3.1/test.desc b/regression/strings/test3.1/test.desc
index 0f5bd6ccca7..c88a62b6704 100644
--- a/regression/strings/test3.1/test.desc
+++ b/regression/strings/test3.1/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3.2/test.desc b/regression/strings/test3.2/test.desc
index 0f5bd6ccca7..c88a62b6704 100644
--- a/regression/strings/test3.2/test.desc
+++ b/regression/strings/test3.2/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3.3/test.c b/regression/strings/test3.3/test.c
index 35e25d82ee5..bef96c6cd4e 100644
--- a/regression/strings/test3.3/test.c
+++ b/regression/strings/test3.3/test.c
@@ -16,7 +16,7 @@ int main()
     // proving the assertions individually seems to be much faster
     //assert(__CPROVER_string_length(s) == i + 5);
     //assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"), s));
-    assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p"));
+    assert(__CPROVER_char_at(s, i) == 'p');
 
     return 0;
 }
diff --git a/regression/strings/test3.3/test.desc b/regression/strings/test3.3/test.desc
index 0f5bd6ccca7..c88a62b6704 100644
--- a/regression/strings/test3.3/test.desc
+++ b/regression/strings/test3.3/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3.4/test.desc b/regression/strings/test3.4/test.desc
index dbf3c40cfdb..d88e1c83744 100644
--- a/regression/strings/test3.4/test.desc
+++ b/regression/strings/test3.4/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/test3/test.c b/regression/strings/test3/test.c
index 2fa4b22e017..cbfc398099e 100644
--- a/regression/strings/test3/test.c
+++ b/regression/strings/test3/test.c
@@ -14,7 +14,7 @@ int main()
 
     assert(__CPROVER_string_length(s) == i + 5);
     assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"),s));
-    assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p"));
+    assert(__CPROVER_char_at(s, i) == 'p');
     assert(__CPROVER_string_issuffix(__CPROVER_string_literal("p!o"), s));
 
     return 0;
diff --git a/regression/strings/test3/test.desc b/regression/strings/test3/test.desc
index 6cacec86a19..54e56188c1b 100644
--- a/regression/strings/test3/test.desc
+++ b/regression/strings/test3/test.desc
@@ -1,10 +1,10 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s) == i + 5: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$
-^\[main.assertion.3\] assertion __CPROVER_uninterpreted_string_char_at_func(s, i) == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$
-^\[main.assertion.4\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"p!o\"), s): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_length(s) == i + 5: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"po\"),s): SUCCESS$
+^\[main.assertion.3\] assertion __CPROVER_char_at(s, i) == .p.: SUCCESS$
+^\[main.assertion.4\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"p!o\"), s): FAILURE$
 --
diff --git a/regression/strings/test4/test.c b/regression/strings/test4/test.c
index d73324f8ef4..3c768717823 100644
--- a/regression/strings/test4/test.c
+++ b/regression/strings/test4/test.c
@@ -9,7 +9,7 @@ int main()
     int j;
     i = 2;
     s = __CPROVER_string_literal("pippo");
-    if (__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")) {
+    if (__CPROVER_char_at(s, i) == 'p') {
         j = 1;
     }
     assert(j == 1);
diff --git a/regression/strings/test4/test.desc b/regression/strings/test4/test.desc
index 0f5bd6ccca7..c88a62b6704 100644
--- a/regression/strings/test4/test.desc
+++ b/regression/strings/test4/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test5/test.desc b/regression/strings/test5/test.desc
index dbf3c40cfdb..d88e1c83744 100644
--- a/regression/strings/test5/test.desc
+++ b/regression/strings/test5/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/test_char_set/test.desc b/regression/strings/test_char_set/test.desc
index 8cf42dda8f3..589767e4b82 100644
--- a/regression/strings/test_char_set/test.desc
+++ b/regression/strings/test_char_set/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("apc")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("abc")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("apc")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("abc")): FAILURE$
 --
diff --git a/regression/strings/test_concat/test.c b/regression/strings/test_concat/test.c
index 007b9ca1b5c..923bffb46ae 100644
--- a/regression/strings/test_concat/test.c
+++ b/regression/strings/test_concat/test.c
@@ -10,7 +10,7 @@ int main()
   u =  __CPROVER_string_concat(s, t);
   __CPROVER_char c = __CPROVER_char_at(u,i);
 
-  assert(c  == __CPROVER_char_literal("p"));
-  assert(__CPROVER_char_at(u,2)  == __CPROVER_char_literal("p"));
+  assert(c  == 'p');
+  assert(__CPROVER_char_at(u,2)  == 'p');
   return 0;
 }
diff --git a/regression/strings/test_concat/test.desc b/regression/strings/test_concat/test.desc
index e5d8b30d6da..c3f1ca2a65a 100644
--- a/regression/strings/test_concat/test.desc
+++ b/regression/strings/test_concat/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion c == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_char_at_func(u, 2) == __CPROVER_uninterpreted_char_literal_func(\"p\"): FAILURE$
+^\[main.assertion.1\] assertion c == .p.: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_char_at(u,2) == .p.: FAILURE$
 --
diff --git a/regression/strings/test_contains/test.desc b/regression/strings/test_contains/test.desc
index 8275425c548..fcf9694b31d 100644
--- a/regression/strings/test_contains/test.desc
+++ b/regression/strings/test_contains/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"3\")): SUCCESS$
diff --git a/regression/strings/test_equal/test.desc b/regression/strings/test_equal/test.desc
index 81ad6913856..d3cfd4f3747 100644
--- a/regression/strings/test_equal/test.desc
+++ b/regression/strings/test_equal/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(s, __CPROVER_uninterpreted_string_literal_func(\"pippo\")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(s, __CPROVER_uninterpreted_string_literal_func(\"mippo\")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("pippo")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("mippo")): FAILURE$
 --
diff --git a/regression/strings/test_index_of/test.c b/regression/strings/test_index_of/test.c
index d64d3c2d66e..c182e7952ab 100644
--- a/regression/strings/test_index_of/test.c
+++ b/regression/strings/test_index_of/test.c
@@ -7,7 +7,7 @@ int main(){
   __CPROVER_string str;
   int firstSlash = __CPROVER_string_index_of(str,'/');
   //__CPROVER_char_literal("/"));
-  int lastSlash = __CPROVER_string_last_index_of(str,__CPROVER_char_literal("/"));
+  int lastSlash = __CPROVER_string_last_index_of(str,'/');
 
   __CPROVER_assume(__CPROVER_string_equal(str, __CPROVER_string_literal("abc/abc/abc")));
 
diff --git a/regression/strings/test_index_of/test.desc b/regression/strings/test_index_of/test.desc
index 6d9ddbc6281..edc8e09c4ed 100644
--- a/regression/strings/test_index_of/test.desc
+++ b/regression/strings/test_index_of/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion firstSlash == 3: SUCCESS$
diff --git a/regression/strings/test_int/test.c b/regression/strings/test_int/test.c
index 3f8f8651783..28aa9c7e156 100644
--- a/regression/strings/test_int/test.c
+++ b/regression/strings/test_int/test.c
@@ -5,12 +5,12 @@
 int main()
 {
   __CPROVER_string s;
-  unsigned i = 10;
+  int i = 10;
   s = __CPROVER_string_of_int(123);
   assert(__CPROVER_char_at(s,0)  == '1');
   assert(__CPROVER_char_at(s,1)  == '2');
 
-  unsigned j = __CPROVER_parse_int(__CPROVER_string_literal("234"));
+  int j = __CPROVER_parse_int(__CPROVER_string_literal("234"));
 
   assert(j == 234);
   assert(j < 233 || __CPROVER_char_at(s,2)  == '4');
diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc
index e46e43ed936..a13b3dad852 100644
--- a/regression/strings/test_int/test.desc
+++ b/regression/strings/test_int/test.desc
@@ -1,10 +1,10 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_char_at_func(s, 0) == .1.: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_char_at_func(s, 1) == .2.: SUCCESS$
+^\[main.assertion.1\] assertion __CPROVER_char_at(s,0) == .1.: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_char_at(s,1) == .2.: SUCCESS$
 ^\[main.assertion.3\] assertion j == 234: SUCCESS$
-^\[main.assertion.4\] assertion j < 233 || __CPROVER_uninterpreted_string_char_at_func(s, 2) == .4.: FAILURE$
+^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at(s,2) == .4.: FAILURE$
 --
diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc
index 7548b6e91ef..4e7cd79fde4 100644
--- a/regression/strings/test_pass1/test.desc
+++ b/regression/strings/test_pass1/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): SUCCESS
diff --git a/regression/strings/test_pass_pc3/test.desc b/regression/strings/test_pass_pc3/test.desc
index 88f4659c45d..0e64d9b84d1 100644
--- a/regression/strings/test_pass_pc3/test.desc
+++ b/regression/strings/test_pass_pc3/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s3) == 0: FAILURE$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_length_func(s3) < 2: SUCCESS$
+^\[main.assertion.1\] assertion __CPROVER_string_length(s3) == 0: FAILURE$
+^\[main.assertion.2\] assertion __CPROVER_string_length(s3) < 2: SUCCESS$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/test_prefix/test.desc b/regression/strings/test_prefix/test.desc
index 187565433e4..6c62a2fa466 100644
--- a/regression/strings/test_prefix/test.desc
+++ b/regression/strings/test_prefix/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion b: SUCCESS$
diff --git a/regression/strings/test_strlen/test.desc b/regression/strings/test_strlen/test.desc
index a35e2499c9f..30c3f4066ed 100644
--- a/regression/strings/test_strlen/test.desc
+++ b/regression/strings/test_strlen/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion len_s == len_t: SUCCESS$
diff --git a/regression/strings/test_substring/test.desc b/regression/strings/test_substring/test.desc
index 327d5bbe1f2..6e2609d9cd3 100644
--- a/regression/strings/test_substring/test.desc
+++ b/regression/strings/test_substring/test.desc
@@ -1,10 +1,10 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cd\")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cc\")): FAILURE$
-^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"bc\")): SUCCESS$
-^\[main.assertion.4\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cd\")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cd")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cc")): FAILURE$
+^\[main.assertion.3\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("bc")): SUCCESS$
+^\[main.assertion.4\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("cd")): FAILURE$
 --
diff --git a/regression/strings/test_suffix/test.desc b/regression/strings/test_suffix/test.desc
index e0e8af7704c..a6667cfbfcf 100644
--- a/regression/strings/test_suffix/test.desc
+++ b/regression/strings/test_suffix/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"pp\"), s): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("po"),s): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("pp"),s): FAILURE$
 --