add a test for a union with a large array

This test asserts that unions with large array members work.  This works
fine with the internal bitvector encoder, but the current SMT encoding
hangs.

Author: kroening

regression/cbmc/union/union_large_array.c

@@ -0,0 +1,15 @@
+#define LARGE 100000
+
+// This is to test the efficiency of unions that contain a large array.
+union U
+{
+  char large_array[LARGE];
+  int something_else;
+};
+
+int main()
+{
+  union U u;
+  u.something_else = 1234;
+  __CPROVER_assert(0, "should fail");
+}

regression/cbmc/union/union_large_array.desc

@@ -0,0 +1,11 @@
+CORE broken-smt-backend
+union_large_array.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ should fail: FAILURE$
+^\*\* 1 of 1 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--