diff --git a/regression/jbmc-strings/StringLastIndexOf/Test.class b/regression/jbmc-strings/StringLastIndexOf/Test.class
index 609cc4f3348..6f4767b8b33 100644
Binary files a/regression/jbmc-strings/StringLastIndexOf/Test.class and b/regression/jbmc-strings/StringLastIndexOf/Test.class differ
diff --git a/regression/jbmc-strings/StringLastIndexOf/Test.java b/regression/jbmc-strings/StringLastIndexOf/Test.java
index 38436b885bf..b86ce51169d 100644
--- a/regression/jbmc-strings/StringLastIndexOf/Test.java
+++ b/regression/jbmc-strings/StringLastIndexOf/Test.java
@@ -13,7 +13,7 @@ public void check(String input_String1, String input_String2, int i) {
                 // Contradiction with the previous condition (should fail).
                 assert "foo".lastIndexOf("") != 3;
             } else if (i == 2 && input_String2.length() > 0) {
-                int lio = input_String1.lastIndexOf(input_String2.charAt(0), fromIndex);
+                int lio = input_String1.lastIndexOf(org.cprover.CProverString.charAt(input_String2, 0), fromIndex);
                 if (input_String2.length() == 0)
                     assert lio == fromIndex;
             } else if (i == 3) {
diff --git a/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class b/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class
index 96733a2b713..156f2f2d791 100644
Binary files a/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class and b/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class differ
diff --git a/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java b/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java
index c06e96a5ced..ce8d3a2e06c 100644
--- a/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java
+++ b/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java
@@ -8,7 +8,7 @@ public static char[] toCharArray(String s)
         char arr[]=new char[s.length()];
         // We limit arbitrarly the loop unfolding to 10
         for(int i=0; i<length && i<10; i++)
-            arr[i]=s.charAt(i);
+            arr[i]=org.cprover.CProverString.charAt(s, i);
         return arr;
     }
 
