Add test for static field of type Integer[]

This test falls into the same category as the tests from the previous
commit (static field with reference to primitive wrapper(s)) but is
closer to the example that was initially found for the bug (TG-8623).

Author: antlechner

jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.class

@@ -333,6 +333,14 @@ public static void testShortWrapperContainerFail() {
     assert shortWrapperContainer.shortField != (short)200;
   }
 
+  public static Integer[] integerWrapperArray = {1111};
+  public static void testIntegerWrapperArrayPass() {
+    assert integerWrapperArray.length == 1 && integerWrapperArray[0] == 1111;
+  }
+  public static void testIntegerWrapperArrayFail() {
+    assert integerWrapperArray.length != 1 || integerWrapperArray[0] != 1111;
+  }
+
   // Strings
   public static String stringField = Util.repeat("hello! ", 6);
   public static void testStringPass() {

jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.java

@@ -476,6 +476,12 @@
     "shortWrapperContainer":{
       "@type":"ContainerForShort",
       "shortField":200
+    },
+    "integerWrapperArray":{
+      "@type":"[Ljava.lang.Integer;",
+      "@items":[
+        1111
+      ]
     }
   },
   "OtherClass":{

jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testIntegerWrapperArrayFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_integer_wrapper_array_fail.desc

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testIntegerWrapperArrayPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--