Add a test checking array types in the trace

This checks that symbols no longer appear as size of array types.

Author: romainbrenguier

jbmc/regression/jbmc/trace_types/Test.class

@@ -0,0 +1,8 @@
+public class Test
+{
+  public void f(int i)
+  {
+    int[] array = new int[i];
+    array[10] = 4;
+  }
+}

jbmc/regression/jbmc/trace_types/Test.java

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.f --trace --json-ui --trace-json-extended
+// Enable multi-line checking
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+"type": \{\n\s*"id": "array",[^{]*\{[^}]*\},[\s\n]*"size": \{\n\s*"id": "constant"
+--
+"type": \{\n\s*"id": "array",[^{]*\{[^}]*\},[\s\n]*"size": \{\n\s*"id": "symbol"
+"type": \{\n\s*"id": "array",[^{]*\{[^}]*\},[\s\n]*"size": \{\n\s*"id": "nondet_symbol",
+--
+Check that symbols in array types in the trace, got replaced by actual values.