@@ -16,11 +16,11 @@ public static void main(String[] args)
     {
         String s1 = "diffblue";
         String s2 = "TESTGENERATION";
-        String s3 = "	automated   ";
+        String s3 = "   automated   ";
 
         assert s1.equals("diffblue");
         assert s2.equals("TESTGENERATION");
-        assert s3.equals("   automated	 ");
+        assert s3.equals("   automated   ");
 
         System.out.printf(
           "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
@@ -43,7 +43,7 @@ public static void main(String[] args)
         int i=0;
         for (char character : charArray)
         {
-            assert character=="diffblue".charAt(i);
+            assert character==org.cprover.CProverString.charAt("diffblue", i);
             ++i;
         }
 
diff --git a/regression/jbmc-strings/SubString01/SubString01.class b/regression/jbmc-strings/SubString01/SubString01.class
index 861bf6905d3..c6c9c4d4cec 100644
Binary files a/regression/jbmc-strings/SubString01/SubString01.class and b/regression/jbmc-strings/SubString01/SubString01.class differ
diff --git a/regression/jbmc-strings/SubString01/SubString01.java b/regression/jbmc-strings/SubString01/SubString01.java
index c99db9b7308..8e211318613 100644
--- a/regression/jbmc-strings/SubString01/SubString01.java
+++ b/regression/jbmc-strings/SubString01/SubString01.java
@@ -1,13 +1,12 @@
 public class SubString01
 {
-   public static void main(String[] args)
-   {
-      String letters = "automatictestcasegenerationatdiffblue";
+    public static void main(String[] args)
+    {
+        String letters = "automatictestcasegenerationatdiffblue";
 
-      String tmp=letters.substring(20);
-      assert tmp.equals("erationatdiffblue");
-
-      tmp=letters.substring(9, 13);
-      assert tmp.equals("test");
-   }
+        String tmp=org.cprover.CProverString.substring(letters, 20);
+        assert tmp.equals("erationatdiffblue");
+        tmp=org.cprover.CProverString.substring(letters, 9, 13);
+        assert tmp.equals("test");
+    }
 }
diff --git a/regression/jbmc-strings/cprover/CProverString.class b/regression/jbmc-strings/cprover/CProverString.class
new file mode 100644
index 00000000000..c1cf5742e39
Binary files /dev/null and b/regression/jbmc-strings/cprover/CProverString.class differ
diff --git a/regression/jbmc-strings/cprover/CProverString.java b/regression/jbmc-strings/cprover/CProverString.java
new file mode 100644
index 00000000000..572056b2100
--- /dev/null
+++ b/regression/jbmc-strings/cprover/CProverString.java
@@ -0,0 +1,29 @@
+package org.cprover;
+
+public final class CProverString {
+    public static char charAt(String s, int i) {
+        if (0 <= i && i < s.length())
+            return s.charAt(i);
+        else
+            return '\u0000';
+    }
+
+    public static String substring(String s, int i) {
+        if (i <= 0)
+            return s;
+        else if (i >= s.length())
+            return "";
+        else
+            return s.substring(i);
+    }
+
+    public static String substring(String s, int i, int j) {
+        if (i < 0)
+            return substring(s, 0, j);
+        if (j >= s.length())
+            return substring(s, 0, s.length() - 1);
+        if (i >= j)
+            return "";
+        return s.substring(i, j);
+    }
+}
diff --git a/regression/jbmc-strings/java_char_array_init/test_init.class b/regression/jbmc-strings/java_char_array_init/test_init.class
index f10bdeb9256..294c48eba4c 100644
Binary files a/regression/jbmc-strings/java_char_array_init/test_init.class and b/regression/jbmc-strings/java_char_array_init/test_init.class differ
diff --git a/regression/jbmc-strings/java_char_array_init/test_init.java b/regression/jbmc-strings/java_char_array_init/test_init.java
index 55f61983018..43b7c52ffdd 100644
--- a/regression/jbmc-strings/java_char_array_init/test_init.java
+++ b/regression/jbmc-strings/java_char_array_init/test_init.java
@@ -13,7 +13,7 @@ public static String stringOfCharArray(char arr[])
 
     public static String stringOfCharArray(char arr[], int i, int j)
     {
-        return stringOfCharArray(arr).substring(i, i+j);
+        return org.cprover.CProverString.substring(stringOfCharArray(arr), i, i+j);
     }
 
     public static void main(int i)
diff --git a/regression/jbmc-strings/java_concat/test_concat.class b/regression/jbmc-strings/java_concat/test_concat.class
index a69c05921f6..df929981f52 100644
Binary files a/regression/jbmc-strings/java_concat/test_concat.class and b/regression/jbmc-strings/java_concat/test_concat.class differ
diff --git a/regression/jbmc-strings/java_concat/test_concat.java b/regression/jbmc-strings/java_concat/test_concat.java
index 6bbe753b2e4..9f4d3f5e371 100644
--- a/regression/jbmc-strings/java_concat/test_concat.java
+++ b/regression/jbmc-strings/java_concat/test_concat.java
@@ -6,7 +6,7 @@ public static void main(/*String[] argv*/)
       int i = s.length();
       String t = new String("ppo");
       String u = s.concat(t);
-      char c = u.charAt(i);
+      char c = org.cprover.CProverString.charAt(u, i);
       assert(c == 'p');
       assert(c != 'p');
    }
diff --git a/regression/strings-smoke-tests/cprover/CProverString.class b/regression/strings-smoke-tests/cprover/CProverString.class
new file mode 100644
index 00000000000..c1cf5742e39
Binary files /dev/null and b/regression/strings-smoke-tests/cprover/CProverString.class differ
diff --git a/regression/strings-smoke-tests/cprover/CProverString.java b/regression/strings-smoke-tests/cprover/CProverString.java
new file mode 100644
index 00000000000..572056b2100
--- /dev/null
+++ b/regression/strings-smoke-tests/cprover/CProverString.java
@@ -0,0 +1,29 @@
+package org.cprover;
+
+public final class CProverString {
+    public static char charAt(String s, int i) {
+        if (0 <= i && i < s.length())
+            return s.charAt(i);
+        else
+            return '\u0000';
+    }
+
+    public static String substring(String s, int i) {
+        if (i <= 0)
+            return s;
+        else if (i >= s.length())
+            return "";
+        else
+            return s.substring(i);
+    }
+
+    public static String substring(String s, int i, int j) {
+        if (i < 0)
+            return substring(s, 0, j);
+        if (j >= s.length())
+            return substring(s, 0, s.length() - 1);
+        if (i >= j)
+            return "";
+        return s.substring(i, j);
+    }
+}
diff --git a/regression/strings-smoke-tests/java_append_string/test_append_string.class b/regression/strings-smoke-tests/java_append_string/test_append_string.class
index a0880dfa764..3594e509e87 100644
Binary files a/regression/strings-smoke-tests/java_append_string/test_append_string.class and b/regression/strings-smoke-tests/java_append_string/test_append_string.class differ
diff --git a/regression/strings-smoke-tests/java_append_string/test_append_string.java b/regression/strings-smoke-tests/java_append_string/test_append_string.java
index 26de37e97d4..83a9ddf9b4c 100644
--- a/regression/strings-smoke-tests/java_append_string/test_append_string.java
+++ b/regression/strings-smoke-tests/java_append_string/test_append_string.java
@@ -20,7 +20,7 @@ public static void check(StringBuilder sb, String str)
             sb.append(str, 2, 4);
             String res = sb.toString();
             assert(res.startsWith(init));
-            assert(res.endsWith(str.substring(2, 4)));
+            assert(res.endsWith(org.cprover.CProverString.substring(str, 2, 4)));
             assert(res.length() == init.length() + 2);
             assert(!res.equals("foobarfuz"));
         }
