Restore array-set for nondet arrays

This was removed because the array is certain to be overwritten with
nondets, and thus the zero-init was worthless-- however, for the special
case of a zero-length array the init statement was the only assignment,
making the difference between the interpreter assigning it value {}
and assigning it no value at all. Ideally we should omit this most of the
time, but its cost is probably minimal and it's much simpler to keep it
than to track down all the special cases required to deal with a symbol
that is referred to but never defined in the inputs map.

Author: smowton

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);
 }
-