diff --git a/regression/contracts-dfcc/test_aliasing_ensure/main.c b/regression/contracts-dfcc/test_aliasing_ensure/main.c
index 9b66c5589cd..d59bfe7deb1 100644
--- a/regression/contracts-dfcc/test_aliasing_ensure/main.c
+++ b/regression/contracts-dfcc/test_aliasing_ensure/main.c
@@ -1,35 +1,15 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
-int z;
-
-// clang-format off
-int foo(int *x, int *y)
-  __CPROVER_assigns(z, *x)
-  __CPROVER_requires(
-    __CPROVER_is_fresh(x, sizeof(int)) &&
-    *x > 0 &&
-    *x < 4)
-  __CPROVER_ensures(
-    __CPROVER_is_fresh(y, sizeof(int)) &&
-    !__CPROVER_is_fresh(x, sizeof(int)) &&
-    x != NULL &&
-    x != y &&
-    __CPROVER_return_value == *x + 5)
+int *foo()
+  // clang-format off
+  __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)))
 // clang-format on
 {
-  *x = *x + 4;
-  y = malloc(sizeof(*y));
-  *y = *x;
-  z = *y;
-  return (*x + 5);
+  int *ret = malloc(sizeof(int));
+  __CPROVER_assume(ret);
+  return ret;
 }
 
 int main()
 {
-  int n = 4;
-  n = foo(&n, &n);
-  assert(!(n < 4));
+  foo();
   return 0;
 }
diff --git a/regression/contracts-dfcc/test_aliasing_ensure/test.desc b/regression/contracts-dfcc/test_aliasing_ensure/test.desc
index 11f828e0e09..f4672b8a3ee 100644
--- a/regression/contracts-dfcc/test_aliasing_ensure/test.desc
+++ b/regression/contracts-dfcc/test_aliasing_ensure/test.desc
@@ -4,10 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
-\[foo.assigns.\d+\].*Check that \*x is assignable: SUCCESS
-\[foo.assigns.\d+\].*Check that \*y is assignable: SUCCESS
-\[foo.assigns.\d+\].*Check that z is assignable: SUCCESS
-\[main.assertion.\d+\].*assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c
new file mode 100644
index 00000000000..3e0f9019148
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c
@@ -0,0 +1,20 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(__CPROVER_pointer_equals(y, x) && __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc
new file mode 100644
index 00000000000..a9518be3f8e
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c
new file mode 100644
index 00000000000..d59373da733
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c
@@ -0,0 +1,20 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(__CPROVER_pointer_equals(y, x) || __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc
new file mode 100644
index 00000000000..fc07efa0e6c
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c
new file mode 100644
index 00000000000..1baed0c514f
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_pointer_in_range_dfcc(x, y, x) &&
+  __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc
new file mode 100644
index 00000000000..a9518be3f8e
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c
new file mode 100644
index 00000000000..7ff64a79922
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_pointer_in_range_dfcc(x, y, x) ||
+  __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc
new file mode 100644
index 00000000000..ce6d882dbfa
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that more than one predicate can be assumed on a same target as long at
+they don't hold at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/main.c
new file mode 100644
index 00000000000..1a4cb7173c7
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_pointer_in_range_dfcc(x, y, x) &&
+  __CPROVER_pointer_in_range_dfcc(x, y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/test.desc
new file mode 100644
index 00000000000..516be7ab02e
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.6] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming more than one pointer predicate on the same target pointer triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c
new file mode 100644
index 00000000000..c51b17dd142
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_pointer_in_range_dfcc(x, y, x) ||
+  __CPROVER_pointer_in_range_dfcc(x, y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc
new file mode 100644
index 00000000000..fc07efa0e6c
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c
new file mode 100644
index 00000000000..9ccae900abe
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c
@@ -0,0 +1,20 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) && __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc
new file mode 100644
index 00000000000..0f5932dd18d
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming more than one pointer predicate on the same target pointer triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c
new file mode 100644
index 00000000000..2a8f24a3e55
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c
@@ -0,0 +1,20 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) || __CPROVER_pointer_equals(y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc
new file mode 100644
index 00000000000..fc07efa0e6c
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c
new file mode 100644
index 00000000000..066174498c7
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_is_fresh(y, sizeof(int)) &&
+  __CPROVER_pointer_in_range_dfcc(x, y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc
new file mode 100644
index 00000000000..1c685d2a1fb
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c
new file mode 100644
index 00000000000..780bcd8e768
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_is_fresh(y, sizeof(int)) ||
+  __CPROVER_pointer_in_range_dfcc(x, y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1 || *x == 0)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc
new file mode 100644
index 00000000000..fc07efa0e6c
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c
new file mode 100644
index 00000000000..cc39fa82856
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c
@@ -0,0 +1,17 @@
+void foo(int *x)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(x, sizeof(int)) && __CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_assigns(*x)
+__CPROVER_ensures(*x == 0)
+// clang-format on
+{
+  *x = 0;
+}
+
+int main()
+{
+  int *x;
+  foo(x);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc
new file mode 100644
index 00000000000..64699f20363
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c
new file mode 100644
index 00000000000..e338a05dd25
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c
@@ -0,0 +1,17 @@
+void foo(int *x)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(x, sizeof(int)) || __CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_assigns(*x)
+__CPROVER_ensures(*x == 0)
+// clang-format on
+{
+  *x = 0;
+}
+
+int main()
+{
+  int *x;
+  foo(x);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc
new file mode 100644
index 00000000000..703a129c1b0
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc
@@ -0,0 +1,14 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.
+- `x` is fresh and inialized to 0
+- `y` is equal to `x`if select is true, or fresh otherwise
+- foo assigns y to 1
+- x is equal to 1 if select is true, 0 otherwise
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/main.c
new file mode 100644
index 00000000000..db9611a59f2
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/main.c
@@ -0,0 +1,21 @@
+void foo(int *x, int *y, int **z)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(z, sizeof(int*)))
+__CPROVER_requires(__CPROVER_pointer_equals(*z, x))
+__CPROVER_assigns(*z)
+__CPROVER_ensures(__CPROVER_pointer_equals(*z, y))
+// clang-format on
+{
+  *z = y;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  int **z;
+  foo(x, y, z);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/test.desc
new file mode 100644
index 00000000000..12ffdbea606
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that assuming different predicates on a same pointer is possible across pre and post conditions.
+Initially *z equals x, after the call *z equals y.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/main.c
new file mode 100644
index 00000000000..d878f006513
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/main.c
@@ -0,0 +1,32 @@
+void foo(int *x, int *y, int **z)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(z, sizeof(int*)))
+__CPROVER_requires(__CPROVER_pointer_equals(*z, x))
+__CPROVER_assigns(*z)
+__CPROVER_ensures(__CPROVER_pointer_equals(*z, y))
+// clang-format on
+{
+  *z = y;
+}
+
+void bar()
+  // clang-format off
+__CPROVER_requires(1)
+__CPROVER_assigns()
+__CPROVER_ensures(1)
+// clang-format on
+{
+  int x;
+  int y;
+  int *z = &x;
+  foo(&x, &y, &z);
+  assert(z == &y);
+}
+
+int main()
+{
+  bar();
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/test.desc
new file mode 100644
index 00000000000..0d7313a649c
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/test.desc
@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract bar --replace-call-with-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that assuming different predicates on a same pointer is possible across pre and post conditions.
+Initially *z equals x, after the call *z equals y.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c
new file mode 100644
index 00000000000..1a4cb7173c7
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c
@@ -0,0 +1,22 @@
+void foo(int *x, int *y)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(*x == 0)
+__CPROVER_requires(
+  __CPROVER_pointer_in_range_dfcc(x, y, x) &&
+  __CPROVER_pointer_in_range_dfcc(x, y, x))
+__CPROVER_assigns(*y)
+__CPROVER_ensures(*y == 1)
+__CPROVER_ensures(*x == 1)
+// clang-format on
+{
+  *y = 1;
+}
+
+int main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc
new file mode 100644
index 00000000000..1c685d2a1fb
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.
diff --git a/regression/contracts-dfcc/test_scalar_memory_enforce/main.c b/regression/contracts-dfcc/test_scalar_memory_enforce/main.c
index b22c93fe00f..ff6bbd8a739 100644
--- a/regression/contracts-dfcc/test_scalar_memory_enforce/main.c
+++ b/regression/contracts-dfcc/test_scalar_memory_enforce/main.c
@@ -21,7 +21,6 @@ int foo(int *x)
     ptr_ok(x))
   __CPROVER_ensures(
     !ptr_ok(x) &&
-    !__CPROVER_is_fresh(x, sizeof(int)) &&
     return_ok(__CPROVER_return_value, x))
 // clang-format on
 {
diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c
index 03c9abb1b3f..e3b3f7c4666 100644
--- a/src/ansi-c/library/cprover_contracts.c
+++ b/src/ansi-c/library/cprover_contracts.c
@@ -64,9 +64,28 @@ typedef struct
   void **elems;
 } __CPROVER_contracts_obj_set_t;
 
-/// \brief Type of pointers to \ref __CPROVER_contracts_car_set_t.
+/// \brief Type of pointers to \ref __CPROVER_contracts_obj_set_t.
 typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t;
 
+/// \brief Stores context information supporting the evaluation of pointer
+/// predicates in both assume and assert contexts for all predicates:
+/// pointer equals, pointer_in_range_dfcc, pointer_is_fresh, obeys_contract.
+typedef struct
+{
+  /// \brief Nondet variable ranging over the set of objects allocated
+  /// by __CPROVER_contracts_is_fresh. Used to check separation constraints
+  /// in __CPROVER_contracts_is_fresh.
+  void *fresh_ptr;
+  /// \brief Nondet variable ranging over the set of locations storing
+  /// pointers on which predicates were assumed/asserted. Used to ensure
+  /// that at most one predicate is assumed per pointer.
+  void **ptr_pred;
+} __CPROVER_contracts_ptr_pred_ctx_t;
+
+/// \brief Type of pointers to \ref __CPROVER_contracts_ptr_pred_ctx_t.
+typedef __CPROVER_contracts_ptr_pred_ctx_t
+  *__CPROVER_contracts_ptr_pred_ctx_ptr_t;
+
 /// \brief Runtime representation of a write set.
 typedef struct
 {
@@ -84,7 +103,7 @@ typedef struct
   __CPROVER_contracts_obj_set_t deallocated;
   /// \brief Pointer to object set supporting the is_fresh predicate checks
   /// (indexed mode)
-  __CPROVER_contracts_obj_set_ptr_t linked_is_fresh;
+  __CPROVER_contracts_ptr_pred_ctx_ptr_t linked_ptr_pred_ctx;
   /// \brief Object set recording the is_fresh allocations in post conditions
   __CPROVER_contracts_obj_set_ptr_t linked_allocated;
   /// \brief Object set recording the deallocations (used by was_freed)
@@ -393,6 +412,27 @@ __CPROVER_HIDE:;
   return set->elems[object_id] == ptr;
 }
 
+/// \brief Resets the nondet tracker for pointer predicates in \p set.
+/// Invoked between requires and ensures clauses evaluation to allow ensures
+/// clauses to establish different pointer predicates on the same pointers.
+void __CPROVER_contracts_ptr_pred_ctx_init(
+  __CPROVER_contracts_ptr_pred_ctx_ptr_t set)
+{
+__CPROVER_HIDE:;
+  set->fresh_ptr = (void *)0;
+  set->ptr_pred = (void **)0;
+}
+
+/// \brief Resets the nondet tracker for pointer predicates in \p set.
+/// Invoked right between requires and ensures clauses to allow ensures clauses
+/// to establish a different pointer predicates on the same pointers.
+void __CPROVER_contracts_ptr_pred_ctx_reset(
+  __CPROVER_contracts_ptr_pred_ctx_ptr_t set)
+{
+__CPROVER_HIDE:;
+  set->ptr_pred = (void **)0;
+}
+
 /// \brief Initialises a \ref __CPROVER_contracts_write_set_t object.
 /// \param[inout] set Pointer to the object to initialise
 /// \param[in] contract_assigns_size Max size of the assigns clause
@@ -434,7 +474,7 @@ __CPROVER_HIDE:;
     &(set->contract_frees_append), contract_frees_size);
   __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->allocated));
   __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->deallocated));
