diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/Test.class
new file mode 100644
index 0000000000..87cad831d9
Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/Test.class differ
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/Test.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/Test.java
new file mode 100644
index 0000000000..389cb8363a
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/Test.java
@@ -0,0 +1,41 @@
+public class Test
+{
+  public void testSuccess1()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.setCharAt(0, 'd');
+    assert sb.toString().equals("dbc");
+  }
+
+  public void testSuccess2()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.setCharAt(2, 'd');
+    assert sb.toString().equals("abd");
+  }
+
+  public void testException1()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.setCharAt(-1, 'd');
+  }
+
+  public void testException2()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.setCharAt(3, 'd');
+  }
+
+  public void testNoPropagation1(StringBuilder sb)
+  {
+    sb.setCharAt(1, 'd');
+    assert sb.toString().equals("dbc");
+  }
+
+  public void testNoPropagation2(int index)
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.setCharAt(index, 'd');
+    assert sb.toString().equals("dbc");
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception1.desc
new file mode 100644
index 0000000000..36c1a99327
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception1.desc
@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testException1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testException1:()V.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception2.desc
new file mode 100644
index 0000000000..cab4e3caca
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception2.desc
@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testException2:()V.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_no_propagation1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_no_propagation1.desc
new file mode 100644
index 0000000000..b12a856457
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_no_propagation1.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation1:(Ljava/lang/StringBuilder;)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/ConstantEvaluationStringBuilderSetCharAt/test_no_propagation2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_no_propagation2.desc
new file mode 100644
index 0000000000..7e8e1d6973
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_no_propagation2.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation2:(I)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_success1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_success1.desc
new file mode 100644
index 0000000000..fb30de3341
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_success1.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess1 --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/ConstantEvaluationStringBuilderSetCharAt/test_success2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_success2.desc
new file mode 100644
index 0000000000..0bccdce46c
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_success2.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess2 --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$
+--
+--