diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java b/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java
index 7abf3d830ee..f2dae940421 100644
--- a/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java
+++ b/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java
@@ -49,13 +49,6 @@ void byteArray(byte[] array)
     }
   }
 
-  void boolArray(boolean[] array)
-  {
-    if (array != null && array.length > 1500 && array[1500] == true) {
-      assert false;
-    }
-  }
-
   void intArrayMulti(int[][] array)
   {
     if (array != null &&
diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc
deleted file mode 100644
index ab6596fc47e..00000000000
--- a/jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-NondetArrayPrimitive.class
---function NondetArrayPrimitive.boolArray --max-nondet-array-length 2000 --unwind 1
-^VERIFICATION FAILED$
-^EXIT=10$
-^SIGNAL=0$
-line 55 assertion.*: FAILURE
---
-Unwinding loop __CPROVER__start.0 iteration 2
-^warning: ignoring
---
-Check no unwind needed to reach non-primitive array cell
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index b0299d0d3de..1ee14c5ee54 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -1424,7 +1424,7 @@ void java_object_factoryt::gen_nondet_array_init(
     init_array_expr =
       typecast_exprt(init_array_expr, pointer_type(element_type));
 
-  if(element_type.id() == ID_pointer)
+  if(element_type.id() == ID_pointer || element_type.id() == ID_c_bool)
   {
     // For arrays of non-primitive types, nondeterministically initialize each
     // element of the array
@@ -1441,6 +1441,9 @@ void java_object_factoryt::gen_nondet_array_init(
   else
   {
     // Arrays of primitive types can be initialized with a single instruction
+    // We don't do this for arrays of Booleans, because Bools are represented
+    // as bytes, so each cell must be initialized in a particular way (see
+    // gen_nondet_init).
     array_primitive_init_code(
       assignments,
       init_array_expr,