diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/A.class b/regression/cbmc-java/lazyloading_multiple_array_types/A.class
new file mode 100644
index 00000000000..a1388a0f223
Binary files /dev/null and b/regression/cbmc-java/lazyloading_multiple_array_types/A.class differ
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/A.java b/regression/cbmc-java/lazyloading_multiple_array_types/A.java
new file mode 100644
index 00000000000..71f8cf87a4f
--- /dev/null
+++ b/regression/cbmc-java/lazyloading_multiple_array_types/A.java
@@ -0,0 +1,7 @@
+public class A {
+
+    public int f() {
+        return 1;
+    }
+
+}
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/B.class b/regression/cbmc-java/lazyloading_multiple_array_types/B.class
new file mode 100644
index 00000000000..3fd3527e72a
Binary files /dev/null and b/regression/cbmc-java/lazyloading_multiple_array_types/B.class differ
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/B.java b/regression/cbmc-java/lazyloading_multiple_array_types/B.java
new file mode 100644
index 00000000000..0f49c7dba43
--- /dev/null
+++ b/regression/cbmc-java/lazyloading_multiple_array_types/B.java
@@ -0,0 +1,7 @@
+public class B {
+
+    public int g() {
+        return 5;
+    }
+
+}
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/Test.class b/regression/cbmc-java/lazyloading_multiple_array_types/Test.class
new file mode 100644
index 00000000000..6e6b1b68d70
Binary files /dev/null and b/regression/cbmc-java/lazyloading_multiple_array_types/Test.class differ
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/Test.java b/regression/cbmc-java/lazyloading_multiple_array_types/Test.java
new file mode 100644
index 00000000000..959c215df68
--- /dev/null
+++ b/regression/cbmc-java/lazyloading_multiple_array_types/Test.java
@@ -0,0 +1,17 @@
+public class Test {
+  
+  A[] arrayA;
+  B[] arrayB;
+
+  public static void check(Test t) {
+    if (t == null || t.arrayA == null || t.arrayB == null ||
+        t.arrayA.length == 0 || t.arrayB.length == 0 ||
+        t.arrayA[0] == null || t.arrayB[0] == null)
+      return;
+    int i = t.arrayA[0].f();
+    int j = t.arrayB[0].g();
+    int sum = i + j;
+    assert(sum == 6);
+  }
+
+}
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/test.desc b/regression/cbmc-java/lazyloading_multiple_array_types/test.desc
new file mode 100644
index 00000000000..f15d1291c02
--- /dev/null
+++ b/regression/cbmc-java/lazyloading_multiple_array_types/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--lazy-methods --verbosity 10 --function Test.check
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)I
+elaborate java::B\.g:\(\)I
+VERIFICATION SUCCESSFUL
diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp
index 12813caf12b..2aa62b01904 100644
--- a/src/java_bytecode/ci_lazy_methods.cpp
+++ b/src/java_bytecode/ci_lazy_methods.cpp
@@ -344,7 +344,10 @@ void ci_lazy_methodst::initialize_needed_classes_from_pointer(
   const symbol_typet &class_type=to_symbol_type(pointer_type.subtype());
   const auto &param_classid=class_type.get_identifier();
 
-  if(needed_lazy_methods.add_needed_class(param_classid))
+  // Note here: different arrays may have different element types, so we should
+  // explore again even if we've seen this classid before in the array case.
+  if(needed_lazy_methods.add_needed_class(param_classid) ||
+     is_java_array_tag(param_classid))
   {
     gather_field_types(pointer_type.subtype(), ns, needed_lazy_methods);
   }