-  set->linked_is_fresh = 0;
+  set->linked_ptr_pred_ctx = 0;
   set->linked_allocated = 0;
   set->linked_deallocated = 0;
   set->assume_requires_ctx = assume_requires_ctx;
@@ -473,8 +513,8 @@ __CPROVER_HIDE:;
   __CPROVER_deallocate(set->contract_frees_append.elems);
   __CPROVER_deallocate(set->allocated.elems);
   __CPROVER_deallocate(set->deallocated.elems);
-  // do not free set->linked_is_fresh->elems or set->deallocated_linked->elems
-  // since they are owned by someone else.
+  // do not free set->linked_ptr_pred_ctx->elems or
+  // set->deallocated_linked->elems since they are owned by someone else.
 }
 
 /// \brief Inserts a snapshot of the range starting at \p ptr of size \p size
@@ -542,9 +582,6 @@ void __CPROVER_contracts_write_set_insert_object_from(
 /// \brief Inserts a snapshot of the range of bytes starting at \p ptr of
 /// \p size bytes in \p set->contact_assigns at index \p idx.
 ///
-/// - The start address is `ptr`
-/// - The size in bytes is `size`
-///
 /// \param[inout] set The set to update
 /// \param[in] idx Insertion index
 /// \param[in] ptr Pointer to the start of the range
@@ -567,10 +604,8 @@ void __CPROVER_contracts_write_set_add_freeable(
   void *ptr)
 {
 __CPROVER_HIDE:;
-  // we don't check yet that the pointer satisfies
-  // the __CPROVER_contracts_is_freeable as precondition.
-  // preconditions will be checked if there is an actual attempt
-  // to free the pointer.
+  // Preconditions will be checked if there is an actual attempt
+  // to free the pointer, don't check preemptively.
 
   // store pointer
   __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
@@ -1060,23 +1095,23 @@ __CPROVER_HIDE:;
 }
 
 /// \brief Links \p is_fresh_set to
-/// \p write_set->linked_is_fresh so that the is_fresh predicates
-/// can be evaluated in requires and ensures clauses.
-void __CPROVER_contracts_link_is_fresh(
+/// \p write_set->linked_ptr_pred_ctx to share evaluation context between
+/// requires and ensures clauses for separation checks.
+void __CPROVER_contracts_link_ptr_pred_ctx(
   __CPROVER_contracts_write_set_ptr_t write_set,
-  __CPROVER_contracts_obj_set_ptr_t is_fresh_set)
+  __CPROVER_contracts_ptr_pred_ctx_ptr_t ptr_pred_ctx)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_DFCC_DEBUG_LIB
   __CPROVER_assert(write_set != 0, "write_set not NULL");
 #endif
-  if((is_fresh_set != 0))
+  if((ptr_pred_ctx != 0))
   {
-    write_set->linked_is_fresh = is_fresh_set;
+    write_set->linked_ptr_pred_ctx = ptr_pred_ctx;
   }
   else
   {
-    write_set->linked_is_fresh = 0;
+    write_set->linked_ptr_pred_ctx = 0;
   }
 }
 
@@ -1205,7 +1240,15 @@ __CPROVER_HIDE:;
     }
     __CPROVER_assert(
       (ptr2 == 0) || __CPROVER_r_ok(ptr2, 0),
-      "pointer_equals is only called with valid pointers");
+      "__CPROVER_pointer_equals is only called with valid pointers");
+    __CPROVER_assert(
+      write_set->linked_ptr_pred_ctx->ptr_pred != ptr1,
+      "__CPROVER_pointer_equals does not conflict with other pointer "
+      "predicate");
+    write_set->linked_ptr_pred_ctx->ptr_pred =
+      __VERIFIER_nondet___CPROVER_bool()
+        ? ptr1
+        : write_set->linked_ptr_pred_ctx->ptr_pred;
     *ptr1 = ptr2;
     return 1;
   }
