diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.class b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.class
index c7052b38c1f..5d0f85de997 100644
Binary files a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.class and b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.class differ
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java
index efb5524c2b8..ab8a67e316b 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java
+++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java
@@ -1,13 +1,33 @@
 public class StringBuilderConstructors01
 {
-   public static void main(String[] args)
-   {
-      StringBuilder buffer1 = new StringBuilder();
-      StringBuilder buffer2 = new StringBuilder(10);
-      StringBuilder buffer3 = new StringBuilder("diffblue");
-
-      assert buffer1.length()==0;
-      assert buffer2.length()==0;
-      assert buffer3.length()>0;
-   }
+  public static void noArgPass() {
+    StringBuilder buffer1 = new StringBuilder();
+    assert buffer1.length() == 0;
+  }
+
+  public static void noArgFail() {
+    StringBuilder buffer1 = new StringBuilder();
+    assert buffer1.length() != 0;
+  }
+
+  public static void capacityPass() {
+    StringBuilder buffer2 = new StringBuilder(10);
+    assert buffer2.length() == 0;
+  }
+
+  public static void capacityFail() {
+
+    StringBuilder buffer2 = new StringBuilder(10);
+    assert buffer2.length() != 0;
+  }
+
+  public static void stringPass() {
+    StringBuilder buffer3 = new StringBuilder("diffblue");
+    assert buffer3.length() == 8;
+  }
+
+  public static void stringFail() {
+    StringBuilder buffer3 = new StringBuilder("diffblue");
+    assert buffer3.length() != 8;
+  }
 }
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc
new file mode 100644
index 00000000000..b3ee4c9bb1f
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.capacityFail --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This is not working currently because the StringBuilder constructor with
+capacity argument is not modelled.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc
new file mode 100644
index 00000000000..3b5b65a053a
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.capacityPass --max-nondet-string-length 1000
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This is not working currently because the StringBuilder constructor with
+capacity argument is not modelled.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc
new file mode 100644
index 00000000000..f1846c50a63
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc
@@ -0,0 +1,12 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.noArgFail --max-nondet-string-length 1000 --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+dynamic_object2=\{\s*\}
+--
+^warning: ignoring
+--
+The check for dynamic_object2 is to make sure the array is created empty and
+is not given arbitrary content before its final assignment.
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-pass.desc
similarity index 54%
rename from jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc
rename to jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-pass.desc
index cfbea436519..6c2f63a597f 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-pass.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 StringBuilderConstructors01.class
---max-nondet-string-length 1000
+--function StringBuilderConstructors01.noArgPass --max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-fail.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-fail.desc
new file mode 100644
index 00000000000..ceb4abbcbf8
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-fail.desc
@@ -0,0 +1,8 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.stringFail --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-pass.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-pass.desc
new file mode 100644
index 00000000000..554c8004014
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-string-pass.desc
@@ -0,0 +1,8 @@
+CORE
+StringBuilderConstructors01.class
+--function StringBuilderConstructors01.stringPass --max-nondet-string-length 1000
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index 515e89f0656..f140877a0e4 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -199,6 +199,11 @@ void goto_symext::assign_string_constant(
   const ssa_exprt &char_array,
   const array_exprt &new_char_array)
 {
+  // We need to make sure that the length of the previous array isn't
+  // unconstrained, otherwise it could be arbitrarily large which causes
+  // invalid traces
+  symex_assume(state, equal_exprt{length, from_integer(0, length.type())});
+
   // assign length of string
   symex_assign.assign_symbol(length, expr_skeletont{}, new_length, {});
 
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 364a83b4376..920b3b1e699 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -590,6 +590,9 @@ class goto_symext
   /// "abc", the symbol will be named "abc_constant_char_array"). Then, the
   /// expression `&sym[0]` is assigned to `char_array` (assuming `sym` denotes
   /// the symbol holding the string data given by `new_char_array`.
+  /// The assignment is preceeded by an assume statement ensuring `length`
+  /// before this call was zero, this is to avoid leaving the previous array
+  /// unconstrained.
   ///
   /// \param state: goto symex state
   /// \param symex_assign: object handling symbol assignments