diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 55dfc96931f..3846845a336 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -549,7 +549,10 @@ void java_object_factoryt::gen_nondet_array_init(
 
     side_effect_exprt java_new_array(ID_java_new_array, expr.type());
     java_new_array.copy_to_operands(length_sym_expr);
-    java_new_array.set(ID_skip_initialize, true);
+    // Retain the array_set instruction for the special case of a
+    // zero-length array, where this will be the only assignment against
+    // the array's identifier.
+    java_new_array.set(ID_skip_initialize, false);
     java_new_array.type().subtype().set(ID_C_element_type, element_type);
     codet assign=code_assignt(expr, java_new_array);
     assign.add_source_location()=loc;
@@ -798,4 +801,3 @@ void gen_nondet_init(
     typet(),
     update_in_place);
 }
-