@@ -1214,35 +1257,41 @@ __CPROVER_HIDE:;
     void *derefd = *ptr1;
     __CPROVER_assert(
       (derefd == 0) || __CPROVER_r_ok(derefd, 0),
-      "pointer_equals is only called with valid pointers");
+      "__CPROVER_pointer_equals is only called with valid pointers");
     __CPROVER_assert(
       (ptr2 == 0) || __CPROVER_r_ok(ptr2, 0),
-      "pointer_equals is only called with valid pointers");
-    return derefd == ptr2;
+      "__CPROVER_pointer_equals is only called with valid pointers");
+    if(derefd != ptr2)
+    {
+      return 0;
+    }
+    __CPROVER_assert(
+      write_set->linked_ptr_pred_ctx->ptr_pred != ptr1,
+      "__CPROVER_pointer_equals does not conflict with other pointer "
+      "predicate");
+    write_set->linked_ptr_pred_ctx->ptr_pred =
+      __VERIFIER_nondet___CPROVER_bool()
+        ? ptr1
+        : write_set->linked_ptr_pred_ctx->ptr_pred;
+    return 1;
   }
 }
 
 /// \brief Implementation of the `is_fresh` front-end predicate.
 ///
-/// The behaviour depends on the boolean flags carried by \p write_set
-/// which reflect the invocation context: checking vs. replacing a contract,
-/// in a requires or an ensures clause context.
 /// \param elem Pointer to the target pointer of the check
-/// \param size Size to check for
+/// \param size Size to check
 /// \param may_fail Allow predicate to fail in assume mode
-/// \param write_set Write set in which seen/allocated objects are recorded;
+/// \param write_set Write set (carries assert/assume requires/ensures context
+///   flags, sets to allocated/seen objects for separation checks)
 ///
 /// \details The behaviour is as follows:
-/// - When \p set->assume_requires_ctx is `true`, the predicate allocates a new
-/// object, records the object in \p set->linked_is_fresh, updates \p *elem to
-/// point to the fresh object and returns `true`;
-/// - When \p set->assume_ensures_ctx is `true`, the predicate allocates a new
-/// object, records the object in \p set->linked_allocated, updates \p *elem
-/// to point to the fresh object and returns `true`;
-/// - When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`,
-/// the predicate first computes wether \p *elem is in \p set->linked_is_fresh
-/// and returns false if it is. Otherwise it records the object in
-/// \p set->linked_is_fresh and returns the value of r_ok(*elem, size).
+/// - In assume contexts, returns false if another pointer predicate is already
+///  assumed, otherwise, allocates a fresh object, mark *elem and elem as seen
+///  in the write set.
+/// - In assert contexts, returns false if another pointer predicate is already
+///  succesfully asserted, otherwise checks separation and size, mark *elem and
+/// elem as seen in the write set.
 __CPROVER_bool __CPROVER_contracts_is_fresh(
   void **elem,
   __CPROVER_size_t size,
@@ -1250,19 +1299,7 @@ __CPROVER_bool __CPROVER_contracts_is_fresh(
   __CPROVER_contracts_write_set_ptr_t write_set)
 {
 __CPROVER_HIDE:;
-  __CPROVER_assert(
-    (write_set != 0) & ((write_set->assume_requires_ctx == 1) |
-                        (write_set->assert_requires_ctx == 1) |
-                        (write_set->assume_ensures_ctx == 1) |
-                        (write_set->assert_ensures_ctx == 1)),
-    "__CPROVER_is_fresh is used only in requires or ensures clauses");
-#ifdef __CPROVER_DFCC_DEBUG_LIB
-  __CPROVER_assert(
-    __CPROVER_rw_ok(write_set, sizeof(__CPROVER_contracts_write_set_t)),
-    "set readable");
-  __CPROVER_assert(
-    write_set->linked_is_fresh, "set->linked_is_fresh is not NULL");
-#endif
+
   if(write_set->assume_requires_ctx)
   {
 #ifdef __CPROVER_DFCC_DEBUG_LIB
@@ -1299,32 +1336,28 @@ __CPROVER_HIDE:;
       __CPROVER_contracts_make_invalid_pointer(elem);
       return 0;
     }
-
     void *ptr = __CPROVER_allocate(size, 0);
     *elem = ptr;
+    __CPROVER_assert(
+      write_set->linked_ptr_pred_ctx->ptr_pred != elem,
+      "__CPROVER_is_fresh does not conflict with other pointer predicate");
+    write_set->linked_ptr_pred_ctx->ptr_pred =
+      __VERIFIER_nondet___CPROVER_bool()
+        ? elem
+        : write_set->linked_ptr_pred_ctx->ptr_pred;
+    write_set->linked_ptr_pred_ctx->fresh_ptr =
+      __VERIFIER_nondet___CPROVER_bool()
+        ? ptr
+        : write_set->linked_ptr_pred_ctx->fresh_ptr;
 
     // record the object size for non-determistic bounds checking
     __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
     __CPROVER_malloc_is_new_array =
       record_malloc ? 0 : __CPROVER_malloc_is_new_array;
-
     // do not detect memory leaks when assuming a precondition of a contract
     // for contract checking
     // __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
     // __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
-
-#ifdef __CPROVER_DFCC_DEBUG_LIB
-    // manually inlined below
-    __CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr);
-#else
-    __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
-    write_set->linked_is_fresh->nof_elems =
-      (write_set->linked_is_fresh->elems[object_id] != 0)
-        ? write_set->linked_is_fresh->nof_elems
-        : write_set->linked_is_fresh->nof_elems + 1;
-    write_set->linked_is_fresh->elems[object_id] = ptr;
-    write_set->linked_is_fresh->is_empty = 0;
-#endif
     return 1;
   }
   else if(write_set->assume_ensures_ctx)
@@ -1362,6 +1395,17 @@ __CPROVER_HIDE:;
 
     void *ptr = __CPROVER_allocate(size, 0);
     *elem = ptr;
+    __CPROVER_assert(
+      write_set->linked_ptr_pred_ctx->ptr_pred != elem,
+      "__CPROVER_is_fresh does not conflict with other pointer predicate");
+    write_set->linked_ptr_pred_ctx->ptr_pred =
+      __VERIFIER_nondet___CPROVER_bool()
+        ? elem
+        : write_set->linked_ptr_pred_ctx->ptr_pred;
+    write_set->linked_ptr_pred_ctx->fresh_ptr =
+      __VERIFIER_nondet___CPROVER_bool()
+        ? ptr
+        : write_set->linked_ptr_pred_ctx->fresh_ptr;
 
     // record the object size for non-determistic bounds checking
     __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
@@ -1395,34 +1439,26 @@ __CPROVER_HIDE:;
         (write_set->assume_ensures_ctx == 0),
       "only one context flag at a time");
 #endif
-    __CPROVER_contracts_obj_set_ptr_t seen = write_set->linked_is_fresh;
     void *ptr = *elem;
