diff --git a/regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc b/regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc
index d1ffab306f0..7849c7b2f9d 100644
--- a/regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc
+++ b/regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --no-simplify --no-propagation
 ^EXIT=10$
@@ -10,5 +10,6 @@ main.c
 --
 Check that the dynamic object property is nondet for uninitialized pointers. We
 use --no-simplify and --no-propagation to ensure that the case is not solved by
-the constant propagation and thus tests the constraint encoding. Recorded as
-ADA-526.
+the constant propagation and thus tests the constraint encoding. We expect
+that `__CPROVER_DYNAMIC_OBJECT` should be nondet for pointers that are neither
+null nor valid.
diff --git a/regression/cbmc-primitives/dynamic-object-02/test.desc b/regression/cbmc-primitives/dynamic-object-02/test.desc
index bf094c6f156..56e1062fb95 100644
--- a/regression/cbmc-primitives/dynamic-object-02/test.desc
+++ b/regression/cbmc-primitives/dynamic-object-02/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=10$
@@ -9,4 +9,3 @@ main.c
 ^warning: ignoring
 --
 Check that the dynamic object property is nondet for uninitialized pointers.
-Recorded as ADA-526.
diff --git a/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc b/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc
index af7f3f3d8b1..3a38f3cefcc 100644
--- a/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc
+++ b/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --no-simplify --no-propagation
 ^EXIT=10$
@@ -11,4 +11,3 @@ main.c
 Check that both positive and negative offsets can be chosen for uninitialized
 pointers. We use --no-simplify and --no-propagation to ensure that the case is
 not solved by the constant propagation and thus tests the constraint encoding.
-Recorded as ADA-528.
diff --git a/regression/cbmc-primitives/pointer-offset-01/test.desc b/regression/cbmc-primitives/pointer-offset-01/test.desc
index 32bf78ea0f5..332d5db8321 100644
--- a/regression/cbmc-primitives/pointer-offset-01/test.desc
+++ b/regression/cbmc-primitives/pointer-offset-01/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=10$
@@ -8,5 +8,10 @@ main.c
 --
 ^warning: ignoring
 --
-Check that both positive and negative offsets can be chosen for uninitialized
-pointers. Recorded as ADA-528.
+For uninitialised pointers, CBMC chooses a nondeterministic value (though no memory
+is allocated). Since the offset of pointers is signed, negative offsets should be
+able to be chosen (along with positive ones) non-deterministically.
+`__CPROVER_POINTER_OFFSET` is the CBMC primitive that gets the pointer offset
+from the base address of the object. This test guards this, and especially
+against the case where we could only observe some cases where offsets were only
+positive (in some CI configurations, for instance).