diff --git a/jbmc/regression/strings-smoke-tests/java_string_printable/Test.class b/jbmc/regression/strings-smoke-tests/java_string_printable/Test.class
index ade78f8eb5..ec9ee8ea0c 100644
Binary files a/jbmc/regression/strings-smoke-tests/java_string_printable/Test.class and b/jbmc/regression/strings-smoke-tests/java_string_printable/Test.class differ
diff --git a/jbmc/regression/strings-smoke-tests/java_string_printable/Test.java b/jbmc/regression/strings-smoke-tests/java_string_printable/Test.java
index eecc244c9e..6a1cab2b15 100644
--- a/jbmc/regression/strings-smoke-tests/java_string_printable/Test.java
+++ b/jbmc/regression/strings-smoke-tests/java_string_printable/Test.java
@@ -33,4 +33,14 @@ public class Test {
       return b;
     }
 
+    public static boolean printable_char_array(char[] c) {
+      if(c.length != 3 || c == null)
+        return false;
+      boolean b0 = c[0] >= ' ' && c[0] <= '~';
+      boolean b1 = c[1] >= ' ' && c[1] <= '~';
+      boolean b2 = c[2] >= ' ' && c[2] <= '~';
+      assert(b0 || b1 || b2);
+      return b0 || b1 || b2;
+    }
+
 }
diff --git a/jbmc/regression/strings-smoke-tests/java_string_printable/test_nonprintable_char_array.desc b/jbmc/regression/strings-smoke-tests/java_string_printable/test_nonprintable_char_array.desc
new file mode 100644
index 0000000000..4e477ae017
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_string_printable/test_nonprintable_char_array.desc
@@ -0,0 +1,11 @@
+FUTURE
+Test.class
+--function Test.printable_char_array --max-nondet-string-length 100
+assertion.* file Test.java line 42 .* FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+Shows that the assertion can be violated when string-printable is not enabled
+for character arrays
+
+The constraint has not been implemented for char arrays.
diff --git a/jbmc/regression/strings-smoke-tests/java_string_printable/test_printable_char_array.desc b/jbmc/regression/strings-smoke-tests/java_string_printable/test_printable_char_array.desc
new file mode 100644
index 0000000000..563894a8b9
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_string_printable/test_printable_char_array.desc
@@ -0,0 +1,12 @@
+FUTURE
+Test.class
+--function Test.printable_char_array --max-nondet-string-length 100 --string-printable
+^EXIT=10$
+^SIGNAL=0$
+--
+assertion.* file Test.java line 42 .* FAILURE
+--
+Shows that the assertion can be violated when string-printable is not enabled
+for character arrays
+
+The constraint has not been implemented for char arrays.