-    // null pointers or already seen pointers are not fresh
-#ifdef __CPROVER_DFCC_DEBUG_LIB
-    // manually inlined below
-    if((ptr == 0) || (__CPROVER_contracts_obj_set_contains(seen, ptr)))
-      return 0;
-#else
-    if(ptr == 0)
-      return 0;
-
-    __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
-
-    if(seen->elems[object_id] != 0)
-      return 0;
-#endif
-
-#ifdef __CPROVER_DFCC_DEBUG_LIB
-    // manually inlined below
-    __CPROVER_contracts_obj_set_add(seen, ptr);
-#else
-    seen->nof_elems =
-      (seen->elems[object_id] != 0) ? seen->nof_elems : seen->nof_elems + 1;
-    seen->elems[object_id] = ptr;
-    seen->is_empty = 0;
-#endif
-    // check size
-    return __CPROVER_r_ok(ptr, size);
+    if(
+      ptr != (void *)0 &&
+      !__CPROVER_same_object(write_set->linked_ptr_pred_ctx->fresh_ptr, ptr) &&
+      __CPROVER_r_ok(ptr, size))
+    {
+      __CPROVER_assert(
+        write_set->linked_ptr_pred_ctx->ptr_pred != elem,
+        "__CPROVER_is_fresh does not conflict with other pointer predicate");
+      write_set->linked_ptr_pred_ctx->ptr_pred =
+        __VERIFIER_nondet___CPROVER_bool()
+          ? elem
+          : write_set->linked_ptr_pred_ctx->ptr_pred;
+      write_set->linked_ptr_pred_ctx->fresh_ptr =
+        __VERIFIER_nondet___CPROVER_bool()
+          ? ptr
+          : write_set->linked_ptr_pred_ctx->fresh_ptr;
+      return 1;
+    }
+    return 0;
   }
   else
   {
@@ -1491,13 +1527,37 @@ __CPROVER_HIDE:;
     __CPROVER_size_t max_offset = ub_offset - lb_offset;
     __CPROVER_assume(offset <= max_offset);
     *ptr = (char *)lb + offset;
+    __CPROVER_assert(
+      write_set->linked_ptr_pred_ctx->ptr_pred != ptr,
+      "__CPROVER_pointer_in_range_dfcc does not conflict with other pointer "
+      "predicate");
+    write_set->linked_ptr_pred_ctx->ptr_pred =
+      __VERIFIER_nondet___CPROVER_bool()
+        ? ptr
+        : write_set->linked_ptr_pred_ctx->ptr_pred;
     return 1;
   }
   else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
   {
     __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(*ptr);
-    return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
-           offset <= ub_offset;
+    if(
+      __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
+      offset <= ub_offset)
+    {
+      __CPROVER_assert(
+        write_set->linked_ptr_pred_ctx->ptr_pred != ptr,
+        "__CPROVER_pointer_in_range_dfcc does not conflict with other "
+        "predicate");
+      write_set->linked_ptr_pred_ctx->ptr_pred =
+        __VERIFIER_nondet___CPROVER_bool()
+          ? ptr
+          : write_set->linked_ptr_pred_ctx->ptr_pred;
+      return 1;
+    }
+    else
+    {
+      return 0;
+    }
   }
 }
 
@@ -1669,6 +1729,14 @@ __CPROVER_HIDE:;
     if(may_fail && __VERIFIER_nondet___CPROVER_bool())
       return 0;
 
+    __CPROVER_assert(
+      set->linked_ptr_pred_ctx->ptr_pred != (void **)function_pointer,
+      "__CPROVER_obeys_contract does not conflict with other pointer "
+      "predicate");
+    set->linked_ptr_pred_ctx->ptr_pred = __VERIFIER_nondet___CPROVER_bool()
+                                           ? (void **)function_pointer
+                                           : set->linked_ptr_pred_ctx->ptr_pred;
+
     // must hold, assign the function pointer to the contract function
     *function_pointer = contract;
     return 1;
@@ -1676,7 +1744,18 @@ __CPROVER_HIDE:;
   else
   {
     // in assumption contexts, the pointer gets checked for equality
-    return *function_pointer == contract;
+    if(*function_pointer == contract)
+    {
+      __CPROVER_assert(
+        set->linked_ptr_pred_ctx->ptr_pred != (void **)function_pointer,
+        "__CPROVER_obeys_contract does not conflict with other pointer "
+        "predicate");
+      set->linked_ptr_pred_ctx->ptr_pred =
+        __VERIFIER_nondet___CPROVER_bool() ? (void **)function_pointer
+                                           : set->linked_ptr_pred_ctx->ptr_pred;
+      return 1;
+    }
+    return 0;
   }
 }
 #endif // __CPROVER_contracts_library_defined
diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md
index f1456324578..6b0b4f225c5 100644
--- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md
+++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md
@@ -112,8 +112,8 @@ typedef struct __CPROVER_contracts_write_set_t
   // Set of objects deallocated by the function under analysis (indexed mode)
   __CPROVER_contracts_obj_set_t deallocated;
 
-  // Object set supporting the is_fresh predicate checks (indexed mode)
-  __CPROVER_contracts_obj_set_ptr_t linked_is_fresh;
+  // Object set supporting the pointer predicate checks
+  __CPROVER_contracts_ptr_pred_ctx_ptr_t linked_ptr_pred_ctx;
 
   // Object set recording the is_fresh allocations in post conditions
   // (replacement mode only)
diff --git a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md
index e2c526bd840..c0369b27f0e 100644
--- a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md
+++ b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md
@@ -4,252 +4,170 @@ Back to @ref contracts-user
 
 @tableofcontents
 
-The built-in and user-defined predicates discussed in this section are meant to
-let users describe the shape of the memory accessed through pointers in
-_requires clauses_ and _ensures clauses_. Attempting to call these predicates
-outside of a requires or ensures clause context will result in a verification
-error.
+The built-in predicates discussed in this section are used to describe pointer
+properties in _requires clauses_ and _ensures clauses_.
 
-## The __CPROVER_pointer_equals predicate
-### Syntax
-
-```c
-bool __CPROVER_pointer_equals(void *p, void *q);
-```
-This predicate can only be used in ensures and requires clauses and checks for
-pointer validity and equality.
-
-#### Parameters
-
-`__CPROVER_pointer_equals` takes two pointers as arguments.
+At a basic level the predicates allow to specify pointers to fresh objects
+(i.e. allocated and distinct, `__CPROVER_is_fresh(p, size)`), of aliased pointers
+(`__CPROVER_pointer_equals(p, q)`), or pointers ranging over pointer intervals
+(`__CPROVER_pointer_in_range_dfcc(lb, p, ub)`).
 
-#### Return Value
+They can only be used in the context of a requires and ensures clauses, any
+attempt to call these predicates outside of a requires or ensures clause will
+result in a verification error.
 
-It returns a `bool` value:
-- `true` iff pointers are both null or valid and are equal,
-- `false` otherwise.
+Pointer predicates can be used with conjunctions, implications or disjunctions
+to describe richer data structures where some parts are only conditionally
+allocated, but requires and ensures clauses must not attempt to establish more
+than one predicate at the same time for a same pointer.
 
-### Semantics
+One can build their own pointer predicates using these built-in predicates,
+to describe (bounded) linked data structures such as buffers, lists, etc.
 
-#### Enforcement
+## The __CPROVER_pointer_equals predicate
 
-When checking a contract using `--enforce-contract foo`:
-- used in a _requires_ clause, the predicate will check that `ptr2` is always
-  either null or valid, and it will make `ptr1` equal to `ptr2`.
-  This results in a state resulting in a state where both pointers are either
-  null or valid and equal;
-- used in an _ensures_ clause it will check that memory both pointers are always
-  either null or valid and equal.
+This predicate checks for pointer validity and equality.
 
-#### Replacement
+```c
+bool __CPROVER_pointer_equals(void *p, void *q);
+```
 
-When checking a contract using `--replace-call-with-contract foo`, we get the
-dual behaviour:
-- used in a _requires_ clause it will check that memory both pointers are always
-  either null or valid and equal,
-- used in an _ensures_ clause, the predicate will check that `ptr2` is always
-  either null or valid, and it will make `ptr1` equal to `ptr2`.
-  This results in a state resulting in a state where both pointers are either
-  null or valid and equal.
+This predicate checks for pointer validity and equality.
+
+It returns:
+- `true` if and only if:
+  -  `p` is either `NULL` or valid,
+  -  `q` is either `NULL` of valid,
+  -  `p` is equal to `q`.
+
+When checking a function against a contract (`--enforce-contract`):
+- in a _requires_ clause, the predicate will check that `q` is always
+  either `NULL` or valid, and it will assign `p` with `q`. This results in a state
+  where both pointers are either `NULL` or valid and are equal;
+- used in an _ensures_ clause it will check that both `p` and `q` are either
+  NULL or valid, and that `p == q`.
+
+When replacing a function call by a contract (`--replace-call-with-contract`):
+we get the dual behaviour:
+- used in a _requires_ clause it will check that both `p` and `q` are either
+  NULL or valid, and that `p == q`.
+- in an _ensures clause, the predicate will check that `q` is always
+  either `NULL` or valid, and it will assign `p` with `q`. This results in a state
+  where both pointers are either `NULL` or valid and are equal;
 
 ## The __CPROVER_is_fresh predicate
-### Syntax
+
+The predicate `__CPROVER_is_fresh `  takes a pointer `p` and an allocation
+size `size` and checks pointer validity and separation with other fresh pointers.
 
 ```c
 bool __CPROVER_is_fresh(void *p, size_t size);
 ```
 
