diff --git a/regression/cbmc/union10/union_list2.desc b/regression/cbmc/union10/union_list2.desc
index 7735057b70f..613581a5fc8 100644
--- a/regression/cbmc/union10/union_list2.desc
+++ b/regression/cbmc/union10/union_list2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 union_list2.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/union14/main.c b/regression/cbmc/union14/main.c
new file mode 100644
index 00000000000..f4e2f2b8f59
--- /dev/null
+++ b/regression/cbmc/union14/main.c
@@ -0,0 +1,47 @@
+struct fatptr
+{
+  int *data;
+  unsigned long int len;
+};
+
+struct slice
+{
+  int *data;
+  unsigned long int len;
+};
+
+union repr {
+  struct slice rust;
+  struct fatptr raw;
+};
+
+struct slice cast(int *data, unsigned long int len)
+{
+  struct fatptr x;
+  union repr z;
+  x.data = data;
+  x.len = len;
+  z.raw = x;
+  return z.rust;
+}
+
+struct fatptr cast2(int *data, unsigned long int len)
+{
+  struct slice w;
+  union repr z;
+  w.data = data;
+  w.len = len;
+  z.rust = w;
+  return z.raw;
+}
+
+int main()
+{
+  int x = 256;
+
+  struct slice z = cast(&x, 1);
+  struct fatptr z2 = cast2(&x, 1);
+
+  __CPROVER_assert(*z.data == 256, "test 1");
+  __CPROVER_assert(*z2.data == 256, "test 2");
+}
diff --git a/regression/cbmc/union14/test.desc b/regression/cbmc/union14/test.desc
new file mode 100644
index 00000000000..e6237ce4922
--- /dev/null
+++ b/regression/cbmc/union14/test.desc
@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Value sets do not properly track pointers through byte-extract operations. Thus
+derferencing yields __CPROVER_memory, which results in a spurious verification
+failure.