diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.class
new file mode 100644
index 0000000000..a0531eb3ef
Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.class differ
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.java
new file mode 100644
index 0000000000..95d424d4fa
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.java
@@ -0,0 +1,22 @@
+public class Test
+{
+  public void testSuccess()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    Integer i = new Integer(3);
+    sb.append(i);
+    assert sb.toString().equals("abc3");
+
+    sb.append((Object)"xyz");
+    assert sb.toString().equals("abc3xyz");
+
+    sb.append((Object)null);
+    assert sb.toString().equals("abc3xyznull");
+  }
+
+  public void testNoPropagation(Object obj)
+  {
+    StringBuffer sb = new StringBuffer();
+    assert obj.toString().equals("");
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_no_propagation.desc
new file mode 100644
index 0000000000..139f500f8c
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_no_propagation.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation:(Ljava/lang/Object;)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_success.desc
new file mode 100644
index 0000000000..8d1b5b06f4
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_success.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.class
new file mode 100644
index 0000000000..281da1a9a1
Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.class differ
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.java
new file mode 100644
index 0000000000..d15ea03fdf
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.java
@@ -0,0 +1,22 @@
+public class Test
+{
+  public void testSuccess()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    Integer i = new Integer(3);
+    sb.append(i);
+    assert sb.toString().equals("abc3");
+
+    sb.append((Object)"xyz");
+    assert sb.toString().equals("abc3xyz");
+
+    sb.append((Object)null);
+    assert sb.toString().equals("abc3xyznull");
+  }
+
+  public void testNoPropagation(Object obj)
+  {
+    StringBuilder sb = new StringBuilder();
+    assert obj.toString().equals("");
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_no_propagation.desc
new file mode 100644
index 0000000000..139f500f8c
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_no_propagation.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation:(Ljava/lang/Object;)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_success.desc
new file mode 100644
index 0000000000..8d1b5b06f4
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_success.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--