-To specify memory footprint we use a special function called `__CPROVER_is_fresh `.
-The meaning of `__CPROVER_is_fresh` is that we are borrowing a pointer from the
-external environment (in a precondition), or returning it to the calling context
-(in a postcondition).
-
-#### Parameters
+The predicate `__CPROVER_is_fresh(p, n)` holds when `p` points into a valid
+object with at least `n` bytes available after the pointer, and the object
+pointed to by `p` is distinct from all other objects pointed to in other
+`__CPROVER_is_fresh(q, m)` found in the requires and ensures clauses.
+
+When checking a function against a contract (`--enforce-contract`):
+- `__CPROVER_is_fresh` in the `requires` clause works like a nondeterministic
+  `p = malloc(size)` (separation is assured by construction);
+- `__CPROVER_is_fresh` in the `ensures` clause checks pointer validity and
+  separation against other `__CPROVER_is_fresh` occurrences in the `requires`
+  clause and the `ensures` clause.
+
+When replacing a function call by a contract (`--replace-call-with-contract`):
+- `__CPROVER_is_fresh` in the `requires` clause checks pointer validity and
+  separation against other `__CPROVER_is_fresh` occurrences in the `requires`
+  clause;
+- `__CPROVER_is_fresh` in the `ensures` clause works like a nondeterministic
+  `p = malloc(size)` (separation is assured by construction);
 
-`__CPROVER_is_fresh` takes two arguments: a pointer and an allocation size.
-The first argument is the pointer to be checked for "freshness" (i.e., not previously
-allocated), and the second is the expected size **in bytes** for the memory
-available at the pointer.
-
-#### Return Value
-
-It returns a `bool` value, indicating whether the pointer is fresh.
-
-### Semantics
+## The __CPROVER_pointer_in_range_dfcc predicate
+### Syntax
 
-To illustrate the semantics for `__CPROVER_is_fresh`, consider the following
-implementation of `sum` function.
+This predicate holds if pointers `lb`, `p` and `ub` are valid pointers, pointing
+within the same object and the condition `lb <= p && p <= ub` holds.
 
 ```c
-int *err_signal; // Global variable
-
-void sum(const uint32_t a, const uint32_t b, uint32_t* out)
-__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out)))
-__CPROVER_ensures(__CPROVER_is_fresh(err_signal, sizeof(*err_signal)))
-__CPROVER_assigns(*out, err_signal)
-{
-  const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
-  err_signal = malloc(sizeof(*err_signal));
-  if (!err_signal) return;
-  if (result > UINT32_MAX) *err_signal = FAILURE;
-  *out = (uint32_t) result;
-  *err_signal = SUCCESS;
-}
+bool __CPROVER_pointer_in_range_dfcc(void *lb, void *p, void *ub);
 ```
 
-#### Enforcement
-
-When checking the contract abstracts a function a `__CPROVER_is_fresh`
-in a _requires_ clause will cause fresh memory to be allocated.
-In an _ensures_ clause it will check that memory was freshly allocated.
-
-```c
-int *err_signal; // Global variable
-
-int __CPROVER_contracts_original_sum(const uint32_t a, const uint32_t b, uint32_t* out)
-{
-  const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
-  err_signal = malloc(sizeof(*err_signal));
-  if (!err_signal) return;
-  if (result > UINT32_MAX) *err_signal = FAILURE;
-  *out = (uint32_t) result;
-  *err_signal = SUCCESS;
-}
-
-/* Function Contract Enforcement */
-int sum(const uint32_t a, const uint32_t b, uint32_t* out)
+When checking a function against a contract (`--enforce-contract`):
+- In the `requires` clause, `__CPROVER_pointer_in_range_dfcc` checks that `lb`
+  and `ub` are valid and point into the same object, and nondeterministically
+  assigns `p` to a nondet pointer between `lb` and `ub`;
+- In the `ensures` clause, `__CPROVER_pointer_in_range_dfcc` checks that `lb`
+  and `ub` are valid and point into the same object, that `p` is between `lb`
+  and `ub`;
+
+When replacing a function call by a contract (`--replace-call-with-contract`):
+- In the `requires` clause, `__CPROVER_pointer_in_range_dfcc` checks that `lb`
+  and `ub` are valid and point into the same object, that `p` is between `lb`
+  and `ub`;
+- In the `ensures` clause, `__CPROVER_pointer_in_range_dfcc` checks that `lb`
+  and `ub` are valid and point into the same object, and nondeterministically
+  assigns `p` to a nondet pointer between `lb` and `ub`;
+
+## Using memory predicates in disjunctions
+
+It is possible to use memory predicates in disjunctions to describe alternatives.
+
+For instance, to specify a conditionally allocated pointer, the implication
+ `==>` operator can be used.
+
+The `array` pointer is only valid when len is in some bounds, otherwise nothing
+is assumed about `array` and the pointer is considered _invalid_, i.e. any
+attempt to use it by the program under verification will result in an error.
+
+```C
+int foo(int *array, size_t len)
+__CPROVER_requires(
+  (len < INT_MAX/sizeof(int) && len > 0)
+      ==> __CPROVER_is_fresh(array, len*sizeof(int)))
 {
-  __CPROVER_assume(__CPROVER_is_fresh(out, sizeof(*out))); // Assumes out is freshly allocated
-  int return_value_sum = __CPROVER_contracts_original_sum(a, b, out);
-  __CPROVER_assert(__CPROVER_is_fresh(err_signal, sizeof(*err_signal)), "Check ensures clause");
-  return return_value_sum;
+   ...
 }
 ```
 
-#### Replacement
-
-In our example, consider that a function `foo` may call `sum`.
-
-```c
-int *err_signal; // Global variable
-
-int foo()
+In this other example, the function takes two pointers `a` and `b` and a
+and sets `*out` to the longest one:
+
+```C
+void foo(int *a, size_t len_a, int *b, size_t len_b, int **out)
+__CPROVER_requires(__CPROVER_is_fresh(a, len_a * sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(b, len_b * sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(int *)))
+__CPROVER_assigns(*out)
+__CPROVER_requires(len_a >= len_b ==> __CPROVER_pointer_equals(*out, a))
+__CPROVER_requires(len_a < len_b ==> __CPROVER_pointer_equals(*out, b))
 {
-  uint32_t a;
-  uint32_t b;
-  uint32_t out;
-  sum(a, b, &out);
-  return *err_signal;
+   ...
 }
 ```
 