diff --git a/regression/strings-smoke-tests/java_char_array/test_char_array.class b/regression/strings-smoke-tests/java_char_array/test_char_array.class
index 709157cf470..bf4d9ea4993 100644
Binary files a/regression/strings-smoke-tests/java_char_array/test_char_array.class and b/regression/strings-smoke-tests/java_char_array/test_char_array.class differ
diff --git a/regression/strings-smoke-tests/java_char_array/test_char_array.java b/regression/strings-smoke-tests/java_char_array/test_char_array.java
index 34d6f009e55..7a9351d0afb 100644
--- a/regression/strings-smoke-tests/java_char_array/test_char_array.java
+++ b/regression/strings-smoke-tests/java_char_array/test_char_array.java
@@ -8,7 +8,7 @@ public static char[] toCharArray(String s)
         char arr[] = new char[s.length()];
         // We limit arbitrarly the loop unfolding to 5
         for(int i = 0; i < length && i < 5; i++)
-        arr[i] = s.charAt(i);
+            arr[i] = org.cprover.CProverString.charAt(s, i);
         return arr;
     }
 
@@ -17,7 +17,7 @@ public static void main(int i)
         String s = "abc";
         char [] str = toCharArray(s);
         char c = str[2];
-        char a = s.charAt(0);
+        char a = org.cprover.CProverString.charAt(s, 0);
         assert(str.length == 3);
         assert(a == 'a');
         assert(c == 'c');
diff --git a/regression/strings-smoke-tests/java_char_at/test_char_at.class b/regression/strings-smoke-tests/java_char_at/test_char_at.class
index de5fe888245..84d68a19c5e 100644
Binary files a/regression/strings-smoke-tests/java_char_at/test_char_at.class and b/regression/strings-smoke-tests/java_char_at/test_char_at.class differ
diff --git a/regression/strings-smoke-tests/java_char_at/test_char_at.java b/regression/strings-smoke-tests/java_char_at/test_char_at.java
index 3b8663d62ae..c91fc7d1cff 100644
--- a/regression/strings-smoke-tests/java_char_at/test_char_at.java
+++ b/regression/strings-smoke-tests/java_char_at/test_char_at.java
@@ -2,6 +2,6 @@ public class test_char_at {
 
   public static void main(/*String[] argv*/) {
     String s = new String("abc");
-    assert(s.charAt(2)=='c');
+    assert(org.cprover.CProverString.charAt(s, 2)=='c');
   }
 }
diff --git a/regression/strings-smoke-tests/java_code_point/test_code_point.class b/regression/strings-smoke-tests/java_code_point/test_code_point.class
index 1d5d2269325..df523be365b 100644
Binary files a/regression/strings-smoke-tests/java_code_point/test_code_point.class and b/regression/strings-smoke-tests/java_code_point/test_code_point.class differ
diff --git a/regression/strings-smoke-tests/java_code_point/test_code_point.java b/regression/strings-smoke-tests/java_code_point/test_code_point.java
index faf9a2051d5..afc21c44fed 100644
--- a/regression/strings-smoke-tests/java_code_point/test_code_point.java
+++ b/regression/strings-smoke-tests/java_code_point/test_code_point.java
@@ -9,6 +9,6 @@ public static void main(/*String[] argv*/)
       assert(s.offsetByCodePoints(1,2) >= 3);
       StringBuilder sb = new StringBuilder();
       sb.appendCodePoint(0x10907);
-      assert(s.charAt(1) == sb.charAt(0));
+      assert(org.cprover.CProverString.charAt(s, 1) == org.cprover.CProverString.charAt(sb.toString(), 0));
    }
 }
