diff --git a/regression/strings/Makefile b/regression/strings/Makefile
new file mode 100644
index 00000000000..545b36925ac
--- /dev/null
+++ b/regression/strings/Makefile
@@ -0,0 +1,3 @@
+
+test:
+	../test.pl -c ../../../src/cbmc/cbmc
diff --git a/regression/strings/cprover-string-hack.h b/regression/strings/cprover-string-hack.h
new file mode 100644
index 00000000000..8a560e9d70d
--- /dev/null
+++ b/regression/strings/cprover-string-hack.h
@@ -0,0 +1,73 @@
+typedef struct __CPROVER_string { char *s; } __CPROVER_string;
+//typedef struct __CPROVER_char { char c; } __CPROVER_char;
+typedef unsigned char __CPROVER_char;
+
+/******************************************************************************
+ * CPROVER string functions
+ ******************************************************************************/
+/* returns s[p] */
+#define __CPROVER_char_at(s, p) __CPROVER_uninterpreted_string_char_at_func(s, p)
+
+/* string equality */
+#define __CPROVER_string_equal(s1, s2) __CPROVER_uninterpreted_string_equal_func(s1, s2)
+
+/* defines a string literal, e.g. __CPROVER_string_literal("foo") */
+#define __CPROVER_string_literal(s) __CPROVER_uninterpreted_string_literal_func(s)
+
+/* defines a char literal, e.g. __CPROVER_char_literal("c"). NOTE: you
+ * *must* use a C string literal as argument (i.e. double quotes "c", not
+ * single 'c') */
+#define __CPROVER_char_literal(c) __CPROVER_uninterpreted_char_literal_func(c)
+
+/* produces the concatenation of s1 and s2 */
+#define __CPROVER_string_concat(s1, s2) __CPROVER_uninterpreted_string_concat_func(s1, s2)
+
+/* return the length of s */
+#define __CPROVER_string_length(s) __CPROVER_uninterpreted_string_length_func(s)
+
+/* extracts the substring between positions i and j (j not included) */
+#define __CPROVER_string_substring(s, i, j) __CPROVER_uninterpreted_string_substring_func(s, i, j)
+
+/* test whether p is a prefix of s */
+#define __CPROVER_string_isprefix(p, s) __CPROVER_uninterpreted_string_is_prefix_func(p, s)
+
+/* test whether p is a suffix of s */
+#define __CPROVER_string_issuffix(p, s) __CPROVER_uninterpreted_string_is_suffix_func(p, s)
+/* test whether p contains s */
+#define __CPROVER_string_contains(p, s) __CPROVER_uninterpreted_string_contains_func(p, s)
+
+/* first index where character c appears, -1 if not found */
+#define __CPROVER_string_index_of(s, c) __CPROVER_uninterpreted_string_index_of_func(s, c)
+
+/* last index where character c appears */
+#define __CPROVER_string_last_index_of(s, c) __CPROVER_uninterpreted_string_last_index_of_func(s, c)
+
+/* returns a new string obtained from s by setting s[p] = c */
+#define __CPROVER_char_set(s, p, c) __CPROVER_uninterpreted_string_char_set_func(s, p, c)
+
+
+#define __CPROVER_string_copy(s) __CPROVER_uninterpreted_string_copy_func(s)
+#define __CPROVER_parse_int(s) __CPROVER_uninterpreted_string_parse_int_func(s)
+#define __CPROVER_string_of_int(i) __CPROVER_uninterpreted_string_of_int_func(i)
+
+
+/******************************************************************************
+ * don't use these directly
+ ******************************************************************************/
+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_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);
+extern __CPROVER_string __CPROVER_uninterpreted_string_substring_func(__CPROVER_string str, int i, int j);
+extern __CPROVER_bool __CPROVER_uninterpreted_string_is_prefix_func(__CPROVER_string pref, __CPROVER_string str);
+extern __CPROVER_bool __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_string suff, __CPROVER_string str);
+extern __CPROVER_bool __CPROVER_uninterpreted_string_contains_func(__CPROVER_string str1, __CPROVER_string str2);
+extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __CPROVER_char c);
+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);
+
diff --git a/regression/strings/java_case/test.desc b/regression/strings/java_case/test.desc
new file mode 100644
index 00000000000..7397314cca8
--- /dev/null
+++ b/regression/strings/java_case/test.desc
@@ -0,0 +1,10 @@
+CORE
+test_case.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_case.java line 11: SUCCESS$
+^\[assertion.2\] assertion at file test_case.java line 12: SUCCESS$
+^\[assertion.3\] assertion at file test_case.java line 13: SUCCESS$
+^\[assertion.4\] assertion at file test_case.java line 14: FAILURE$
+--
\ No newline at end of file
diff --git a/regression/strings/java_case/test_case.class b/regression/strings/java_case/test_case.class
new file mode 100644
index 00000000000..8579881de17
Binary files /dev/null and b/regression/strings/java_case/test_case.class differ
diff --git a/regression/strings/java_case/test_case.java b/regression/strings/java_case/test_case.java
new file mode 100644
index 00000000000..ce3a51814c8
--- /dev/null
+++ b/regression/strings/java_case/test_case.java
@@ -0,0 +1,16 @@
+public class test_case {
+
+    public static void main(String[] argv) {
+
+	String s = new String("AbcCdE");
+	String l = s.toLowerCase();
+	System.out.println(l);
+	
+	String u = s.toUpperCase();
+	System.out.println(u);
+	assert(l.equals("abccde"));
+	assert(u.equals("ABCCDE"));
+	assert(s.equalsIgnoreCase("ABccDe"));
+	assert(!l.equals("abccde") || !u.equals("ABCCDE"));
+    }
+}
diff --git a/regression/strings/java_char_at/test.desc b/regression/strings/java_char_at/test.desc
new file mode 100644
index 00000000000..babcc395bcf
--- /dev/null
+++ b/regression/strings/java_char_at/test.desc
@@ -0,0 +1,9 @@
+CORE
+test_char_at.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_char_at.java line 11: SUCCESS$
+^\[assertion.2\] assertion at file test_char_at.java line 13: FAILURE$
+^\[assertion.3\] assertion at file test_char_at.java line 15: SUCCESS$
+--
diff --git a/regression/strings/java_char_at/test_char_at.class b/regression/strings/java_char_at/test_char_at.class
new file mode 100644
index 00000000000..7d1f07fad7d
Binary files /dev/null and b/regression/strings/java_char_at/test_char_at.class differ
diff --git a/regression/strings/java_char_at/test_char_at.java b/regression/strings/java_char_at/test_char_at.java
new file mode 100644
index 00000000000..337c6524099
--- /dev/null
+++ b/regression/strings/java_char_at/test_char_at.java
@@ -0,0 +1,17 @@
+public class test_char_at {
+
+    public static void main(String[] argv) {
+	String s = new String("Hello World!");
+	char c = s.charAt(4);
+	StringBuilder sb = new StringBuilder(s);
+	sb.setCharAt(5,'-');
+	s = sb.toString();
+
+	if(argv.length==1)
+	    assert(c == 'o');
+	else if(argv.length==2)
+	    assert(c == 'p');
+	else
+	    assert(s.equals("Hello-World!"));
+    }
+}
diff --git a/regression/strings/java_code_point/test.desc b/regression/strings/java_code_point/test.desc
new file mode 100644
index 00000000000..bb69366ce61
--- /dev/null
+++ b/regression/strings/java_code_point/test.desc
@@ -0,0 +1,11 @@
+CORE
+test_code_point.class
+--pass
+^EXIT=0$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_code_point.java line 5: SUCCESS$
+^\[assertion.2\] assertion at file test_code_point.java line 6: SUCCESS$
+^\[assertion.3\] assertion at file test_code_point.java line 7: SUCCESS$
+^\[assertion.4\] assertion at file test_code_point.java line 8: SUCCESS$
+^\[assertion.5\] assertion at file test_code_point.java line 11: SUCCESS$
+--
\ No newline at end of file
diff --git a/regression/strings/java_code_point/test_code_point.class b/regression/strings/java_code_point/test_code_point.class
new file mode 100644
index 00000000000..c257f0633ec
Binary files /dev/null and b/regression/strings/java_code_point/test_code_point.class differ
diff --git a/regression/strings/java_code_point/test_code_point.java b/regression/strings/java_code_point/test_code_point.java
new file mode 100644
index 00000000000..c27a56f575c
--- /dev/null
+++ b/regression/strings/java_code_point/test_code_point.java
@@ -0,0 +1,13 @@
+public class test_code_point {
+
+    public static void main(String[] argv) {
+	String s = "!𐤇𐤄𐤋𐤋𐤅"; 
+	assert(s.codePointAt(1) == 67847);
+	assert(s.codePointBefore(3) == 67847);
+	assert(s.codePointCount(1,5) >= 2);
+	assert(s.offsetByCodePoints(1,2) >= 3);
+	StringBuilder sb = new StringBuilder();
+	sb.appendCodePoint(0x10907);
+	assert(s.charAt(1) == sb.charAt(0));
+    }
+}
diff --git a/regression/strings/java_compare/test.desc b/regression/strings/java_compare/test.desc
new file mode 100644
index 00000000000..c500900a21e
--- /dev/null
+++ b/regression/strings/java_compare/test.desc
@@ -0,0 +1,10 @@
+CORE
+test_compare.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_compare.java line 6: SUCCESS$
+^\[assertion.2\] assertion at file test_compare.java line 8: FAILURE$
+^\[assertion.3\] assertion at file test_compare.java line 11: SUCCESS$
+^\[assertion.4\] assertion at file test_compare.java line 12: FAILURE$
+--
diff --git a/regression/strings/java_compare/test_compare.class b/regression/strings/java_compare/test_compare.class
new file mode 100644
index 00000000000..5616013c523
Binary files /dev/null and b/regression/strings/java_compare/test_compare.class differ
diff --git a/regression/strings/java_compare/test_compare.java b/regression/strings/java_compare/test_compare.java
new file mode 100644
index 00000000000..8c1d4b71a0c
--- /dev/null
+++ b/regression/strings/java_compare/test_compare.java
@@ -0,0 +1,18 @@
+public class test_compare {
+
+    public static void main(String[] argv) {
+	String s1 = "abc";
+	String s2 = "aac";
+	assert(s1.compareTo(s2) == 1);
+
+	assert(s2.compareTo(argv[0]) != -1);
+	
+	String s3 = "abc";
+	assert(s3.hashCode() == s1.hashCode());
+	assert(s3.hashCode() == s2.hashCode());
+			  
+	/*String x = s1.intern();
+	String y = s3.intern();
+	assert(x == y);*/
+    }
+}
diff --git a/regression/strings/java_concat/test.desc b/regression/strings/java_concat/test.desc
new file mode 100644
index 00000000000..c6c0b193e5b
--- /dev/null
+++ b/regression/strings/java_concat/test.desc
@@ -0,0 +1,8 @@
+CORE
+test_concat.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_concat.java line 9: SUCCESS$
+^\[assertion.2\] assertion at file test_concat.java line 10: FAILURE$
+--
diff --git a/regression/strings/java_concat/test_concat.class b/regression/strings/java_concat/test_concat.class
new file mode 100644
index 00000000000..a6d4008aa26
Binary files /dev/null and b/regression/strings/java_concat/test_concat.class differ
diff --git a/regression/strings/java_concat/test_concat.java b/regression/strings/java_concat/test_concat.java
new file mode 100644
index 00000000000..d714ea89538
--- /dev/null
+++ b/regression/strings/java_concat/test_concat.java
@@ -0,0 +1,12 @@
+public class test_concat {
+
+    public static void main(String[] argv) {
+	String s = new String("pi");
+	int i = s.length();
+	String t = new String("ppo");
+	String u = s.concat(t);
+	char c = u.charAt(i);
+	assert(c == 'p');
+	assert(c == 'o');
+    }
+}
diff --git a/regression/strings/java_contains/test.desc b/regression/strings/java_contains/test.desc
new file mode 100644
index 00000000000..ade6b433bf1
--- /dev/null
+++ b/regression/strings/java_contains/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+test_contains.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_contains.java line 7: SUCCESS$
+^\[assertion.2\] assertion at file test_contains.java line 8: FAILURE$
+--
diff --git a/regression/strings/java_contains/test_contains.class b/regression/strings/java_contains/test_contains.class
new file mode 100644
index 00000000000..855ab828393
Binary files /dev/null and b/regression/strings/java_contains/test_contains.class differ
diff --git a/regression/strings/java_contains/test_contains.java b/regression/strings/java_contains/test_contains.java
new file mode 100644
index 00000000000..fce2ee63047
--- /dev/null
+++ b/regression/strings/java_contains/test_contains.java
@@ -0,0 +1,10 @@
+public class test_contains {
+
+    public static void main(String[] argv) {
+	String s = new String("Hello World!");
+	String u = "o W";
+	String t = "W o";
+	assert(s.contains(u));	
+	assert(s.contains(t));
+    }
+}
diff --git a/regression/strings/java_delete/test.desc b/regression/strings/java_delete/test.desc
new file mode 100644
index 00000000000..377ada44770
--- /dev/null
+++ b/regression/strings/java_delete/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+test_delete.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_delete.java line 11: SUCCESS$
+^\[assertion.2\] assertion at file test_delete.java line 12: FAILURE$
+--
diff --git a/regression/strings/java_delete/test_delete.class b/regression/strings/java_delete/test_delete.class
new file mode 100644
index 00000000000..6d30024f108
Binary files /dev/null and b/regression/strings/java_delete/test_delete.class differ
diff --git a/regression/strings/java_delete/test_delete.java b/regression/strings/java_delete/test_delete.java
new file mode 100644
index 00000000000..c91b16c5b89
--- /dev/null
+++ b/regression/strings/java_delete/test_delete.java
@@ -0,0 +1,15 @@
+public class test_delete {
+
+    public static void main(String[] argv) {
+	StringBuilder s = new StringBuilder();
+	s.append("Hello World!");
+	s.delete(4,6);
+	s.deleteCharAt(1);
+
+	String str = s.toString();
+	System.out.println(str);
+	assert(str.equals("HllWorld!"));
+	assert(!str.equals("HllWorld!"));
+
+    }
+}
diff --git a/regression/strings/java_easychair/easychair.class b/regression/strings/java_easychair/easychair.class
new file mode 100644
index 00000000000..e47900cc0b2
Binary files /dev/null and b/regression/strings/java_easychair/easychair.class differ
diff --git a/regression/strings/java_easychair/easychair.java b/regression/strings/java_easychair/easychair.java
new file mode 100644
index 00000000000..55ca2a31bb3
--- /dev/null
+++ b/regression/strings/java_easychair/easychair.java
@@ -0,0 +1,34 @@
+public class easychair {
+
+    public static void main(String[] argv) {
+	if(argv.length > 1){
+	    String str = new String(argv[1]);
+	    if(str.length() < 40){
+
+		// containing "/" and containing "EasyChair"
+		int lastSlash = str.lastIndexOf('/');
+		if(lastSlash < 0) return ;
+		
+		String rest = str.substring(lastSlash + 1);
+		// warning: removed this because contains is not efficient at the moment
+		if(! rest.contains("EasyChair")) return ;
+		// (2) Check that str starts with "http://"
+		if(! str.startsWith("http://")) return ;
+		// (3) Take the string between "http://" and the last "/".
+		// if it starts with "www." strip the "www." off
+		String t = str.substring("http://".length(),lastSlash - "http://".length());
+		if(t.startsWith("www."))
+		    t = t.substring("www.".length());
+		
+		//
+		//(4) Check that after stripping we have either "live.com"
+		// or "google.com"
+		if(!t.equals("live.com") && !t.equals("google.com"))
+		    return ;
+		// s survived all checks
+		assert(false); //return true;
+	    }
+	}
+    }
+
+}
diff --git a/regression/strings/java_easychair/test.desc b/regression/strings/java_easychair/test.desc
new file mode 100644
index 00000000000..bd68fd1f60a
--- /dev/null
+++ b/regression/strings/java_easychair/test.desc
@@ -0,0 +1,7 @@
+KNOWNBUG
+easychair.class
+--pass
+^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
new file mode 100644
index 00000000000..56b21e2041c
--- /dev/null
+++ b/regression/strings/java_empty/test.desc
@@ -0,0 +1,8 @@
+CORE
+test_empty.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_empty.java line 4: SUCCESS$
+^\[assertion.2\] assertion at file test_empty.java line 5: FAILURE$
+--
diff --git a/regression/strings/java_empty/test_empty.class b/regression/strings/java_empty/test_empty.class
new file mode 100644
index 00000000000..f0ced290ee3
Binary files /dev/null and b/regression/strings/java_empty/test_empty.class differ
diff --git a/regression/strings/java_empty/test_empty.java b/regression/strings/java_empty/test_empty.java
new file mode 100644
index 00000000000..2465fb16e41
--- /dev/null
+++ b/regression/strings/java_empty/test_empty.java
@@ -0,0 +1,7 @@
+public class test_empty {
+    public static void main(String[] argv) {
+	String empty = "   ";
+	assert(empty.trim().isEmpty());
+	assert(empty.isEmpty());
+    }
+}
diff --git a/regression/strings/java_equal/test.desc b/regression/strings/java_equal/test.desc
new file mode 100644
index 00000000000..6375cfdc3d8
--- /dev/null
+++ b/regression/strings/java_equal/test.desc
@@ -0,0 +1,8 @@
+CORE
+test_equal.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_equal.java line 7: FAILURE$
+^\[assertion.2\] assertion at file test_equal.java line 8: SUCCESS$
+--
diff --git a/regression/strings/java_equal/test_equal.class b/regression/strings/java_equal/test_equal.class
new file mode 100644
index 00000000000..26ee19e6cb1
Binary files /dev/null and b/regression/strings/java_equal/test_equal.class differ
diff --git a/regression/strings/java_equal/test_equal.java b/regression/strings/java_equal/test_equal.java
new file mode 100644
index 00000000000..151162a106d
--- /dev/null
+++ b/regression/strings/java_equal/test_equal.java
@@ -0,0 +1,10 @@
+public class test_equal {
+
+    public static void main(String[] argv) {
+	String s = new String("pi");
+	String t = new String("po");
+	String u = "po";
+	assert(s.equals(t));
+	assert(t.equals(u));
+    }
+}
diff --git a/regression/strings/java_float/test.desc b/regression/strings/java_float/test.desc
new file mode 100644
index 00000000000..47e915cda98
--- /dev/null
+++ b/regression/strings/java_float/test.desc
@@ -0,0 +1,10 @@
+CORE
+test_float.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_float.java line 14: SUCCESS$
+^\[assertion.2\] assertion at file test_float.java line 15: SUCCESS$
+^\[assertion.3\] assertion at file test_float.java line 16: SUCCESS$
+^\[assertion.4\] assertion at file test_float.java line 17: FAILURE$
+--
\ No newline at end of file
diff --git a/regression/strings/java_float/test_float.class b/regression/strings/java_float/test_float.class
new file mode 100644
index 00000000000..356d0e17871
Binary files /dev/null and b/regression/strings/java_float/test_float.class differ
diff --git a/regression/strings/java_float/test_float.java b/regression/strings/java_float/test_float.java
new file mode 100644
index 00000000000..e59c631d91e
--- /dev/null
+++ b/regression/strings/java_float/test_float.java
@@ -0,0 +1,20 @@
+public class test_float {
+
+    public static void main(String[] arg) {
+	float inf = 100.0f / 0.0f;
+	float minus_inf = -100.0f / 0.0f;
+	float nan = 0.0f / 0.0f;
+	String inf_string = Float.toString(inf);
+	String mininf_string = Float.toString(minus_inf);
+	String nan_string = Float.toString(nan);
+	//String arg1 = arg[0];
+	System.out.println(nan_string);
+	System.out.println(inf_string);
+	System.out.println(mininf_string);
+	assert(nan_string.equals("NaN"));
+	assert(inf_string.equals("Infinity"));
+	assert(mininf_string.equals("-Infinity"));
+	assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity")
+	       || !mininf_string.equals("-Infinity"));
+    }
+}
diff --git a/regression/strings/java_index_of/test.desc b/regression/strings/java_index_of/test.desc
new file mode 100644
index 00000000000..dd5c60464d5
--- /dev/null
+++ b/regression/strings/java_index_of/test.desc
@@ -0,0 +1,16 @@
+CORE
+test_index_of.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_index_of.java line 13: SUCCESS$
+^\[assertion.2\] assertion at file test_index_of.java line 14: FAILURE$
+^\[assertion.3\] assertion at file test_index_of.java line 17: SUCCESS$
+^\[assertion.4\] assertion at file test_index_of.java line 18: FAILURE$
+^\[assertion.5\] assertion at file test_index_of.java line 21: SUCCESS$
+^\[assertion.6\] assertion at file test_index_of.java line 22: FAILURE$
+^\[assertion.7\] assertion at file test_index_of.java line 25: SUCCESS$
+^\[assertion.8\] assertion at file test_index_of.java line 26: FAILURE$
+^\[assertion.9\] assertion at file test_index_of.java line 28: SUCCESS$
+^\[assertion.10\] assertion at file test_index_of.java line 29: SUCCESS$
+--
diff --git a/regression/strings/java_index_of/test_index_of.class b/regression/strings/java_index_of/test_index_of.class
new file mode 100644
index 00000000000..8b3b7525f1a
Binary files /dev/null and b/regression/strings/java_index_of/test_index_of.class differ
diff --git a/regression/strings/java_index_of/test_index_of.java b/regression/strings/java_index_of/test_index_of.java
new file mode 100644
index 00000000000..bbe06d279ec
--- /dev/null
+++ b/regression/strings/java_index_of/test_index_of.java
@@ -0,0 +1,32 @@
+public class test_index_of {
+
+    public static void main(String[] argv) {
+	String s = "Hello World!"; 
+	char c = 'o';
+	int i = s.indexOf(c);
+	int j = s.lastIndexOf('o');
+	int k = s.indexOf(c,5);
+	int l = s.lastIndexOf(c,5);
+	int m = s.indexOf("lo");
+	int n = s.lastIndexOf("lo");
+	if(argv.length == 1){
+	    assert(i == 4);
+	    assert(i != 4);
+	}
+	else if(argv.length == 2){
+	    assert(j == 7);	
+	    assert(j != 7);
+	}
+	else if(argv.length == 3){
+	    assert(k == 7);
+	    assert(k != 7);
+	}
+	else if(argv.length == 4){
+	    assert(l == 4);
+	    assert(l != 4);
+	} else {
+	    assert(m != 2);
+	    assert(n != 2);
+	}
+    }
+}
diff --git a/regression/strings/java_insert/test_insert.class b/regression/strings/java_insert/test_insert.class
new file mode 100644
index 00000000000..5fa0f425061
Binary files /dev/null and b/regression/strings/java_insert/test_insert.class differ
diff --git a/regression/strings/java_insert/test_insert.java b/regression/strings/java_insert/test_insert.java
new file mode 100644
index 00000000000..6871a51716c
--- /dev/null
+++ b/regression/strings/java_insert/test_insert.java
@@ -0,0 +1,19 @@
+public class test_insert {
+
+    public static void main(String[] argv) {
+	int i = 123;
+	long j = 123;
+	char c = '/';
+	boolean b = true;
+	StringBuilder sb = new StringBuilder("hello");
+	sb.insert(2,i);
+	sb.insert(2,c);
+	sb.insert(2,j);
+	sb.insert(2,b);
+	sb.insert(2,"abc");
+	String s = sb.toString();
+	System.out.println(s);
+	assert(s.equals("heabctrue123/123llo"));
+	assert(!s.equals("heabctrue123/123llo"));
+    }
+}
diff --git a/regression/strings/java_insert/test_insert1.class b/regression/strings/java_insert/test_insert1.class
new file mode 100644
index 00000000000..80091936cea
Binary files /dev/null and b/regression/strings/java_insert/test_insert1.class differ
diff --git a/regression/strings/java_insert/test_insert1.java b/regression/strings/java_insert/test_insert1.java
new file mode 100644
index 00000000000..54e754302c5
--- /dev/null
+++ b/regression/strings/java_insert/test_insert1.java
@@ -0,0 +1,23 @@
+public class test_insert1 {
+
+    public static void main(String[] argv) {
+	int i = 123;
+	long j = 123;
+	char c = '/';
+	boolean b = true;
+	StringBuilder sb = new StringBuilder("hello");
+	sb.insert(2,i);
+
+	/*
+	sb.insert(2,c);
+	sb.insert(2,j);
+	sb.insert(2,b);
+	sb.insert(2,"abc");
+	*/
+	String s = sb.toString();
+	System.out.println(s);
+	assert(s.equals("he123llo"));
+	//assert(s.equals("heabctrue123/123llo"));
+	//assert(!s.equals("heabctrue123/123llo"));
+    }
+}
diff --git a/regression/strings/java_int/test.desc b/regression/strings/java_int/test.desc
new file mode 100644
index 00000000000..5211656c61b
--- /dev/null
+++ b/regression/strings/java_int/test.desc
@@ -0,0 +1,13 @@
+CORE
+test_int.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_int.java line 8: SUCCESS$
+^\[assertion.2\] assertion at file test_int.java line 9: SUCCESS$
+^\[assertion.3\] assertion at file test_int.java line 12: SUCCESS$
+^\[assertion.4\] assertion at file test_int.java line 15: SUCCESS$
+^\[assertion.5\] assertion at file test_int.java line 18: SUCCESS$
+^\[assertion.6\] assertion at file test_int.java line 21: SUCCESS$
+^\[assertion.7\] assertion at file test_int.java line 23: FAILURE$
+--
diff --git a/regression/strings/java_int/test_int.class b/regression/strings/java_int/test_int.class
new file mode 100644
index 00000000000..643d7eca09c
Binary files /dev/null and b/regression/strings/java_int/test_int.class differ
diff --git a/regression/strings/java_int/test_int.java b/regression/strings/java_int/test_int.java
new file mode 100644
index 00000000000..620ae638dce
--- /dev/null
+++ b/regression/strings/java_int/test_int.java
@@ -0,0 +1,25 @@
+public class test_int {
+
+    public static void main(String[] argv) {
+	String s = Integer.toString(2345);
+	char c = s.charAt(1);
+	char d = s.charAt(2);
+	char e = s.charAt(3);
+	assert(c == '3');
+	assert(d == '4');
+
+	int i = Integer.parseInt("1234");
+	assert(i == 1234);
+
+	String t = Integer.toString(-2345);
+	assert(t.charAt(0) == '-');
+	
+	int j = Integer.parseInt("-4231");
+	assert(j == -4231);
+
+	String u = Integer.toHexString(43981);
+	assert(u.equals("abcd"));
+
+	assert(e == '2' || i < 1234 || t.charAt(0) != '-' || j != -4231 || !u.equals("abcd"));
+    }
+}
diff --git a/regression/strings/java_prefix/test.desc b/regression/strings/java_prefix/test.desc
new file mode 100644
index 00000000000..b234bba1788
--- /dev/null
+++ b/regression/strings/java_prefix/test.desc
@@ -0,0 +1,10 @@
+CORE
+test_prefix.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_prefix.java line 14: SUCCESS$
+^\[assertion.2\] assertion at file test_prefix.java line 16: FAILURE$
+^\[assertion.3\] assertion at file test_prefix.java line 18: SUCCESS$
+^\[assertion.4\] assertion at file test_prefix.java line 20: FAILURE$
+--
diff --git a/regression/strings/java_prefix/test_prefix.class b/regression/strings/java_prefix/test_prefix.class
new file mode 100644
index 00000000000..6f5f4025932
Binary files /dev/null and b/regression/strings/java_prefix/test_prefix.class differ
diff --git a/regression/strings/java_prefix/test_prefix.java b/regression/strings/java_prefix/test_prefix.java
new file mode 100644
index 00000000000..c9b5fa72fcf
--- /dev/null
+++ b/regression/strings/java_prefix/test_prefix.java
@@ -0,0 +1,23 @@
+public class test_prefix {
+
+    public static void main(String[] argv) {
+	String s = new String("Hello World!");
+	//String t = new String("Hello");
+	//String u = new String("Wello");
+	String u = "Wello";
+	boolean b = s.startsWith("Hello");
+	//boolean c = s.startsWith("Wello");
+	//boolean b = s.startsWith(t);
+	boolean c = s.startsWith(u);
+	boolean d = s.startsWith("lo",3);
+	if(argv.length == 1){
+	    assert(b);	
+	} else if(argv.length == 2){
+	    assert(c);
+	} else if(argv.length == 3){
+	    assert(d);
+	} else if(argv.length == 4){	
+	    assert(!d);
+	}
+    }
+}
diff --git a/regression/strings/java_replace/test.desc b/regression/strings/java_replace/test.desc
new file mode 100644
index 00000000000..a5b15efd737
--- /dev/null
+++ b/regression/strings/java_replace/test.desc
@@ -0,0 +1,8 @@
+CORE
+test_replace.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_replace.java line 6: SUCCESS$
+^\[assertion.2\] assertion at file test_replace.java line 8: FAILURE$
+--
diff --git a/regression/strings/java_replace/test_replace.class b/regression/strings/java_replace/test_replace.class
new file mode 100644
index 00000000000..c795826dc15
Binary files /dev/null and b/regression/strings/java_replace/test_replace.class differ
diff --git a/regression/strings/java_replace/test_replace.java b/regression/strings/java_replace/test_replace.java
new file mode 100644
index 00000000000..342bf9afddc
--- /dev/null
+++ b/regression/strings/java_replace/test_replace.java
@@ -0,0 +1,10 @@
+public class test_replace {
+
+    public static void main(String[] argv) {
+	String s = new String("Hello World!");
+	String t = s.replace('o','u');
+	assert(t.equals("Hellu Wurld!"));
+	System.out.println(t);
+	assert(!t.equals("Hellu Wurld!"));
+    }
+}
diff --git a/regression/strings/java_set_length/test.desc b/regression/strings/java_set_length/test.desc
new file mode 100644
index 00000000000..59204c9c5a8
--- /dev/null
+++ b/regression/strings/java_set_length/test.desc
@@ -0,0 +1,9 @@
+CORE
+test_set_length.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_set_length.java line 8: SUCCESS$
+^\[assertion.2\] assertion at file test_set_length.java line 9: SUCCESS$
+^\[assertion.3\] assertion at file test_set_length.java line 10: FAILURE$
+--
\ No newline at end of file
diff --git a/regression/strings/java_set_length/test_set_length.class b/regression/strings/java_set_length/test_set_length.class
new file mode 100644
index 00000000000..8836640967a
Binary files /dev/null and b/regression/strings/java_set_length/test_set_length.class differ
diff --git a/regression/strings/java_set_length/test_set_length.java b/regression/strings/java_set_length/test_set_length.java
new file mode 100644
index 00000000000..97b20f2332d
--- /dev/null
+++ b/regression/strings/java_set_length/test_set_length.java
@@ -0,0 +1,12 @@
+public class test_set_length {
+
+    public static void main(String[] argv) {
+
+	StringBuilder s = new StringBuilder("abc");
+	s.setLength(10);
+	String t = s.toString();
+	assert(t.startsWith("abc"));
+	assert(t.length() == 10);
+	assert(t.length() == 3);
+    }
+}
diff --git a/regression/strings/java_string_builder/test.desc b/regression/strings/java_string_builder/test.desc
new file mode 100644
index 00000000000..c0b3b6a51ce
--- /dev/null
+++ b/regression/strings/java_string_builder/test.desc
@@ -0,0 +1,9 @@
+CORE
+test_string_builder.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_string_builder.java line 11: SUCCESS$
+^\[assertion.2\] assertion at file test_string_builder.java line 12: SUCCESS$
+^\[assertion.3\] assertion at file test_string_builder.java line 13: FAILURE$
+--
diff --git a/regression/strings/java_string_builder/test_string_builder.class b/regression/strings/java_string_builder/test_string_builder.class
new file mode 100644
index 00000000000..7a61d1f02be
Binary files /dev/null and b/regression/strings/java_string_builder/test_string_builder.class differ
diff --git a/regression/strings/java_string_builder/test_string_builder.java b/regression/strings/java_string_builder/test_string_builder.java
new file mode 100644
index 00000000000..1d76b34e9f8
--- /dev/null
+++ b/regression/strings/java_string_builder/test_string_builder.java
@@ -0,0 +1,16 @@
+public class test_string_builder {
+    public static void main(String[] argv) {
+	if(argv.length > 2) {
+	    StringBuilder tmp = new StringBuilder(); 
+	    tmp.append("prefix ");
+	    tmp.append(argv[1]);
+	    tmp.append(" middle ").append(argv[2]).append(" end");
+	    //StringBuilder tmp1 = tmp.append(argv[2]);
+	    //tmp1.append(" end");
+	    String r = tmp.toString();
+	    assert(r.startsWith("pref"));	    
+	    assert(r.endsWith("end"));
+	    assert(r.startsWith("pr3f"));
+	}
+    }
+}
diff --git a/regression/strings/java_string_builder_length/test.desc b/regression/strings/java_string_builder_length/test.desc
new file mode 100644
index 00000000000..a15660ee85b
--- /dev/null
+++ b/regression/strings/java_string_builder_length/test.desc
@@ -0,0 +1,8 @@
+CORE
+test_sb_length.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+\[assertion.1\] assertion at file test_sb_length.java line 6: SUCCESS$
+\[assertion.2\] assertion at file test_sb_length.java line 8: FAILURE$
+--
diff --git a/regression/strings/java_string_builder_length/test_sb_length.class b/regression/strings/java_string_builder_length/test_sb_length.class
new file mode 100644
index 00000000000..586e8f71935
Binary files /dev/null and b/regression/strings/java_string_builder_length/test_sb_length.class differ
diff --git a/regression/strings/java_string_builder_length/test_sb_length.java b/regression/strings/java_string_builder_length/test_sb_length.java
new file mode 100644
index 00000000000..652b72cdc90
--- /dev/null
+++ b/regression/strings/java_string_builder_length/test_sb_length.java
@@ -0,0 +1,11 @@
+public class test_sb_length {
+    public static void main(String[] argv) {
+	StringBuilder tmp = new StringBuilder("prefix"); 
+	//tmp.append("prefix");
+	tmp.append("end");
+	assert(tmp.length() == 9);	    
+	if(argv.length > 1) {
+	    assert(tmp.length() == 12);	    
+	}
+    }
+}
diff --git a/regression/strings/java_strlen/test.desc b/regression/strings/java_strlen/test.desc
new file mode 100644
index 00000000000..78007186493
--- /dev/null
+++ b/regression/strings/java_strlen/test.desc
@@ -0,0 +1,8 @@
+CORE
+test_length.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_length.java line 10: SUCCESS$
+^\[assertion.2\] assertion at file test_length.java line 11: FAILURE$
+--
diff --git a/regression/strings/java_strlen/test_length.class b/regression/strings/java_strlen/test_length.class
new file mode 100644
index 00000000000..7f1c10c02ca
Binary files /dev/null and b/regression/strings/java_strlen/test_length.class differ
diff --git a/regression/strings/java_strlen/test_length.java b/regression/strings/java_strlen/test_length.java
new file mode 100644
index 00000000000..9410315db38
--- /dev/null
+++ b/regression/strings/java_strlen/test_length.java
@@ -0,0 +1,14 @@
+public class test_length {
+
+    public static void main(String[] argv) {
+	String s = new String("hello");
+	if(argv.length > 1) {
+	    String t = argv[1];
+	    int i = t.length();
+	    String u = t.concat(s);
+	    char c = u.charAt(i);
+	    assert(c == 'h');
+	    assert(c == 'o');
+	}
+    }
+}
diff --git a/regression/strings/java_substring/test.desc b/regression/strings/java_substring/test.desc
new file mode 100644
index 00000000000..78a9bcca9cb
--- /dev/null
+++ b/regression/strings/java_substring/test.desc
@@ -0,0 +1,10 @@
+CORE
+test_substring.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_substring.java line 12: SUCCESS$
+^\[assertion.2\] assertion at file test_substring.java line 13: FAILURE$
+^\[assertion.3\] assertion at file test_substring.java line 20: SUCCESS$
+^\[assertion.4\] assertion at file test_substring.java line 21: FAILURE$
+--
diff --git a/regression/strings/java_substring/test_substring.class b/regression/strings/java_substring/test_substring.class
new file mode 100644
index 00000000000..e6532aca43e
Binary files /dev/null and b/regression/strings/java_substring/test_substring.class differ
diff --git a/regression/strings/java_substring/test_substring.java b/regression/strings/java_substring/test_substring.java
new file mode 100644
index 00000000000..8a2ac883cca
--- /dev/null
+++ b/regression/strings/java_substring/test_substring.java
@@ -0,0 +1,27 @@
+public class test_substring {
+
+    public static void main(String[] argv) {
+	if(argv.length > 1) {
+	    String t = argv[1];
+
+	    if(t.length() == 6) {
+		String u = t.substring(2,4);
+		char c = u.charAt(1);
+		char d = t.charAt(3);
+		char e = t.charAt(4);
+		assert(c == d);
+		assert(c == e);
+	    }
+	    else if(t.length() == 5){
+		CharSequence u = t.subSequence(2,4);
+		char c = u.charAt(1);
+		char d = t.charAt(3);
+		char e = t.charAt(4);
+		assert(c == d);
+		assert(c == e);
+	    }
+		
+
+	}
+    }
+}
diff --git a/regression/strings/java_suffix/test.desc b/regression/strings/java_suffix/test.desc
new file mode 100644
index 00000000000..f9472f03b47
--- /dev/null
+++ b/regression/strings/java_suffix/test.desc
@@ -0,0 +1,8 @@
+CORE
+test_suffix.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_suffix.java line 12: SUCCESS$
+^\[assertion.2\] assertion at file test_suffix.java line 13: FAILURE$
+--
diff --git a/regression/strings/java_suffix/test_suffix.class b/regression/strings/java_suffix/test_suffix.class
new file mode 100644
index 00000000000..557acd02653
Binary files /dev/null and b/regression/strings/java_suffix/test_suffix.class differ
diff --git a/regression/strings/java_suffix/test_suffix.java b/regression/strings/java_suffix/test_suffix.java
new file mode 100644
index 00000000000..f61b0b8ba36
--- /dev/null
+++ b/regression/strings/java_suffix/test_suffix.java
@@ -0,0 +1,15 @@
+public class test_suffix {
+
+    public static void main(String[] argv) {
+	String s = new String("Hello World!");
+	//String t = new String("Hello");
+	//String u = new String("Wello");
+	String u = "Wello!";
+	boolean b = s.endsWith("World!");
+	//boolean c = s.startsWith("Wello");
+	//boolean b = s.startsWith(t);
+	boolean c = s.startsWith(u);
+	assert(b);	
+	assert(c);
+    }
+}
diff --git a/regression/strings/java_trim/test.desc b/regression/strings/java_trim/test.desc
new file mode 100644
index 00000000000..fa0e10a1ca7
--- /dev/null
+++ b/regression/strings/java_trim/test.desc
@@ -0,0 +1,8 @@
+CORE
+test_trim.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_trim.java line 5: SUCCESS$
+^\[assertion.2\] assertion at file test_trim.java line 6: FAILURE$
+--
diff --git a/regression/strings/java_trim/test_trim.class b/regression/strings/java_trim/test_trim.class
new file mode 100644
index 00000000000..8e6a923dcbc
Binary files /dev/null and b/regression/strings/java_trim/test_trim.class differ
diff --git a/regression/strings/java_trim/test_trim.java b/regression/strings/java_trim/test_trim.java
new file mode 100644
index 00000000000..8d8d41cb29a
--- /dev/null
+++ b/regression/strings/java_trim/test_trim.java
@@ -0,0 +1,8 @@
+public class test_trim {
+    public static void main(String[] argv) {
+	String t = "  a b c  ";
+	String x = t.trim();
+	assert(x.equals("a b c"));
+	assert(x.equals("abc "));
+    }
+}
diff --git a/regression/strings/test1/test.c b/regression/strings/test1/test.c
new file mode 100644
index 00000000000..d3830e38a3f
--- /dev/null
+++ b/regression/strings/test1/test.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+    __CPROVER_string s;
+    __CPROVER_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");
+    assert (c1 == c2);
+    assert (c1 != c2);
+    return 0;
+}
diff --git a/regression/strings/test1/test.desc b/regression/strings/test1/test.desc
new file mode 100644
index 00000000000..3483081c0f0
--- /dev/null
+++ b/regression/strings/test1/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.c
+--pass 
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] assertion c1 == c2: SUCCESS$
+^\[main.assertion.2\] assertion c1 != c2: FAILURE$
+--
diff --git a/regression/strings/test2/test.c b/regression/strings/test2/test.c
new file mode 100644
index 00000000000..aedc37ba3b3
--- /dev/null
+++ b/regression/strings/test2/test.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+int main()
+{
+    __CPROVER_string s;
+    int n;
+    s = __CPROVER_string_literal("pippo");
+    n = __CPROVER_string_length(s);
+    assert(n == 5);
+    assert(n != 5);
+    return 0;
+}
diff --git a/regression/strings/test2/test.desc b/regression/strings/test2/test.desc
new file mode 100644
index 00000000000..d3054f813f1
--- /dev/null
+++ b/regression/strings/test2/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.c
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] assertion n == 5: SUCCESS$
+^\[main.assertion.2\] assertion n != 5: FAILURE$
+--
diff --git a/regression/strings/test3.1/test.c b/regression/strings/test3.1/test.c
new file mode 100644
index 00000000000..e0d408322be
--- /dev/null
+++ b/regression/strings/test3.1/test.c
@@ -0,0 +1,20 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+    __CPROVER_string s, s2, s3;
+    int i;
+
+    s = __CPROVER_string_concat(s2, s3);
+    __CPROVER_assume(__CPROVER_string_length(s2) == i);
+    __CPROVER_assume(__CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
+
+    // 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"));
+
+    return 0;
+}
diff --git a/regression/strings/test3.1/test.desc b/regression/strings/test3.1/test.desc
new file mode 100644
index 00000000000..0f5bd6ccca7
--- /dev/null
+++ b/regression/strings/test3.1/test.desc
@@ -0,0 +1,7 @@
+CORE
+test.c
+--pass
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/strings/test3.2/test.c b/regression/strings/test3.2/test.c
new file mode 100644
index 00000000000..86d93224878
--- /dev/null
+++ b/regression/strings/test3.2/test.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+    __CPROVER_string s, s2, s3;
+    int i;
+
+    //__CPROVER_assume(i < 10);
+    //__CPROVER_assume(__CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
+    s3 = __CPROVER_string_literal("pippo");
+    s = __CPROVER_string_concat(s2, s3);
+    __CPROVER_assume(__CPROVER_string_length(s2) == i);
+
+    // 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"));
+
+    return 0;
+}
diff --git a/regression/strings/test3.2/test.desc b/regression/strings/test3.2/test.desc
new file mode 100644
index 00000000000..0f5bd6ccca7
--- /dev/null
+++ b/regression/strings/test3.2/test.desc
@@ -0,0 +1,7 @@
+CORE
+test.c
+--pass
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/strings/test3.3/test.c b/regression/strings/test3.3/test.c
new file mode 100644
index 00000000000..35e25d82ee5
--- /dev/null
+++ b/regression/strings/test3.3/test.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+    __CPROVER_string s, s2, s3;
+    int i;
+
+    s = __CPROVER_string_concat(s2, s3);
+    __CPROVER_assume(i < 10);
+    __CPROVER_assume(__CPROVER_string_length(s2) == i);
+    __CPROVER_assume(
+        __CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
+
+    // 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"));
+
+    return 0;
+}
diff --git a/regression/strings/test3.3/test.desc b/regression/strings/test3.3/test.desc
new file mode 100644
index 00000000000..0f5bd6ccca7
--- /dev/null
+++ b/regression/strings/test3.3/test.desc
@@ -0,0 +1,7 @@
+CORE
+test.c
+--pass
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/strings/test3.4/test.c b/regression/strings/test3.4/test.c
new file mode 100644
index 00000000000..70931d803d1
--- /dev/null
+++ b/regression/strings/test3.4/test.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+    __CPROVER_string s, s2, s3;
+    int i;
+
+    s = __CPROVER_string_concat(s2, s3);
+    __CPROVER_assume(__CPROVER_string_length(s2) == i);
+    __CPROVER_assume(
+        __CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
+
+    assert(__CPROVER_string_issuffix(__CPROVER_string_literal("p!o"), s));
+
+    return 0;
+}
diff --git a/regression/strings/test3.4/test.desc b/regression/strings/test3.4/test.desc
new file mode 100644
index 00000000000..dbf3c40cfdb
--- /dev/null
+++ b/regression/strings/test3.4/test.desc
@@ -0,0 +1,7 @@
+CORE
+test.c
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
diff --git a/regression/strings/test3/test-bv-to-int-onebyone.smt2 b/regression/strings/test3/test-bv-to-int-onebyone.smt2
new file mode 100644
index 00000000000..61e490a72bf
--- /dev/null
+++ b/regression/strings/test3/test-bv-to-int-onebyone.smt2
@@ -0,0 +1,37 @@
+(set-option :produce-models true)
+(set-logic ALL_SUPPORTED)
+
+(declare-fun s () String)
+(declare-fun s2 () String)
+(declare-fun s3 () String)
+
+(define-sort cprover.Pos () (_ BitVec 32))
+(define-fun cprover.ubv_to_int ((?x cprover.Pos)) Int (let ((bit0 (_ bv0 1)))
+ (+ (ite (= ((_ extract 0 0) ?x) bit0) 0 1) (ite (= ((_ extract 1 1) ?x) bit0) 0 2) (ite (= ((_ extract 2 2) ?x) bit0) 0 4) (ite (= ((_ extract 3 3) ?x) bit0) 0 8) (ite (= ((_ extract 4 4) ?x) bit0) 0 16) (ite (= ((_ extract 5 5) ?x) bit0) 0 32) (ite (= ((_ extract 6 6) ?x) bit0) 0 64) (ite (= ((_ extract 7 7) ?x) bit0) 0 128) (ite (= ((_ extract 8 8) ?x) bit0) 0 256) (ite (= ((_ extract 9 9) ?x) bit0) 0 512) (ite (= ((_ extract 10 10) ?x) bit0) 0 1024) (ite (= ((_ extract 11 11) ?x) bit0) 0 2048) (ite (= ((_ extract 12 12) ?x) bit0) 0 4096) (ite (= ((_ extract 13 13) ?x) bit0) 0 8192) (ite (= ((_ extract 14 14) ?x) bit0) 0 16384) (ite (= ((_ extract 15 15) ?x) bit0) 0 32768) (ite (= ((_ extract 16 16) ?x) bit0) 0 65536) (ite (= ((_ extract 17 17) ?x) bit0) 0 131072) (ite (= ((_ extract 18 18) ?x) bit0) 0 262144) (ite (= ((_ extract 19 19) ?x) bit0) 0 524288) (ite (= ((_ extract 20 20) ?x) bit0) 0 1048576) (ite (= ((_ extract 21 21) ?x) bit0) 0 2097152) (ite (= ((_ extract 22 22) ?x) bit0) 0 4194304) (ite (= ((_ extract 23 23) ?x) bit0) 0 8388608) (ite (= ((_ extract 24 24) ?x) bit0) 0 16777216) (ite (= ((_ extract 25 25) ?x) bit0) 0 33554432) (ite (= ((_ extract 26 26) ?x) bit0) 0 67108864) (ite (= ((_ extract 27 27) ?x) bit0) 0 134217728) (ite (= ((_ extract 28 28) ?x) bit0) 0 268435456) (ite (= ((_ extract 29 29) ?x) bit0) 0 536870912) (ite (= ((_ extract 30 30) ?x) bit0) 0 1073741824) (ite (= ((_ extract 31 31) ?x) bit0) 0 2147483648) 0)))
+
+(declare-fun bvi () cprover.Pos)
+(define-fun i () Int (cprover.ubv_to_int bvi))
+
+(assert (= s (str.++ s2 s3)))
+
+(assert (= (str.len s2) i))
+(assert (= s3 "pippo"))
+
+(define-fun p1 () Bool (= (str.len s) (+ i 5)))
+(define-fun p2 () Bool (str.suffixof "po" s))
+(define-fun p3 () Bool (= (str.at s i) "p"))
+
+(push 1)
+(assert (not p1))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (not p2))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (not p3))
+(check-sat)
+(pop 1)
diff --git a/regression/strings/test3/test-bv-to-int.smt2 b/regression/strings/test3/test-bv-to-int.smt2
new file mode 100644
index 00000000000..8e036a3aaa4
--- /dev/null
+++ b/regression/strings/test3/test-bv-to-int.smt2
@@ -0,0 +1,25 @@
+(set-option :produce-models true)
+(set-logic ALL_SUPPORTED)
+
+(declare-fun s () String)
+(declare-fun s2 () String)
+(declare-fun s3 () String)
+
+(define-sort cprover.Pos () (_ BitVec 32))
+(define-fun cprover.ubv_to_int ((?x cprover.Pos)) Int (let ((bit0 (_ bv0 1)))
+ (+ (ite (= ((_ extract 0 0) ?x) bit0) 0 1) (ite (= ((_ extract 1 1) ?x) bit0) 0 2) (ite (= ((_ extract 2 2) ?x) bit0) 0 4) (ite (= ((_ extract 3 3) ?x) bit0) 0 8) (ite (= ((_ extract 4 4) ?x) bit0) 0 16) (ite (= ((_ extract 5 5) ?x) bit0) 0 32) (ite (= ((_ extract 6 6) ?x) bit0) 0 64) (ite (= ((_ extract 7 7) ?x) bit0) 0 128) (ite (= ((_ extract 8 8) ?x) bit0) 0 256) (ite (= ((_ extract 9 9) ?x) bit0) 0 512) (ite (= ((_ extract 10 10) ?x) bit0) 0 1024) (ite (= ((_ extract 11 11) ?x) bit0) 0 2048) (ite (= ((_ extract 12 12) ?x) bit0) 0 4096) (ite (= ((_ extract 13 13) ?x) bit0) 0 8192) (ite (= ((_ extract 14 14) ?x) bit0) 0 16384) (ite (= ((_ extract 15 15) ?x) bit0) 0 32768) (ite (= ((_ extract 16 16) ?x) bit0) 0 65536) (ite (= ((_ extract 17 17) ?x) bit0) 0 131072) (ite (= ((_ extract 18 18) ?x) bit0) 0 262144) (ite (= ((_ extract 19 19) ?x) bit0) 0 524288) (ite (= ((_ extract 20 20) ?x) bit0) 0 1048576) (ite (= ((_ extract 21 21) ?x) bit0) 0 2097152) (ite (= ((_ extract 22 22) ?x) bit0) 0 4194304) (ite (= ((_ extract 23 23) ?x) bit0) 0 8388608) (ite (= ((_ extract 24 24) ?x) bit0) 0 16777216) (ite (= ((_ extract 25 25) ?x) bit0) 0 33554432) (ite (= ((_ extract 26 26) ?x) bit0) 0 67108864) (ite (= ((_ extract 27 27) ?x) bit0) 0 134217728) (ite (= ((_ extract 28 28) ?x) bit0) 0 268435456) (ite (= ((_ extract 29 29) ?x) bit0) 0 536870912) (ite (= ((_ extract 30 30) ?x) bit0) 0 1073741824) (ite (= ((_ extract 31 31) ?x) bit0) 0 2147483648) 0)))
+
+(declare-fun bvi () cprover.Pos)
+(define-fun i () Int (cprover.ubv_to_int bvi))
+
+(assert (= s (str.++ s2 s3)))
+
+(assert (= (str.len s2) i))
+(assert (= s3 "pippo"))
+
+(define-fun p1 () Bool (= (str.len s) (+ i 5)))
+(define-fun p2 () Bool (str.suffixof "po" s))
+(define-fun p3 () Bool (= (str.at s i) "p"))
+
+(assert (or (not p1) (not p2) (not p3)))
+(check-sat)
diff --git a/regression/strings/test3/test-int.smt2 b/regression/strings/test3/test-int.smt2
new file mode 100644
index 00000000000..1cebe5cba31
--- /dev/null
+++ b/regression/strings/test3/test-int.smt2
@@ -0,0 +1,20 @@
+(set-option :produce-models true)
+(set-logic ALL_SUPPORTED)
+
+(declare-fun s () String)
+(declare-fun s2 () String)
+(declare-fun s3 () String)
+
+(declare-fun i () Int)
+
+(assert (= s (str.++ s2 s3)))
+
+(assert (= (str.len s2) i))
+(assert (= s3 "pippo"))
+
+(define-fun p1 () Bool (= (str.len s) (+ i 5)))
+(define-fun p2 () Bool (str.suffixof "po" s))
+(define-fun p3 () Bool (= (str.at s i) "p"))
+
+(assert (or (not p1) (not p2) (not p3)))
+(check-sat)
diff --git a/regression/strings/test3/test.c b/regression/strings/test3/test.c
new file mode 100644
index 00000000000..2fa4b22e017
--- /dev/null
+++ b/regression/strings/test3/test.c
@@ -0,0 +1,21 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+    __CPROVER_string s, s2, s3;
+    int i;
+
+    s = __CPROVER_string_concat(s2, s3);
+    __CPROVER_assume(__CPROVER_string_length(s2) == i);
+    __CPROVER_assume(
+        __CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
+
+    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_string_issuffix(__CPROVER_string_literal("p!o"), s));
+
+    return 0;
+}
diff --git a/regression/strings/test3/test.desc b/regression/strings/test3/test.desc
new file mode 100644
index 00000000000..6cacec86a19
--- /dev/null
+++ b/regression/strings/test3/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--pass
+^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$
+--
diff --git a/regression/strings/test4/test.c b/regression/strings/test4/test.c
new file mode 100644
index 00000000000..d73324f8ef4
--- /dev/null
+++ b/regression/strings/test4/test.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+    __CPROVER_string s;
+    int i;
+    int j;
+    i = 2;
+    s = __CPROVER_string_literal("pippo");
+    if (__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")) {
+        j = 1;
+    }
+    assert(j == 1);
+    return 0;
+}
diff --git a/regression/strings/test4/test.desc b/regression/strings/test4/test.desc
new file mode 100644
index 00000000000..0f5bd6ccca7
--- /dev/null
+++ b/regression/strings/test4/test.desc
@@ -0,0 +1,7 @@
+CORE
+test.c
+--pass
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/strings/test5/test.c b/regression/strings/test5/test.c
new file mode 100644
index 00000000000..812a20f3442
--- /dev/null
+++ b/regression/strings/test5/test.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+void main()
+{
+    __CPROVER_string x, y, z, w;
+
+    if (__CPROVER_string_equal(z, __CPROVER_string_concat(x, y)) &&
+        __CPROVER_string_equal(z, __CPROVER_string_concat(w, __CPROVER_string_literal("c"))) &&
+        __CPROVER_string_equal(__CPROVER_string_concat(__CPROVER_string_literal("c"), y), __CPROVER_string_concat(__CPROVER_string_literal("c"), __CPROVER_string_concat(__CPROVER_string_literal("b"), __CPROVER_string_literal("c"))))) {
+        assert(0);
+    }
+}
diff --git a/regression/strings/test5/test.desc b/regression/strings/test5/test.desc
new file mode 100644
index 00000000000..dbf3c40cfdb
--- /dev/null
+++ b/regression/strings/test5/test.desc
@@ -0,0 +1,7 @@
+CORE
+test.c
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
diff --git a/regression/strings/test_char_set/test.c b/regression/strings/test_char_set/test.c
new file mode 100644
index 00000000000..61aaf9b768e
--- /dev/null
+++ b/regression/strings/test_char_set/test.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s = __CPROVER_string_literal("abc");;
+  char c = 'p';
+  __CPROVER_string t = __CPROVER_char_set(s,1,c);;
+  
+  assert(__CPROVER_string_equal(t, __CPROVER_string_literal("apc")));
+  assert(__CPROVER_string_equal(t, __CPROVER_string_literal("abc")));
+  return 0;
+}
diff --git a/regression/strings/test_char_set/test.desc b/regression/strings/test_char_set/test.desc
new file mode 100644
index 00000000000..8cf42dda8f3
--- /dev/null
+++ b/regression/strings/test_char_set/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.c
+--pass
+^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$
+--
diff --git a/regression/strings/test_concat/test.c b/regression/strings/test_concat/test.c
new file mode 100644
index 00000000000..ceab520e960
--- /dev/null
+++ b/regression/strings/test_concat/test.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s,t,u;
+  unsigned i = __CPROVER_string_length(s);
+  t = __CPROVER_string_literal("ppo");
+  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"));
+  return 0;
+}
diff --git a/regression/strings/test_concat/test.desc b/regression/strings/test_concat/test.desc
new file mode 100644
index 00000000000..e5d8b30d6da
--- /dev/null
+++ b/regression/strings/test_concat/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.c
+--pass
+^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$
+--
diff --git a/regression/strings/test_contains/test.c b/regression/strings/test_contains/test.c
new file mode 100644
index 00000000000..9e7c627f3c4
--- /dev/null
+++ b/regression/strings/test_contains/test.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s1 = __CPROVER_string_literal("a1");
+  __CPROVER_string s2 = __CPROVER_string_literal("2b");
+  __CPROVER_string t = __CPROVER_string_concat(s1, s2);
+  
+  int i = nondet_int();
+  
+
+  if(i==1) 
+    assert(!__CPROVER_string_contains(t,__CPROVER_string_literal("3")));
+  else if(i==2)
+    assert(__CPROVER_string_contains(t,__CPROVER_string_literal("12")));
+  else if(i==3)
+    assert(!__CPROVER_string_contains(t,__CPROVER_string_literal("b")));
+
+  return 0;
+}
diff --git a/regression/strings/test_contains/test.desc b/regression/strings/test_contains/test.desc
new file mode 100644
index 00000000000..8275425c548
--- /dev/null
+++ b/regression/strings/test_contains/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+test.c
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"3\")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"12\")): SUCCESS$
+^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"b\")): FAILURE$
+--
diff --git a/regression/strings/test_easychair/test.c b/regression/strings/test_easychair/test.c
new file mode 100644
index 00000000000..5d249225280
--- /dev/null
+++ b/regression/strings/test_easychair/test.c
@@ -0,0 +1,43 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+#define false 0
+#define true 1
+
+int main(){
+  //IsEasyChairQuery
+  __CPROVER_string str;
+  // (1) check that str contains "/" followed by anything not
+  // containing "/" and containing "EasyChair"
+  int lastSlash = __CPROVER_string_last_index_of(str,__CPROVER_char_literal("/"));
+  if(lastSlash < 0) {
+    __CPROVER_assert(false,"PC1");
+    return false;
+  }
+
+  __CPROVER_string rest = __CPROVER_string_substring(str,lastSlash + 1, __CPROVER_string_length(str)-1);
+
+  if(! __CPROVER_string_contains(rest,__CPROVER_string_literal("EasyChair"))) {
+    __CPROVER_assert(false,"PC2");
+    return false;
+  }
+
+  // (2) Check that str starts with "http://"
+  if(! __CPROVER_string_isprefix(__CPROVER_string_literal("http://"),str)) {
+    __CPROVER_assert(false,"PC3");
+    return false;
+  }
+  //(3) Take the string between "http://" and the last "/".
+  // if it starts with "www." strip the "www." off
+  __CPROVER_string t = __CPROVER_string_substring(str,__CPROVER_string_length(__CPROVER_string_literal("http://")), lastSlash - __CPROVER_string_length(__CPROVER_string_literal("http://")));
+  if(__CPROVER_string_isprefix(__CPROVER_string_literal("www."),t))
+    t = __CPROVER_string_substring(t,__CPROVER_string_length(__CPROVER_string_literal("www.")), __CPROVER_string_length(t)-1);
+  // (4) Check that after stripping we have either "live.com"
+  // or "google.com"
+  if (!__CPROVER_string_equal(t,__CPROVER_string_literal("live.com")) && !__CPROVER_string_equal(t,__CPROVER_string_literal( "google.com"))) {
+    __CPROVER_assert(false,"PC4");
+    return false;
+  }
+  // s survived all checks
+  return true;
+}
+
diff --git a/regression/strings/test_equal/test.c b/regression/strings/test_equal/test.c
new file mode 100644
index 00000000000..2f26689589d
--- /dev/null
+++ b/regression/strings/test_equal/test.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s;
+  s = __CPROVER_string_literal("pippo");
+  assert(__CPROVER_string_equal(s, __CPROVER_string_literal("pippo")));
+  assert(__CPROVER_string_equal(s, __CPROVER_string_literal("mippo")));
+    
+  return 0;
+}
diff --git a/regression/strings/test_equal/test.desc b/regression/strings/test_equal/test.desc
new file mode 100644
index 00000000000..81ad6913856
--- /dev/null
+++ b/regression/strings/test_equal/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.c
+--pass
+^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$
+--
diff --git a/regression/strings/test_index_of/test.c b/regression/strings/test_index_of/test.c
new file mode 100644
index 00000000000..d64d3c2d66e
--- /dev/null
+++ b/regression/strings/test_index_of/test.c
@@ -0,0 +1,20 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+#define false 0
+#define true 1
+
+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("/"));
+
+  __CPROVER_assume(__CPROVER_string_equal(str, __CPROVER_string_literal("abc/abc/abc")));
+
+  assert(firstSlash == 3);
+  assert(lastSlash == 7);
+
+  assert(firstSlash != 3 || lastSlash != 7);
+
+  return 0;
+}
diff --git a/regression/strings/test_index_of/test.desc b/regression/strings/test_index_of/test.desc
new file mode 100644
index 00000000000..af22cc2efb5
--- /dev/null
+++ b/regression/strings/test_index_of/test.desc
@@ -0,0 +1,9 @@
+CORE
+test.c
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] assertion firstSlash == 3: SUCCESS$
+^\[main.assertion.2\] assertion lastSlash == 7: SUCCESS$
+^\[main.assertion.3\] assertion firstSlash != 3 || lastSlash != 7: FAILURE$
+--
\ No newline at end of file
diff --git a/regression/strings/test_int/test.c b/regression/strings/test_int/test.c
new file mode 100644
index 00000000000..3f8f8651783
--- /dev/null
+++ b/regression/strings/test_int/test.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s;
+  unsigned 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"));
+
+  assert(j == 234);
+  assert(j < 233 || __CPROVER_char_at(s,2)  == '4');
+  return 0;
+}
diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc
new file mode 100644
index 00000000000..e46e43ed936
--- /dev/null
+++ b/regression/strings/test_int/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--pass
+^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.3\] assertion j == 234: SUCCESS$
+^\[main.assertion.4\] assertion j < 233 || __CPROVER_uninterpreted_string_char_at_func(s, 2) == .4.: FAILURE$
+--
diff --git a/regression/strings/test_pass1/test.c b/regression/strings/test_pass1/test.c
new file mode 100644
index 00000000000..0ec758c9f64
--- /dev/null
+++ b/regression/strings/test_pass1/test.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string t;
+  __CPROVER_string s = __CPROVER_string_concat(t, t);
+  __CPROVER_assume(__CPROVER_string_equal(s, __CPROVER_string_literal("aa")));
+ 
+  assert(__CPROVER_string_equal(t,__CPROVER_string_literal("a")));  
+  assert(!__CPROVER_string_equal(t,__CPROVER_string_literal("a")));
+  // Warning the following does not express the same thing, because
+  // equality can fail while the two sides represent the same thing:
+  //assert(t  == __CPROVER_string_literal("a"));
+  //assert(t != __CPROVER_string_literal("a"));
+  return 0;
+}
diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc
new file mode 100644
index 00000000000..2531c253510
--- /dev/null
+++ b/regression/strings/test_pass1/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+test.c
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): SUCCESS
+^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): FAILURE$
+^\*\* 1 of 2 failed (2 iterations)$
+
diff --git a/regression/strings/test_pass_pc1/test.c b/regression/strings/test_pass_pc1/test.c
new file mode 100644
index 00000000000..95dadef8c1d
--- /dev/null
+++ b/regression/strings/test_pass_pc1/test.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s1,s2;
+  __CPROVER_string t = __CPROVER_string_concat(s1, s2);
+  __CPROVER_assume(__CPROVER_string_isprefix(__CPROVER_string_literal("a1"),s1));
+ 
+  __CPROVER_assume(__CPROVER_string_contains(s2,__CPROVER_string_literal("12")));
+
+  __CPROVER_assume(__CPROVER_string_issuffix(__CPROVER_string_literal("cd"),t));
+
+  assert(__CPROVER_string_length(t) > 3);
+  assert(__CPROVER_string_length(t) > 4);
+  return 0;
+}
diff --git a/regression/strings/test_pass_pc3/test.c b/regression/strings/test_pass_pc3/test.c
new file mode 100644
index 00000000000..e70b34b898d
--- /dev/null
+++ b/regression/strings/test_pass_pc3/test.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s1,s2,s3;
+  __CPROVER_string t = __CPROVER_string_concat(s1,__CPROVER_string_concat(s2, s3));
+  __CPROVER_assume(__CPROVER_string_equal(t, __CPROVER_string_literal("aaaa")));
+  __CPROVER_assume(__CPROVER_string_length(s1) >= __CPROVER_string_length(s2));
+  __CPROVER_assume(__CPROVER_string_length(s2) >= __CPROVER_string_length(s3));
+
+  assert(__CPROVER_string_length(s3) == 0);
+  assert(__CPROVER_string_length(s3) < 2);
+  return 0;
+}
diff --git a/regression/strings/test_pass_pc3/test.desc b/regression/strings/test_pass_pc3/test.desc
new file mode 100644
index 00000000000..b4c45aee0ee
--- /dev/null
+++ b/regression/strings/test_pass_pc3/test.desc
@@ -0,0 +1,9 @@
+CORE
+test.c
+--pass
+^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$
+^VERIFICATION FAILED$
+
diff --git a/regression/strings/test_prefix/test.c b/regression/strings/test_prefix/test.c
new file mode 100644
index 00000000000..041a6a3ed41
--- /dev/null
+++ b/regression/strings/test_prefix/test.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s = __CPROVER_string_literal("Hello World!");
+
+  //__CPROVER_assume(__CPROVER_string_equal(s, __CPROVER_string_literal("Hello World!")));
+
+  __CPROVER_bool b = __CPROVER_string_isprefix(__CPROVER_string_literal("Hello"),s);
+  __CPROVER_bool c = __CPROVER_string_isprefix(__CPROVER_string_literal("Wello"),s);
+  assert(b);
+  assert(c);
+    
+  return 0;
+}
diff --git a/regression/strings/test_prefix/test.desc b/regression/strings/test_prefix/test.desc
new file mode 100644
index 00000000000..187565433e4
--- /dev/null
+++ b/regression/strings/test_prefix/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.c
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] assertion b: SUCCESS$
+^\[main.assertion.2\] assertion c: FAILURE$
+--
diff --git a/regression/strings/test_strlen/test.c b/regression/strings/test_strlen/test.c
new file mode 100644
index 00000000000..d3a4348bd43
--- /dev/null
+++ b/regression/strings/test_strlen/test.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s,t;
+  int len_s, len_t;
+  s = __CPROVER_string_literal("abc");
+  t = __CPROVER_string_literal("xyz");
+  len_s = __CPROVER_string_length(s);
+  len_t = __CPROVER_string_length(t);
+  assert(len_s == len_t);
+  assert(len_s == 2);
+  return 0;
+}
diff --git a/regression/strings/test_strlen/test.desc b/regression/strings/test_strlen/test.desc
new file mode 100644
index 00000000000..a35e2499c9f
--- /dev/null
+++ b/regression/strings/test_strlen/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.c
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] assertion len_s == len_t: SUCCESS$
+^\[main.assertion.2\] assertion len_s == 2: FAILURE$
+--
diff --git a/regression/strings/test_substring/test.c b/regression/strings/test_substring/test.c
new file mode 100644
index 00000000000..d2c26eca01a
--- /dev/null
+++ b/regression/strings/test_substring/test.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s = __CPROVER_string_literal("abcdef");
+  __CPROVER_string t = __CPROVER_string_substring(s,2,4);
+  
+  assert(__CPROVER_string_equal(t,__CPROVER_string_literal("cd")));
+  assert(__CPROVER_string_equal(t,__CPROVER_string_literal("cc")));
+  assert(!__CPROVER_string_equal(t,__CPROVER_string_literal("bc")));
+  assert(!__CPROVER_string_equal(t,__CPROVER_string_literal("cd")));
+  return 0;
+}
diff --git a/regression/strings/test_substring/test.desc b/regression/strings/test_substring/test.desc
new file mode 100644
index 00000000000..6fe9134b59d
--- /dev/null
+++ b/regression/strings/test_substring/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--pass
+^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$
+--
\ No newline at end of file
diff --git a/regression/strings/test_suffix/test.c b/regression/strings/test_suffix/test.c
new file mode 100644
index 00000000000..d28bde61712
--- /dev/null
+++ b/regression/strings/test_suffix/test.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+#include "../cprover-string-hack.h"
+
+
+int main()
+{
+  __CPROVER_string s;
+
+  __CPROVER_assume(__CPROVER_string_equal(s, __CPROVER_string_literal("pippo")));
+
+  assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"),s));
+  assert(__CPROVER_string_issuffix(__CPROVER_string_literal("pp"),s));
+    
+  return 0;
+}
diff --git a/regression/strings/test_suffix/test.desc b/regression/strings/test_suffix/test.desc
new file mode 100644
index 00000000000..e0e8af7704c
--- /dev/null
+++ b/regression/strings/test_suffix/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.c
+--pass
+^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$
+--