diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.class b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.class
new file mode 100644
index 00000000000..fe13d89a5c9
Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.class differ
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java
new file mode 100644
index 00000000000..3244e91fc6d
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test.java
@@ -0,0 +1,16 @@
+public class test
+{
+    public static void nondet(String stringArg)
+    {
+        StringBuilder sb = new StringBuilder(stringArg);
+        sb.append("Z");
+        String s = sb.toString();
+        if (s.startsWith("fg")) {
+            assert false;
+        } else if (s.endsWith("Z")) {
+            assert false;
+        } else {
+            assert false;
+        }
+    }
+}
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc
new file mode 100644
index 00000000000..0e6da5a1c97
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc
@@ -0,0 +1,10 @@
+CORE
+test.class
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+\[.*assertion\.1\] .* line 9 .* FAILURE
+^VERIFICATION FAILED$
+--
+--
+Check that StringBuilder.append() is correct when the base String is an input.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc
new file mode 100644
index 00000000000..10c1a6b6a64
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc
@@ -0,0 +1,10 @@
+CORE
+test.class
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.2"
+^EXIT=10$
+^SIGNAL=0$
+\[.*assertion\.2\] .* line 11.* FAILURE
+^VERIFICATION FAILED$
+--
+--
+Check that StringBuilder.append() is correct when the base String is an input.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc
new file mode 100644
index 00000000000..ac6bf282fb0
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc
@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+test.class
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.3"
+^EXIT=0$
+^SIGNAL=0$
+\[.*assertion\.3\] .* line 13.* SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check that StringBuilder.append() is correct when the base String is an input.
diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.class b/jbmc/regression/jbmc-strings/bug-test-gen-095/test.class
deleted file mode 100644
index 3895d218c3d..00000000000
Binary files a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.class and /dev/null differ
diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-095/test.desc
deleted file mode 100644
index 25b7c86bea2..00000000000
--- a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-FUTURE
-test.class
---max-nondet-string-length 1000
-^EXIT=10$
-^SIGNAL=0$
-\[.*assertion\.1\] .* line 8 .* FAILURE
-^VERIFICATION FAILED$
---
diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.java b/jbmc/regression/jbmc-strings/bug-test-gen-095/test.java
deleted file mode 100644
index a6910527551..00000000000
--- a/jbmc/regression/jbmc-strings/bug-test-gen-095/test.java
+++ /dev/null
@@ -1,10 +0,0 @@
-public class test
-{
-   public static void main(String[] args)
-   {
-      StringBuilder sb = new StringBuilder(args[0]);
-      sb.append("Z");
-      String s = sb.toString();
-      assert(s.equals("fg"));
-   }
-}