diff --git a/regression/strings-smoke-tests/java_concat/test_concat.class b/regression/strings-smoke-tests/java_concat/test_concat.class
index e4143c15773..8802b3957d2 100644
Binary files a/regression/strings-smoke-tests/java_concat/test_concat.class and b/regression/strings-smoke-tests/java_concat/test_concat.class differ
diff --git a/regression/strings-smoke-tests/java_concat/test_concat.java b/regression/strings-smoke-tests/java_concat/test_concat.java
index b9909c723d4..9e861e722bf 100644
--- a/regression/strings-smoke-tests/java_concat/test_concat.java
+++ b/regression/strings-smoke-tests/java_concat/test_concat.java
@@ -6,7 +6,7 @@ public static void main(/*String[] argv*/)
       int i = s.length();
       String t = new String("ppo");
       String u = s.concat(t);
-      char c = u.charAt(i);
+      char c = org.cprover.CProverString.charAt(u, i);
       assert(c == 'p');
       assert(c == 'o');
    }
diff --git a/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class
index 6e843afbe2a..e83ac01dcaf 100644
Binary files a/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class and b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class differ
diff --git a/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java
index fd1d1fbf9e2..9e67eba0de7 100644
--- a/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java
+++ b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java
@@ -3,11 +3,11 @@ public class test_set_char_at
    public static void main(/*String[] argv*/)
    {
       String s = new String("Abc");
-      char c = s.charAt(1);
+      char c = org.cprover.CProverString.charAt(s, 1);
       StringBuilder sb = new StringBuilder(s);
       sb.setCharAt(1,'w');
       s = sb.toString();
       assert(s.equals("Awc"));
-      assert(s.charAt(2)=='c');
+      assert(org.cprover.CProverString.charAt(s, 2)=='c');
    }
 }
diff --git a/regression/strings-smoke-tests/java_substring/test_substring.class b/regression/strings-smoke-tests/java_substring/test_substring.class
index 3ba0b60e7f2..086aff06ab9 100644
Binary files a/regression/strings-smoke-tests/java_substring/test_substring.class and b/regression/strings-smoke-tests/java_substring/test_substring.class differ
diff --git a/regression/strings-smoke-tests/java_substring/test_substring.java b/regression/strings-smoke-tests/java_substring/test_substring.java
index 03a33fdbebd..e94ee9c51cb 100644
--- a/regression/strings-smoke-tests/java_substring/test_substring.java
+++ b/regression/strings-smoke-tests/java_substring/test_substring.java
@@ -3,10 +3,10 @@ public class test_substring
    public static void main(/*String[] argv*/)
    {
       String abcdef = "AbcDef";
-      String cde = abcdef.substring(2,5);
-      char c = cde.charAt(0);
-      char d = cde.charAt(1);
-      char e = cde.charAt(2);
+      String cde = org.cprover.CProverString.substring(abcdef, 2,5);
+      char c = org.cprover.CProverString.charAt(cde, 0);
+      char d = org.cprover.CProverString.charAt(cde, 1);
+      char e = org.cprover.CProverString.charAt(cde, 2);
       assert(c == 'c');
       assert(d == 'D');
       assert(e == 'e');
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
index 35ce5c63225..6cb6c6e5c96 100644
--- a/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1890,8 +1890,10 @@ void java_string_library_preprocesst::initialize_conversion_table()
     ["java::java.lang.String.<init>:()V"]=
       ID_cprover_string_empty_string_func;
 
+  // CProverString.charAt differs from the Java String.charAt in that no
+  // exception is raised for the out of bounds case.
   cprover_equivalent_to_java_function
-    ["java::java.lang.String.charAt:(I)C"]=
+    ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
       ID_cprover_string_char_at_func;
   cprover_equivalent_to_java_function
     ["java::java.lang.String.codePointAt:(I)I"]=
@@ -1999,11 +2001,15 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;"]=
       ID_cprover_string_substring_func;
+  // CProverString.substring differs from the Java String.substring in that no
+  // exception is raised for the out of bounds case.
   cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.substring:(II)Ljava/lang/String;"]=
+    ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
+    "Ljava/lang/String;"]=
       ID_cprover_string_substring_func;
   cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.substring:(I)Ljava/lang/String;"]=
+    ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
+    "Ljava/lang/String;"]=
       ID_cprover_string_substring_func;
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=