add three tests for unions in structs

These tests pass with the built-in solver but fail with three different
errors when using SMT.

Author: kroening

regression/cbmc/union/union_initialization.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct s
+{
+  union U
+  {
+    char c;
+    char b[2];
+  } u;
+} X;
+
+int main()
+{
+  // expected to fail
+  __CPROVER_assert(X.u.b[1] == 2, "should fail");
+}

regression/cbmc/union/union_initialization.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+union_initialization.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ should fail: FAILURE$
+^\*\* 1 of 1 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This fails when using the SMT backend with Z3 with the error message
+"invalid function/constant definition, sort mismatch".

regression/cbmc/union/union_member.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+struct s
+{
+  union U
+  {
+    char b[2];
+  };
+};
+
+int main()
+{
+  struct s X;
+  __CPROVER_assert(X.b[1] == 2, "should fail");
+}

regression/cbmc/union/union_member.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+union_member.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ should fail: FAILURE$
+^\*\* 1 of 1 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This fails when using the SMT backend with Z3 with the error message
+"select requires 1 arguments, but was provided with 2 arguments"

regression/cbmc/union/union_update.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct s
+{
+  char a;
+  union U
+  {
+    char c;
+    char b[2];
+  } u;
+} X = {1, 2};
+
+int main()
+{
+  __CPROVER_assert(X.u.b[1] == 123, "should fail");
+}

regression/cbmc/union/union_update.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+union_update.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ should fail: FAILURE$
+^\*\* 1 of 1 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This fails when using the SMT backend with Z3 with the error message
+"store expects the first argument sort to be an array".