Add regression tests for changes to JBMC enumeration support

Update regression tests

Author: Matthias Güdemann

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class

@@ -0,0 +1,16 @@
+package com.diffblue.regression;
+
+public class Foo {
+  public int foo(MyEnum e) {
+    if (e == null) return 0;
+    switch (e) {
+      case A:
+        return 1;
+      case B:
+        return 2;
+      case C:
+        return 3;
+    }
+    return 5;
+  }
+}

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class

@@ -0,0 +1,5 @@
+package com.diffblue.regression;
+
+enum MyEnum {
+ A, B, C, D;
+}

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java

@@ -0,0 +1,10 @@
+CORE
+com/diffblue/regression/Foo.class
+--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
+line 8.*SATISFIED
+line 10.*SATISFIED
+line 12.*SATISFIED
+line 14.*SATISFIED
+^EXIT=0$
+^SIGNAL=0$
+--

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.class

@@ -0,0 +1,8 @@
+package com.diffblue.regression;
+public class EnumIter {
+    int f() {
+        MyEnum[] a = MyEnum.values();
+        int num = a[2].ordinal() + a[3].ordinal();
+        return num ;
+    }
+}

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java

@@ -0,0 +1,5 @@
+package com.diffblue.regression;
+
+enum MyEnum {
+ A, B, C, D;
+}