diff --git a/regression/cbmc-java/NondetInitValidate/Test.class b/regression/cbmc-java/NondetInit/Test.class
similarity index 100%
rename from regression/cbmc-java/NondetInitValidate/Test.class
rename to regression/cbmc-java/NondetInit/Test.class
diff --git a/regression/cbmc-java/NondetInitValidate/Test.java b/regression/cbmc-java/NondetInit/Test.java
similarity index 100%
rename from regression/cbmc-java/NondetInitValidate/Test.java
rename to regression/cbmc-java/NondetInit/Test.java
diff --git a/regression/cbmc-java/NondetInitValidate/test.desc b/regression/cbmc-java/NondetInit/test.desc
similarity index 100%
rename from regression/cbmc-java/NondetInitValidate/test.desc
rename to regression/cbmc-java/NondetInit/test.desc
diff --git a/regression/cbmc-java/NondetInitValidate/test_lazy.desc b/regression/cbmc-java/NondetInit/test_lazy.desc
similarity index 100%
rename from regression/cbmc-java/NondetInitValidate/test_lazy.desc
rename to regression/cbmc-java/NondetInit/test_lazy.desc
diff --git a/regression/cbmc-java/NondetInit2/Test.class b/regression/cbmc-java/NondetInit2/Test.class
new file mode 100644
index 00000000000..323039fe3ae
Binary files /dev/null and b/regression/cbmc-java/NondetInit2/Test.class differ
diff --git a/regression/cbmc-java/NondetInit2/Test.java b/regression/cbmc-java/NondetInit2/Test.java
new file mode 100644
index 00000000000..8f81787947a
--- /dev/null
+++ b/regression/cbmc-java/NondetInit2/Test.java
@@ -0,0 +1,16 @@
+import org.cprover.CProver;
+
+class Test {
+
+    int[] arr;
+
+    void cproverNondetInitialize() {
+        CProver.assume(arr != null && arr.length == 1);
+        // The following access should now be legal:
+        arr[0] = 100;
+    }
+
+    public static void main(Test nondetInput) {
+    }
+
+}
diff --git a/regression/cbmc-java/NondetInit2/test.desc b/regression/cbmc-java/NondetInit2/test.desc
new file mode 100644
index 00000000000..d75e7538e9b
--- /dev/null
+++ b/regression/cbmc-java/NondetInit2/test.desc
@@ -0,0 +1,5 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+
diff --git a/regression/cbmc-java/NondetInit3/Subclass.class b/regression/cbmc-java/NondetInit3/Subclass.class
new file mode 100644
index 00000000000..ff6f1ffb001
Binary files /dev/null and b/regression/cbmc-java/NondetInit3/Subclass.class differ
diff --git a/regression/cbmc-java/NondetInit3/Test.class b/regression/cbmc-java/NondetInit3/Test.class
new file mode 100644
index 00000000000..d3b4a9378f8
Binary files /dev/null and b/regression/cbmc-java/NondetInit3/Test.class differ
diff --git a/regression/cbmc-java/NondetInit3/Test.java b/regression/cbmc-java/NondetInit3/Test.java
new file mode 100644
index 00000000000..edcea5419ca
--- /dev/null
+++ b/regression/cbmc-java/NondetInit3/Test.java
@@ -0,0 +1,22 @@
+import org.cprover.CProver;
+
+class Test {
+
+    int[] arr;
+
+    void cproverNondetInitialize() {
+        CProver.assume(arr != null && arr.length == 1);
+        // The following access should now be legal:
+        arr[0] = 100;
+    }
+
+    public static void main(Subclass nondetInput) {
+        // The condition enforced by cproverNondetInitialize should hold
+        // even though the parameter is a subtype of Test, not directly an
+        // instance of Test itself.
+        assert nondetInput.arr.length == 1;
+    }
+
+}
+
+class Subclass extends Test { }
diff --git a/regression/cbmc-java/NondetInit3/test.desc b/regression/cbmc-java/NondetInit3/test.desc
new file mode 100644
index 00000000000..d75e7538e9b
--- /dev/null
+++ b/regression/cbmc-java/NondetInit3/test.desc
@@ -0,0 +1,5 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index c44eaeb7edf..a1706cde435 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -1076,16 +1076,16 @@ void java_object_factoryt::gen_nondet_struct_init(
     }
   }
 
-  // If <class_identifier>.cproverValidate() can be found in the
+  // If <class_identifier>.cproverNondetInitialize() can be found in the
   // symbol table, we add a call:
   // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  // expr.cproverValidate();
+  // expr.cproverNondetInitialize();
   // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-  const irep_idt validate_method_name =
-    "java::" + id2string(class_identifier) + ".cproverNondetInitialize:()V";
+  const irep_idt init_method_name =
+    "java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V";
 
-  if(const auto func = symbol_table.lookup(validate_method_name))
+  if(const auto func = symbol_table.lookup(init_method_name))
   {
     const code_typet &type = to_code_type(func->type);
     code_function_callt fun_call;