diff --git a/regression/cbmc/union12/main.c b/regression/cbmc/union12/main.c
new file mode 100644
index 00000000000..af0abe31f43
--- /dev/null
+++ b/regression/cbmc/union12/main.c
@@ -0,0 +1,23 @@
+typedef struct
+{
+  union {
+    int access[256];
+  };
+} S1;
+
+typedef struct
+{
+  int c;
+} S2;
+
+static S1(*const l[1]) = {((S1 *)((0x50000000UL) + 0x00000))};
+
+void main()
+{
+  __CPROVER_allocated_memory(0x50000000UL, sizeof(S1));
+  l[0]->access[0] = 0;
+  __CPROVER_assert(l[0]->access[0] == 0, "holds");
+  __CPROVER_assert(l[0]->access[1] == 0, "should fail");
+  __CPROVER_allocated_memory(0x40000000UL + 0x40000, sizeof(S2));
+  ((S2 *)((0x40000000UL) + 0x40000))->c = 0x0707;
+}
diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc
new file mode 100644
index 00000000000..82b3a34754a
--- /dev/null
+++ b/regression/cbmc/union12/test.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.2\] line 20 should fail: FAILURE$
+^\*\* 1 of 17 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Despite the large array inside the union, the test should complete within 10
+seconds. Simplify extractbits(concatenation(...)) is essential to make this
+possible. With 77236cc34 (Avoid nesting of ID_with/byte_update by rewriting
+byte_extract to use the root object) the test already is trivial, however.
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests
index 1c180cf7452..33f1b8a4417 100755
--- a/scripts/delete_failing_smt2_solver_tests
+++ b/scripts/delete_failing_smt2_solver_tests
@@ -94,6 +94,7 @@ rm struct7/test.desc
 rm struct9/test.desc
 rm trace-values/trace-values.desc
 rm trace_show_function_calls/test.desc
+rm union12/test.desc
 rm union6/test.desc
 rm union7/test.desc
 rm union9/test.desc
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 8e32c7064b6..e3ba6b1251a 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -992,12 +992,16 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
       alloc_disjuncts.push_back(and_exprt(lb_check, ub_check));
     }
 
-    const exprt allocs = disjunction(alloc_disjuncts);
+    const exprt in_bounds_of_some_explicit_allocation =
+      disjunction(alloc_disjuncts);
 
     if(flags.is_unknown() || flags.is_null())
     {
       conditions.push_back(conditiont(
-        or_exprt(allocs, not_exprt(null_pointer(address))), "pointer NULL"));
+        or_exprt(
+          in_bounds_of_some_explicit_allocation,
+          not_exprt(null_pointer(address))),
+        "pointer NULL"));
     }
 
     if(flags.is_unknown())
@@ -1010,21 +1014,28 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
     if(flags.is_uninitialized())
     {
       conditions.push_back(conditiont(
-        or_exprt(allocs, not_exprt(invalid_pointer(address))),
+        or_exprt(
+          in_bounds_of_some_explicit_allocation,
+          not_exprt(invalid_pointer(address))),
         "pointer uninitialized"));
     }
 
     if(flags.is_unknown() || flags.is_dynamic_heap())
     {
       conditions.push_back(conditiont(
-        not_exprt(deallocated(address, ns)),
+        or_exprt(
+          in_bounds_of_some_explicit_allocation,
+          not_exprt(deallocated(address, ns))),
         "deallocated dynamic object"));
     }
 
     if(flags.is_unknown() || flags.is_dynamic_local())
     {
       conditions.push_back(conditiont(
-        not_exprt(dead_object(address, ns)), "dead object"));
+        or_exprt(
+          in_bounds_of_some_explicit_allocation,
+          not_exprt(dead_object(address, ns))),
+        "dead object"));
     }
 
     if(flags.is_unknown() || flags.is_dynamic_heap())
@@ -1034,7 +1045,10 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         dynamic_object_upper_bound(address, ns, size));
 
       conditions.push_back(conditiont(
-        implies_exprt(malloc_object(address, ns), not_exprt(dynamic_bounds_violation)),
+        or_exprt(
+          in_bounds_of_some_explicit_allocation,
+          implies_exprt(
+            malloc_object(address, ns), not_exprt(dynamic_bounds_violation))),
         "pointer outside dynamic object bounds"));
     }
 
@@ -1047,14 +1061,19 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         object_upper_bound(address, ns, size));
 
       conditions.push_back(conditiont(
-        implies_exprt(not_exprt(dynamic_object(address)), not_exprt(object_bounds_violation)),
+        or_exprt(
+          in_bounds_of_some_explicit_allocation,
+          implies_exprt(
+            not_exprt(dynamic_object(address)),
+            not_exprt(object_bounds_violation))),
         "pointer outside object bounds"));
     }
 
     if(flags.is_unknown() || flags.is_integer_address())
     {
       conditions.push_back(conditiont(
-        implies_exprt(integer_address(address), allocs),
+        implies_exprt(
+          integer_address(address), in_bounds_of_some_explicit_allocation),
         "invalid integer address"));
     }