-When using a contract as an abstraction in place of a call to the function
-a `__CPROVER_is_fresh` in a _requires_ clause will check that the argument
-supplied is fresh and `__CPROVER_is_fresh` in an _ensures_ clause will
-result in a fresh malloc.
-
-```c
-int *err_signal; // Global variable
-
-int foo()
+In last other example, the function takes two pointers `a` and `b` and a
+and sets `*out` to either `a` or `b`, nondeterministically:
+
+```C
+void foo(int *a, int *b, int **out)
+__CPROVER_requires(__CPROVER_is_fresh(a, 1)) // at least one byte
+__CPROVER_requires(__CPROVER_is_fresh(b, 1))
+__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(int *)))
+__CPROVER_assigns(*out)
+__CPROVER_requires(
+  __CPROVER_pointer_equals(*out, a) || __CPROVER_pointer_equals(*out, b))
 {
-  uint32_t a;
-  uint32_t b;
-  uint32_t out;
-
-  /* Function Contract Replacement */
-  /* Precondition */
-  __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause");
-
-  /* Writable Set */
-  *(&out) = nondet_uint32_t();
-  err_signal = nondet_int_pointer();
-
-  /* Postconditions */
-  __CPROVER_assume(__CPROVER_is_fresh(err_signal, sizeof(*err_signal))); // Assumes out is allocated
-
-  return *err_signal;
+   ...
 }
 ```
 
-#### Influence of memory allocation failure modes flags in assumption contexts
-
-CBMC models
-[memory allocation failure modes](https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/memory-primitives.md#malloc-modelling).
-When activated, these modesl result in different
-behaviours for `__CPROVER_is_fresh` in assumption contexts (i.e. when used in a
-requires clause of a contract being checked against a function, or in an
-ensures clause of a contract being used to abstract a function call).
-
-1. **No failure mode** (no flags):
-  In this mode, `malloc` and `__CPROVER_is_fresh` never fail
-  and will accept a size parameter up to `SIZE_MAX` without triggerring errors.
-  However, pointer overflow and assigns clause checking errors will happen any
-  time one tries to access such objects beyond an offset of
-  `__CPROVER_max_malloc_size` (in bytes), by executing `ptr[size-1]` or
-  `ptr[size]` in user-code, or by writing
-  `__CPROVER_assigns(__CPROVER_object_from(ptr))` in a contract;
-1. **Fail with NULL** (flags: `--malloc-may-fail --malloc-fail-null`):
-  In this mode, if `size` is larger than
-  `__CPROVER_max_malloc_size`, `malloc` returns a NULL pointer, and imposes an
-  implicit assumption that size is less than `__CPROVER_max_malloc_size` when
-  returning a non-NULL pointer. `__CPROVER_is_fresh` never fails in assumption
-  contexts, so it adds an implicit assumption that `size` is less
-  than `__CPROVER_max_malloc_size`.
-1. **Fail assert** (flags: `--malloc-may-fail --malloc-fail-assert`):
-  In this mode, if `size` is larger
-  than `__CPROVER_max_malloc_size`, an `max allocation size exceeded` assertion
-  is triggered in `malloc` and execution continues under the assumption that
-  `size` is less than `__CPROVER_max_malloc_size`, with `malloc` returning a
-  non-NULL pointer. `__CPROVER_is_fresh` never fails in assumption contexts,
-  so it will trigger a `max allocation size exceeded` assertion and continue
-  execution under the implicit assumption that `size` is less than
-  `__CPROVER_max_malloc_size`.
-
-## The __CPROVER_pointer_in_range_dfcc predicate
-### Syntax
-
-```c
-bool __CPROVER_pointer_in_range_dfcc(void *lb, void *p, void *ub);
-```
-
-This predicate holds if `lb`, `p` and `ub` are valid pointers within the same
-object and the pointers are ordered such that `lb <= p && p <= ub` holds.
+## Writing your own memory predicates
 
-### Semantics
-In assertion contexts, the predicate checks the conditions described above.
-In assumption contexts, the predicate checks that `lb` and `ub` are valid pointers
-into the same object, and updates `p` using a side effect to be a non-deterministic
-pointer ranging between `lb` and `ub`.
-
-## User defined memory predicates
-
-Users can write their own memory predicates based on the core predicates described above.
-`__CPROVER_is_fresh` allows to specify pointer validity and separation.
-`__CPROVER_pointer_in_range` allows to specify aliasing constraints.
-
-For instance, one could write a predicate defining linked lists of at most `len`
-elements as follows:
-
-```c
-typedef struct list_t
-{
-  int value;
-  struct list_t *next;
-} list_t;
+One can write their own memory predicates based on the built-in predicates.
 
-// true iff list of len nodes with values in [-10,10]
-bool is_list(list_t *l, size_t len)
-{
-  if(len == 0)
-    return l == NULL;
-  else
-    return __CPROVER_is_fresh(l, sizeof(*l)) && -10 <= l->value &&
-           l->value <= 10 && is_list(l->next, len - 1);
-}
-```
 
-One can also simply describe finite nested structures:
+One can specify (finite) nested structures:
 
 ```c
 typedef struct buffer_t
@@ -283,16 +201,46 @@ bool is_double_buffer(double_buffer_t *b)
 }
 ```
 
-And one can then use these predicates in requires or ensures clauses for function
-contracts.
+One can even describe inductively defined (but bounded) structures such as lists:
+
+```c
+typedef struct list_t
+{
+  int value;
+  struct list_t *next;
+} list_t;
+
+bool value_in_range(int lb, int value, int ub) {
+  return lb <= value && value <= ub;
+}
+
+bool is_list(list_t *l, size_t len)
+{
+  if(len == 0) {
+    // list size bounded by `len`
+    return __CPROVER_pointer_equals(l,  NULL);
+  } else {
+    // either NULL or some fresh node
+    if (__CPROVER_pointer_equals(l,  NULL)) {
+      return true;
+    } else {
+      return __CPROVER_is_fresh(l, sizeof(*l)) &&
+        value_in_range(-10, l->value, 10) &&
+        is_list(l->next, len - 1);
+    }
+  }
+}
+```
+
+And use these predicates in requires/ensures clauses:
 
 ```c
+// take a list and a double buffer and sum list values and buffer sizes
 int foo(list_t *l, double_buffer_t *b)
   // clang-format off
   __CPROVER_requires(is_list(l, 3))
   __CPROVER_requires(is_double_buffer(b))
