Add test for multiple array types in single method

regression/cbmc-java/lazyloading_multiple_array_types/A.java

@@ -0,0 +1,7 @@
+public class A {
+
+    public int f() {
+        return 1;
+    }
+
+}

regression/cbmc-java/lazyloading_multiple_array_types/B.java

@@ -0,0 +1,7 @@
+public class B {
+
+    public int g() {
+        return 5;
+    }
+
+}

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

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