diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.class b/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.class
new file mode 100644
index 00000000000..d4632a8dfbf
Binary files /dev/null and b/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.class differ
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.java b/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.java
new file mode 100644
index 00000000000..28a084eb58c
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.java
@@ -0,0 +1,42 @@
+public class TestDeleteCharAt
+{
+   public static void testStringBuilderSuccess(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuilder sb = new StringBuilder(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ac");
+      assert b || result.equals("xz");
+   }
+
+   public static void testStringBuilderFailure(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuilder sb = new StringBuilder(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ab");
+      assert b || result.equals("yz");
+   }
+
+   public static void testStringBufferSuccess(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuffer sb = new StringBuffer(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ac");
+      assert b || result.equals("xz");
+   }
+
+   public static void testStringBufferFailure(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuffer sb = new StringBuffer(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ab");
+      assert b || result.equals("yz");
+   }
+}
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
deleted file mode 100644
index 11fd2e5474f..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-test_delete_char_at.class
---max-nondet-string-length 1000 --function test_delete_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class
deleted file mode 100644
index d9148dfc211..00000000000
Binary files a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class and /dev/null differ
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java
deleted file mode 100644
index 3121aab316c..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java
+++ /dev/null
@@ -1,11 +0,0 @@
-public class test_delete_char_at
-{
-   public static void main()
-   {
-      StringBuilder s = new StringBuilder();
-      s.append("Abc");
-      org.cprover.CProverString.deleteCharAt(s, 1);
-      String str = s.toString();
-      assert(str.equals("Ac"));
-   }
-}
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_failure.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_failure.desc
new file mode 100644
index 00000000000..fe62837c839
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_failure.desc
@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBufferFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_success.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_success.desc
new file mode 100644
index 00000000000..42af49d8fa8
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_success.desc
@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBufferSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_failure.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_failure.desc
new file mode 100644
index 00000000000..a7f3ccbfc5a
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_failure.desc
@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBuilderFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_success.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_success.desc
new file mode 100644
index 00000000000..84e3d5ff739
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_success.desc
@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBuilderSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+non equal types
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 044f13401fc..55ed8dc642c 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1507,7 +1507,7 @@ void java_string_library_preprocesst::initialize_conversion_table()
       ID_cprover_string_delete_func;
   cprover_equivalent_to_java_assign_and_return_function
     ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
-     "StringBufferI)Ljava/lang/StringBuffer;"] =
+     "StringBuffer;I)Ljava/lang/StringBuffer;"] =
       ID_cprover_string_delete_char_at_func;
   cprover_equivalent_to_java_assign_and_return_function
     ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"