diff --git a/regression/cbmc-primitives/dynamic-object-01/main.c b/regression/cbmc-primitives/dynamic-object-01/main.c
new file mode 100644
index 00000000000..76e2fbe71ea
--- /dev/null
+++ b/regression/cbmc-primitives/dynamic-object-01/main.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  free(p);
+
+  assert(__CPROVER_DYNAMIC_OBJECT(p));
+  assert(!__CPROVER_DYNAMIC_OBJECT(p));
+}
diff --git a/regression/cbmc-primitives/dynamic-object-01/test-no-cp.desc b/regression/cbmc-primitives/dynamic-object-01/test-no-cp.desc
new file mode 100644
index 00000000000..8c6f4dee17a
--- /dev/null
+++ b/regression/cbmc-primitives/dynamic-object-01/test-no-cp.desc
@@ -0,0 +1,14 @@
+FUTURE
+main.c
+--no-simplify --no-propagation
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+\[main.assertion.2\] line \d+ assertion !__CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+--
+^warning: ignoring
+--
+Check that the dynamic object property is havoc'd when dynamic objects are
+deallocated. 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.
diff --git a/regression/cbmc-primitives/dynamic-object-01/test.desc b/regression/cbmc-primitives/dynamic-object-01/test.desc
new file mode 100644
index 00000000000..11a72c113df
--- /dev/null
+++ b/regression/cbmc-primitives/dynamic-object-01/test.desc
@@ -0,0 +1,12 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+\[main.assertion.2\] line \d+ assertion !__CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+--
+^warning: ignoring
+--
+Check that the dynamic object property is havoc'd when dynamic objects are
+deallocated. Recorded as ADA-526.
diff --git a/regression/cbmc-primitives/dynamic-object-02/main.c b/regression/cbmc-primitives/dynamic-object-02/main.c
new file mode 100644
index 00000000000..fdd7d4a8142
--- /dev/null
+++ b/regression/cbmc-primitives/dynamic-object-02/main.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p;
+
+  assert(__CPROVER_DYNAMIC_OBJECT(p));
+  assert(!__CPROVER_DYNAMIC_OBJECT(p));
+}
diff --git a/regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc b/regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc
new file mode 100644
index 00000000000..d1ffab306f0
--- /dev/null
+++ b/regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc
@@ -0,0 +1,14 @@
+FUTURE
+main.c
+--no-simplify --no-propagation
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+\[main.assertion.2\] line \d+ assertion !__CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+--
+^warning: ignoring
+--
+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.
diff --git a/regression/cbmc-primitives/dynamic-object-02/test.desc b/regression/cbmc-primitives/dynamic-object-02/test.desc
new file mode 100644
index 00000000000..bf094c6f156
--- /dev/null
+++ b/regression/cbmc-primitives/dynamic-object-02/test.desc
@@ -0,0 +1,12 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+\[main.assertion.2\] line \d+ assertion !__CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+--
+^warning: ignoring
+--
+Check that the dynamic object property is nondet for uninitialized pointers.
+Recorded as ADA-526.
diff --git a/regression/cbmc-primitives/object-size-01/main.c b/regression/cbmc-primitives/object-size-01/main.c
new file mode 100644
index 00000000000..eab0c578834
--- /dev/null
+++ b/regression/cbmc-primitives/object-size-01/main.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  free(p);
+
+  assert(__CPROVER_OBJECT_SIZE(p) == 1);
+  assert(__CPROVER_OBJECT_SIZE(p) != 1);
+
+  {
+    char c;
+    p = &c;
+  }
+
+  assert(__CPROVER_OBJECT_SIZE(p) == 1);
+  assert(__CPROVER_OBJECT_SIZE(p) != 1);
+}
diff --git a/regression/cbmc-primitives/object-size-01/test-no-cp.desc b/regression/cbmc-primitives/object-size-01/test-no-cp.desc
new file mode 100644
index 00000000000..351ce83ca71
--- /dev/null
+++ b/regression/cbmc-primitives/object-size-01/test-no-cp.desc
@@ -0,0 +1,16 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) == 1: FAILURE
+\[main.assertion.2\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) != 1: FAILURE
+\[main.assertion.3\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) == 1: FAILURE
+\[main.assertion.4\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) != 1: FAILURE
+--
+^warning: ignoring
+--
+Check that object size is havoc'd when objects are deallocated. 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-527.
diff --git a/regression/cbmc-primitives/object-size-01/test.desc b/regression/cbmc-primitives/object-size-01/test.desc
new file mode 100644
index 00000000000..d4a46763ea9
--- /dev/null
+++ b/regression/cbmc-primitives/object-size-01/test.desc
@@ -0,0 +1,14 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) == 1: FAILURE
+\[main.assertion.2\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) != 1: FAILURE
+\[main.assertion.3\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) == 1: FAILURE
+\[main.assertion.4\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) != 1: FAILURE
+--
+^warning: ignoring
+--
+Check that object size is havoc'd when objects are deallocated. Recorded as
+ADA-527.
diff --git a/regression/cbmc-primitives/pointer-offset-01/main.c b/regression/cbmc-primitives/pointer-offset-01/main.c
new file mode 100644
index 00000000000..20369cf322f
--- /dev/null
+++ b/regression/cbmc-primitives/pointer-offset-01/main.c
@@ -0,0 +1,8 @@
+#include <assert.h>
+
+void main()
+{
+  char *p;
+  assert(__CPROVER_POINTER_OFFSET(p) >= 0);
+  assert(__CPROVER_POINTER_OFFSET(p) < 0);
+}
diff --git a/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc b/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc
new file mode 100644
index 00000000000..af7f3f3d8b1
--- /dev/null
+++ b/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc
@@ -0,0 +1,14 @@
+FUTURE
+main.c
+--no-simplify --no-propagation
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE
+\[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE
+--
+^warning: ignoring
+--
+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
new file mode 100644
index 00000000000..32bf78ea0f5
--- /dev/null
+++ b/regression/cbmc-primitives/pointer-offset-01/test.desc
@@ -0,0 +1,12 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE
+\[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE
+--
+^warning: ignoring
+--
+Check that both positive and negative offsets can be chosen for uninitialized
+pointers. Recorded as ADA-528.
diff --git a/regression/cbmc-primitives/same-object-01/main.c b/regression/cbmc-primitives/same-object-01/main.c
new file mode 100644
index 00000000000..363c1dd4c1c
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-01/main.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  assert(__CPROVER_POINTER_OBJECT(p) == 2);
+
+  assert(
+    __CPROVER_same_object(p, (char *)((size_t)2 << (sizeof(char *) * 8 - 8))));
+  assert(
+    !__CPROVER_same_object(p, (char *)((size_t)3 << (sizeof(char *) * 8 - 8))));
+}
diff --git a/regression/cbmc-primitives/same-object-01/test-no-cp.desc b/regression/cbmc-primitives/same-object-01/test-no-cp.desc
new file mode 100644
index 00000000000..97df364eec4
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-01/test-no-cp.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is true when given a pointer variable, and an
+integer address pointing to the same object. 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.
diff --git a/regression/cbmc-primitives/same-object-01/test.desc b/regression/cbmc-primitives/same-object-01/test.desc
new file mode 100644
index 00000000000..d32f40840c5
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-01/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is true when given a pointer variable, and an
+integer address pointing to the same object
diff --git a/regression/cbmc-primitives/same-object-02/main.c b/regression/cbmc-primitives/same-object-02/main.c
new file mode 100644
index 00000000000..eb9f4982cb7
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-02/main.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p1 = malloc(1);
+  char *p2 = malloc(1);
+
+  assert(!__CPROVER_same_object(p1, p2));
+}
diff --git a/regression/cbmc-primitives/same-object-02/test-no-cp.desc b/regression/cbmc-primitives/same-object-02/test-no-cp.desc
new file mode 100644
index 00000000000..1ac4fc36084
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-02/test-no-cp.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is false when given two pointers to different
+malloc'd objects. 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.
diff --git a/regression/cbmc-primitives/same-object-02/test.desc b/regression/cbmc-primitives/same-object-02/test.desc
new file mode 100644
index 00000000000..38d01968b72
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-02/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is false when given two pointers to different
+malloc'd objects
diff --git a/regression/cbmc-primitives/same-object-03/main.c b/regression/cbmc-primitives/same-object-03/main.c
new file mode 100644
index 00000000000..a46c4f285b6
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-03/main.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p1 = malloc(1);
+  free(p1);
+  char *p2 = malloc(1);
+
+  assert(!__CPROVER_same_object(p1, p2));
+}
diff --git a/regression/cbmc-primitives/same-object-03/test-no-cp.desc b/regression/cbmc-primitives/same-object-03/test-no-cp.desc
new file mode 100644
index 00000000000..1fb48dd8ec4
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-03/test-no-cp.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is false when given two pointers, with one
+of them being freed before the other is allocated. 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.
diff --git a/regression/cbmc-primitives/same-object-03/test.desc b/regression/cbmc-primitives/same-object-03/test.desc
new file mode 100644
index 00000000000..e6bfec93ba4
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-03/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is false when given two pointers, with one
+of them being freed before the other is allocated
diff --git a/regression/cbmc-primitives/same-object-04/main.c b/regression/cbmc-primitives/same-object-04/main.c
new file mode 100644
index 00000000000..3603f6ea512
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-04/main.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(10);
+  char *q = p + 5;
+
+  assert(__CPROVER_same_object(p, q));
+}
diff --git a/regression/cbmc-primitives/same-object-04/test-no-cp.desc b/regression/cbmc-primitives/same-object-04/test-no-cp.desc
new file mode 100644
index 00000000000..af320058c24
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-04/test-no-cp.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is true when given a pointer to the start of
+a memory block, and a pointer to within the memory block. 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.
diff --git a/regression/cbmc-primitives/same-object-04/test.desc b/regression/cbmc-primitives/same-object-04/test.desc
new file mode 100644
index 00000000000..04675e48d79
--- /dev/null
+++ b/regression/cbmc-primitives/same-object-04/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is true when given a pointer to the start of
+a memory block, and a pointer to within the memory block.