-  __CPROVER_ensures(-28 <= __CPROVER_return_value &&
-                    __CPROVER_return_value <= 50)
+  __CPROVER_ensures(-28 <= __CPROVER_return_value && __CPROVER_return_value <= 50)
 // clang-format on
 {
   // access the assumed data structure
@@ -301,16 +249,21 @@ int foo(list_t *l, double_buffer_t *b)
 }
 ```
 
+Internally, CBMC instruments these user-defined predicates to turn them into
+- nondeterministic allocators that build the data structures when used in
+  assumption contexts;
+- checker functions that can walk a pointer structure and check pointer validity
+  and separation/aliasing/interval constraints in assertion contexts.
+
 ### Limitations
 
 The main limitation with user defined predicates are:
 - their evaluation must terminate;
-- self-recursive predicates are supported, but mutually recursive predicates are
-  not supported for the moment.
+  - For instance, in the `is_list` example above, recursion is bounded using
+  use of the explicit `len` parameter.
+  - The `is_double_buffer` predicate also describes a bounded structure.
+- mutually-recursive predicates are not supported for the moment.
 
-For instance, in the `is_list` example above, recursion is bounded by the use of
-the explicit `len` parameter. The `is_double_buffer` predicate also describes
-a bounded structure.
 
 ## Additional Resources
 
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp
index 649e3e0cee9..321a6bdbadb 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp
@@ -30,6 +30,8 @@ init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
     function_symbols.insert(CPROVER_PREFIX "assert");
     function_symbols.insert(CPROVER_PREFIX "assignable");
     function_symbols.insert(CPROVER_PREFIX "assume");
+    function_symbols.insert(CPROVER_PREFIX "contracts_ptr_pred_ctx_init");
+    function_symbols.insert(CPROVER_PREFIX "contracts_ptr_pred_ctx_reset");
     function_symbols.insert(CPROVER_PREFIX "contracts_car_create");
     function_symbols.insert(CPROVER_PREFIX "contracts_car_set_contains");
     function_symbols.insert(CPROVER_PREFIX "contracts_car_set_create");
@@ -42,7 +44,7 @@ init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
     function_symbols.insert(CPROVER_PREFIX "contracts_is_fresh");
     function_symbols.insert(CPROVER_PREFIX "contracts_link_allocated");
     function_symbols.insert(CPROVER_PREFIX "contracts_link_deallocated");
-    function_symbols.insert(CPROVER_PREFIX "contracts_link_is_fresh");
+    function_symbols.insert(CPROVER_PREFIX "contracts_link_ptr_pred_ctx");
     function_symbols.insert(CPROVER_PREFIX "contracts_obeys_contract");
     function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_add");
     function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_append");
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
index efa62681c5f..f9a5f51c2fe 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
@@ -52,6 +52,8 @@ const std::map<dfcc_typet, irep_idt> create_dfcc_type_to_name()
     {dfcc_typet::CAR, CONTRACTS_PREFIX "car_t"},
     {dfcc_typet::CAR_SET, CONTRACTS_PREFIX "car_set_t"},
     {dfcc_typet::CAR_SET_PTR, CONTRACTS_PREFIX "car_set_ptr_t"},
+    {dfcc_typet::PTR_PRED_CTX, CONTRACTS_PREFIX "ptr_pred_ctx_t"},
+    {dfcc_typet::PTR_PRED_CTX_PTR, CONTRACTS_PREFIX "ptr_pred_ctx_ptr_t"},
     {dfcc_typet::OBJ_SET, CONTRACTS_PREFIX "obj_set_t"},
     {dfcc_typet::OBJ_SET_PTR, CONTRACTS_PREFIX "obj_set_ptr_t"},
     {dfcc_typet::WRITE_SET, CONTRACTS_PREFIX "write_set_t"},
@@ -122,9 +124,11 @@ const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name()
      CONTRACTS_PREFIX "write_set_havoc_object_whole"},
     {dfcc_funt::WRITE_SET_HAVOC_SLICE,
      CONTRACTS_PREFIX "write_set_havoc_slice"},
-    {dfcc_funt::LINK_IS_FRESH, CONTRACTS_PREFIX "link_is_fresh"},
+    {dfcc_funt::LINK_PTR_PRED_CTX, CONTRACTS_PREFIX "link_ptr_pred_ctx"},
     {dfcc_funt::LINK_ALLOCATED, CONTRACTS_PREFIX "link_allocated"},
     {dfcc_funt::LINK_DEALLOCATED, CONTRACTS_PREFIX "link_deallocated"},
+    {dfcc_funt::PTR_PRED_CTX_INIT, CONTRACTS_PREFIX "ptr_pred_ctx_init"},
+    {dfcc_funt::PTR_PRED_CTX_RESET, CONTRACTS_PREFIX "ptr_pred_ctx_reset"},
     {dfcc_funt::POINTER_EQUALS, CONTRACTS_PREFIX "pointer_equals"},
     {dfcc_funt::IS_FRESH, CONTRACTS_PREFIX "is_fresh"},
     {dfcc_funt::POINTER_IN_RANGE_DFCC,
@@ -810,14 +814,14 @@ const code_function_callt dfcc_libraryt::write_set_deallocate_freeable_call(
   return call;
 }
 
-const code_function_callt dfcc_libraryt::link_is_fresh_call(
+const code_function_callt dfcc_libraryt::link_ptr_pred_ctx_call(
   const exprt &write_set_ptr,
-  const exprt &is_fresh_obj_set_ptr,
+  const exprt &ptr_pred_ctx_ptr,
   const source_locationt &source_location)
 {
   code_function_callt call(
-    dfcc_fun_symbol[dfcc_funt::LINK_IS_FRESH].symbol_expr(),
-    {write_set_ptr, is_fresh_obj_set_ptr});
+    dfcc_fun_symbol[dfcc_funt::LINK_PTR_PRED_CTX].symbol_expr(),
+    {write_set_ptr, ptr_pred_ctx_ptr});
   call.add_source_location() = source_location;
   return call;
 }
@@ -882,3 +886,25 @@ const code_function_callt dfcc_libraryt::obj_set_release_call(
   call.add_source_location() = source_location;
   return call;
 }
+
+const code_function_callt dfcc_libraryt::ptr_pred_ctx_init_call(
+  const exprt &ptr_pred_ctx_ptr,
+  const source_locationt &source_location)
+{
+  code_function_callt call(
+    dfcc_fun_symbol[dfcc_funt::PTR_PRED_CTX_INIT].symbol_expr(),
+    {ptr_pred_ctx_ptr});
+  call.add_source_location() = source_location;
+  return call;
+}
+
+const code_function_callt dfcc_libraryt::ptr_pred_ctx_reset_call(
+  const exprt &ptr_pred_ctx_ptr,
+  const source_locationt &source_location)
+{
+  code_function_callt call(
+    dfcc_fun_symbol[dfcc_funt::PTR_PRED_CTX_INIT].symbol_expr(),
+    {ptr_pred_ctx_ptr});
+  call.add_source_location() = source_location;
+  return call;
+}
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
index 68e243200b7..d119fc1926b 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
@@ -31,6 +31,10 @@ enum class dfcc_typet
   CAR_SET,
   /// type of pointers to sets of CAR
   CAR_SET_PTR,
+  /// type of context info for pointer predicates evaluation
+  PTR_PRED_CTX,
+  /// type of pointers to context info for pointer predicates evaluation
+  PTR_PRED_CTX_PTR,
   /// type of sets of object identifiers
   OBJ_SET,
   /// type of pointers to sets of object identifiers
@@ -62,6 +66,10 @@ enum class dfcc_funt
   OBJ_SET_CREATE_APPEND,
   /// \see __CPROVER_contracts_obj_set_release
   OBJ_SET_RELEASE,
+  /// \see __CPROVER_contracts_ptr_pred_ctx_init
+  PTR_PRED_CTX_INIT,
+  /// \see __CPROVER_contracts_ptr_pred_ctx_reset
+  PTR_PRED_CTX_RESET,
   /// \see __CPROVER_contracts_obj_set_add
   OBJ_SET_ADD,
   /// \see __CPROVER_contracts_obj_set_append
@@ -120,8 +128,8 @@ enum class dfcc_funt
   WRITE_SET_HAVOC_OBJECT_WHOLE,
   /// \see __CPROVER_contracts_write_set_havoc_slice
   WRITE_SET_HAVOC_SLICE,
-  /// \see __CPROVER_contracts_link_is_fresh
-  LINK_IS_FRESH,
+  /// \see __CPROVER_contracts_link_ptr_pred_ctx
+  LINK_PTR_PRED_CTX,
   /// \see __CPROVER_contracts_link_allocated
   LINK_ALLOCATED,
   /// \see __CPROVER_contracts_link_deallocated
@@ -155,9 +163,7 @@ class typet;
 class dfcc_libraryt
 {
 public:
-  dfcc_libraryt(
-    goto_modelt &goto_model,
-    message_handlert &lmessage_handler);
+  dfcc_libraryt(goto_modelt &goto_model, message_handlert &lmessage_handler);
 
 protected:
   /// True iff the contracts library symbols are loaded
@@ -413,10 +419,10 @@ class dfcc_libraryt
     const source_locationt &source_location);
 
   /// \brief Builds call to
-  /// \ref __CPROVER_contracts_link_is_fresh
-  const code_function_callt link_is_fresh_call(
+  /// \ref __CPROVER_contracts_link_ptr_pred_ctx
+  const code_function_callt link_ptr_pred_ctx_call(
     const exprt &write_set_ptr,
-    const exprt &is_fresh_obj_set_ptr,
+    const exprt &ptr_pred_ctx_ptr,
     const source_locationt &source_location);
 
   /// \brief Builds call to
@@ -451,6 +457,18 @@ class dfcc_libraryt
   const code_function_callt obj_set_release_call(
     const exprt &obj_set_ptr,
     const source_locationt &source_location);
+
+  /// \brief Builds call to
+  /// \ref __CPROVER_contracts_ptr_pred_ctx_init
+  const code_function_callt ptr_pred_ctx_init_call(
+    const exprt &ptr_pred_ctx_ptr,
+    const source_locationt &source_location);
+
+  /// \brief Builds call to
+  /// \ref __CPROVER_contracts_ptr_pred_ctx_init
+  const code_function_callt ptr_pred_ctx_reset_call(
+    const exprt &ptr_pred_ctx_ptr,
+    const source_locationt &source_location);
 };
 
 #endif
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
index 17b2f07d195..9124f954e8d 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
@@ -116,30 +116,30 @@ static symbol_exprt create_addr_of_ensures_write_set(
 }
 
 /// Generate object set used to support is_fresh predicates
-static symbol_exprt create_is_fresh_set(
+static symbol_exprt create_ptr_pred_ctx(
   symbol_table_baset &symbol_table,
   dfcc_libraryt &library,
   const symbolt &wrapper_symbol)
 {
   return dfcc_utilst::create_symbol(
     symbol_table,
-    library.dfcc_type[dfcc_typet::OBJ_SET],
+    library.dfcc_type[dfcc_typet::PTR_PRED_CTX],
     wrapper_symbol.name,
-    "__is_fresh_set",
+    "__ptr_pred_ctx",
     wrapper_symbol.location);
 }
 
 /// Generate object set pointer used to support is_fresh predicates
-static symbol_exprt create_addr_of_is_fresh_set(
+static symbol_exprt create_addr_of_ptr_pred_ctx(
   symbol_table_baset &symbol_table,
   dfcc_libraryt &library,
   const symbolt &wrapper_symbol)
 {
   return dfcc_utilst::create_symbol(
     symbol_table,
-    library.dfcc_type[dfcc_typet::OBJ_SET_PTR],
+    library.dfcc_type[dfcc_typet::PTR_PRED_CTX_PTR],
     wrapper_symbol.name,
-    "__address_of_is_fresh_set",
+    "__address_of_ptr_pred_ctx",
     wrapper_symbol.location);
 }
 
@@ -187,9 +187,9 @@ dfcc_wrapper_programt::dfcc_wrapper_programt(
       goto_model.symbol_table,
       library,
       wrapper_symbol)),
-    is_fresh_set(
-      create_is_fresh_set(goto_model.symbol_table, library, wrapper_symbol)),
-    addr_of_is_fresh_set(create_addr_of_is_fresh_set(
+    ptr_pred_ctx(
+      create_ptr_pred_ctx(goto_model.symbol_table, library, wrapper_symbol)),
+    addr_of_ptr_pred_ctx(create_addr_of_ptr_pred_ctx(
       goto_model.symbol_table,
       library,
       wrapper_symbol)),
@@ -227,7 +227,7 @@ dfcc_wrapper_programt::dfcc_wrapper_programt(
   // encode all contract clauses
   encode_requires_write_set();
   encode_ensures_write_set();
-  encode_is_fresh_set();
+  encode_ptr_pred_ctx();
   encode_requires_clauses();
   encode_contract_write_set();
   encode_function_call();
@@ -247,7 +247,7 @@ void dfcc_wrapper_programt::add_to_dest(goto_programt &dest)
 {
   // add code to dest in the right order
   dest.destructive_append(preamble);
-  dest.destructive_append(link_is_fresh);
+  dest.destructive_append(link_ptr_pred_ctx);
   dest.destructive_append(preconditions);
   dest.destructive_append(history);
   dest.destructive_append(write_set_checks);
@@ -501,39 +501,39 @@ void dfcc_wrapper_programt::encode_contract_write_set()
     goto_programt::make_dead(addr_of_contract_write_set, wrapper_sl));
 }
 
-void dfcc_wrapper_programt::encode_is_fresh_set()
+void dfcc_wrapper_programt::encode_ptr_pred_ctx()
 {
-  preamble.add(goto_programt::make_decl(is_fresh_set, wrapper_sl));
+  preamble.add(goto_programt::make_decl(ptr_pred_ctx, wrapper_sl));
 
-  preamble.add(goto_programt::make_decl(addr_of_is_fresh_set, wrapper_sl));
+  preamble.add(goto_programt::make_decl(addr_of_ptr_pred_ctx, wrapper_sl));
   preamble.add(goto_programt::make_assignment(
-    addr_of_is_fresh_set, address_of_exprt(is_fresh_set), wrapper_sl));
+    addr_of_ptr_pred_ctx, address_of_exprt(ptr_pred_ctx), wrapper_sl));
 
-  // CALL obj_set_create_indexed_by_object_id(is_fresh_set) in preamble
+  // CALL ptr_pred_ctx_init(ptr_pred_ctx) in preamble
   preamble.add(goto_programt::make_function_call(
-    library.obj_set_create_indexed_by_object_id_call(
-      addr_of_is_fresh_set, wrapper_sl),
+    library.ptr_pred_ctx_init_call(addr_of_ptr_pred_ctx, wrapper_sl),
     wrapper_sl));
 
   // link to requires write set
-  link_is_fresh.add(goto_programt::make_function_call(
-    library.link_is_fresh_call(
-      addr_of_requires_write_set, addr_of_is_fresh_set, wrapper_sl),
+  link_ptr_pred_ctx.add(goto_programt::make_function_call(
+    library.link_ptr_pred_ctx_call(
+      addr_of_requires_write_set, addr_of_ptr_pred_ctx, wrapper_sl),
     wrapper_sl));
 
   // link to ensures write set
-  link_is_fresh.add(goto_programt::make_function_call(
-    library.link_is_fresh_call(
-      addr_of_ensures_write_set, addr_of_is_fresh_set, wrapper_sl),
+  link_ptr_pred_ctx.add(goto_programt::make_function_call(
+    library.link_ptr_pred_ctx_call(
+      addr_of_ensures_write_set, addr_of_ptr_pred_ctx, wrapper_sl),
     wrapper_sl));
 
-  // release call in postamble
-  postamble.add(goto_programt::make_function_call(
-    library.obj_set_release_call(addr_of_is_fresh_set, wrapper_sl),
+  // reset tracking of target pointers to allow ensures clause to
+  // post different predicates.
+  link_deallocated_contract.add(goto_programt::make_function_call(
+    library.ptr_pred_ctx_reset_call(addr_of_ptr_pred_ctx, wrapper_sl),
     wrapper_sl));
 
   // DEAD instructions in postamble
-  postamble.add(goto_programt::make_dead(is_fresh_set, wrapper_sl));
+  postamble.add(goto_programt::make_dead(ptr_pred_ctx, wrapper_sl));
 }
 
 /// Recursively traverses expression, adding "no_fail" attributes to pointer
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
index 224bdf8f795..cd6910507d0 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
@@ -41,14 +41,15 @@ class conditional_target_group_exprt;
 /// \details The body of the wrapper is divided into a number of sections
 /// represented as separate goto_programs:
 /// - \ref preamble
-///  - create is_fresh_set, requires_write_set, ensures_write_set,
+///  - create ptr_pred_ctx, requires_write_set, ensures_write_set,
 ///    contract_write_set variables
-/// - \ref link_is_fresh
-///   - link the is_fresh_set to requires_write_set and ensures_write_set
+/// - \ref link_ptr_pred_ctx
+///   - link the ptr_pred_ctx to requires_write_set and ensures_write_set
 ///   - in REPLACE mode, link the caller_write_set to the contract_write_set
 ///     so that deallocations and allocations are reflected in the caller
 /// - \ref preconditions
-///   - evaluate preconditions, checking side effects against requires_write_set
+///   - evaluate preconditions, while checking the absence of side effects
+///     against the empty requires_write_set
 /// - \ref history
 ///   - declare and snapshot history variables
 /// - \ref write_set_checks
@@ -82,7 +83,8 @@ class conditional_target_group_exprt;
 ///   CALL link_allocated(ensures_write_set, caller_write_set);
 ///   ```
 /// - \ref postconditions
-///   - evaluate preconditions, checking side effects against ensures_write_set
+///   - reset pointer predicate context object, evaluate preconditions while
+///     checking absence of side effects against the empty ensures_write_set
 /// - \ref postamble
 ///  - release all object sets and write set variables
 ///
@@ -159,10 +161,10 @@ class dfcc_wrapper_programt
   const symbol_exprt addr_of_ensures_write_set;
 
   /// Symbol for the object set used to evaluate is_fresh predicates.
-  const symbol_exprt is_fresh_set;
+  const symbol_exprt ptr_pred_ctx;
 
   /// Symbol for the pointer to the is_fresh object set.
-  const symbol_exprt addr_of_is_fresh_set;
+  const symbol_exprt addr_of_ptr_pred_ctx;
 
   /// Set of required or ensured contracts for function pointers discovered
   /// when processing the contract of interest.
@@ -187,7 +189,7 @@ class dfcc_wrapper_programt
   // in the declaration order below.
 
   goto_programt preamble;
-  goto_programt link_is_fresh;
+  goto_programt link_ptr_pred_ctx;
   goto_programt preconditions;
   goto_programt history;
   goto_programt write_set_checks;
@@ -224,11 +226,12 @@ class dfcc_wrapper_programt
   /// - Adds release function call in \ref postamble
   void encode_contract_write_set();
 
-  /// Encodes the object set used to evaluate is fresh predicates,
-  /// - Adds declaration of object set and pointer to set to \ref preamble
-  /// - Adds initialisation function call in \ref preamble
-  /// - Adds release function call in \ref postamble
-  void encode_is_fresh_set();
+  /// Encodes the pointer predicates evaluation context object.
+  /// - Adds declaration of context object and pointer to \ref preamble
+  /// - Adds init function call in \ref preamble
+  /// - Adds reset function call in \ref link_deallocated_contract
+  /// - Adds dead instruction in \ref postamble
+  void encode_ptr_pred_ctx();
 
   /// Encodes preconditions, instruments them to check for side effects
   void encode_requires_clauses();