diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c
new file mode 100644
index 00000000000..604aef643ac
--- /dev/null
+++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c
@@ -0,0 +1,14 @@
+void foo(int *x)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)) || 1)
+  __CPROVER_assigns(*x)
+// clang-format on
+{
+  *x = 0;
+}
+
+void main()
+{
+  int *x;
+  foo(x);
+}
diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc
new file mode 100644
index 00000000000..b97ad84cbab
--- /dev/null
+++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc
@@ -0,0 +1,20 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$
+^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: (FAILURE|UNKNOWN)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (FAILURE|UNKNOWN)
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (FAILURE|UNKNOWN)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (FAILURE|UNKNOWN)
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (FAILURE|UNKNOWN)
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (FAILURE|UNKNOWN)
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (FAILURE|UNKNOWN)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when `__CPROVER_is_fresh` is used in disjunctions,
+the program accepts models where `__CPROVER_is_fresh` evaluates to false
+and no object gets allocated, and pointers remain invalid.
diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c
new file mode 100644
index 00000000000..204e3e3e9cc
--- /dev/null
+++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c
@@ -0,0 +1,30 @@
+#include <stdlib.h>
+void foo(int *x, int *y)
+  // clang-format off
+  __CPROVER_requires(
+    (__CPROVER_is_fresh(x, sizeof(*x)) && y == NULL) ||
+    (x == NULL && __CPROVER_is_fresh(y, sizeof(*y)))
+  )
+  __CPROVER_assigns(y == NULL: *x)
+  __CPROVER_assigns(x == NULL: *y)
+// clang-format on
+{
+  if(y == NULL)
+  {
+    assert(0);
+    *x = 0;
+  }
+  else
+  {
+    assert(0);
+    assert(x == NULL);
+    *y = 0;
+  }
+}
+
+void main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+}
diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc
new file mode 100644
index 00000000000..f5d0da4c552
--- /dev/null
+++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc
@@ -0,0 +1,30 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[foo.assertion.\d+\] line 14 assertion 0: FAILURE$
+^\[foo.assigns.\d+\] line 15 Check that \*x is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer NULL in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer invalid in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: dead object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: invalid integer address in \*x: SUCCESS$
+^\[foo.assertion.\d+\] line 19 assertion 0: FAILURE$
+^\[foo.assertion.\d+\] line 20 assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[foo.assigns.\d+\] line 21 Check that \*y is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer NULL in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer invalid in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: dead object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: invalid integer address in \*y: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts.
+The precondition of `foo` describes a disjunction of cases, either `x` is fresh and `y` is null,
+or `x` is null and `y` is fresh. The function `foo` branches on `y == NULL`.
+The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
+that both cases of the disjunction expressed in the requires clause are reachable.
diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c
new file mode 100644
index 00000000000..c5b856e6110
--- /dev/null
+++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c
@@ -0,0 +1,15 @@
+int *foo()
+  // clang-format off
+  __CPROVER_ensures(
+    __CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)) || 1);
+// clang-format on
+
+void bar()
+{
+  int *x = foo();
+  *x = 0; //expected to fail
+}
+void main()
+{
+  bar();
+}
diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc
new file mode 100644
index 00000000000..45828926d6a
--- /dev/null
+++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc
@@ -0,0 +1,17 @@
+CORE dfcc-only
+main.c
+--dfcc main --replace-call-with-contract foo
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when `__CPROVER_is_fresh` is used in disjunctions,
+the program accepts models where `__CPROVER_is_fresh` evaluates to false
+and no object gets allocated, and pointers remain invalid.
diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c
new file mode 100644
index 00000000000..c592dc8f4de
--- /dev/null
+++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c
@@ -0,0 +1,41 @@
+#include <stdlib.h>
+typedef struct
+{
+  int *x;
+  int *y;
+} ret_t;
+
+ret_t foo()
+  // clang-format off
+  __CPROVER_ensures((
+      __CPROVER_is_fresh(__CPROVER_return_value.x, sizeof(int)) &&
+      __CPROVER_return_value.y == NULL
+    ) || (
+      __CPROVER_return_value.x == NULL &&
+      __CPROVER_is_fresh(__CPROVER_return_value.y, sizeof(int))
+    ))
+  // clang-format on
+  ;
+
+void bar()
+{
+  ret_t ret = foo();
+  int *x = ret.x;
+  int *y = ret.y;
+  if(y == NULL)
+  {
+    assert(0);
+    *x = 0;
+  }
+  else
+  {
+    assert(0);
+    assert(x == NULL);
+    *y = 0;
+  }
+}
+
+void main()
+{
+  bar();
+}
diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc
new file mode 100644
index 00000000000..295434501f9
--- /dev/null
+++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc
@@ -0,0 +1,30 @@
+CORE dfcc-only
+main.c
+--dfcc main --replace-call-with-contract foo
+^\[bar.assertion.\d+\] line 27 assertion 0: FAILURE$
+^\[bar.assigns.\d+\] line 28 Check that \*x is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer NULL in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer invalid in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: dead object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: invalid integer address in \*x: SUCCESS$
+^\[bar.assertion.\d+\] line 32 assertion 0: FAILURE$
+^\[bar.assertion.\d+\] line 33 assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[bar.assigns.\d+\] line 34 Check that \*y is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer NULL in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer invalid in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: dead object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: invalid integer address in \*y: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts.
+The postcondition of `foo` describes a disjunction of cases: either `x` is fresh and `y` is null,
+or `x` is null and `y` is fresh. The function `bar` branches on `y == NULL`.
+The test succeeds if the two `assert(0)` are falsifiable, which which shows that
+both cases of the disjunction expressed in the ensures clause of `foo` are reachable.
diff --git a/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/main.c b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/main.c
new file mode 100644
index 00000000000..b4ad7f4386c
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/main.c
@@ -0,0 +1,16 @@
+void foo(int *x, int *y)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(x, 8*sizeof(int)))
+  __CPROVER_requires(__CPROVER_pointer_in_range_dfcc(x, y, x+7) || 1)
+  __CPROVER_assigns(*y)
+// clang-format on
+{
+  *y = 0;
+}
+
+void main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+}
diff --git a/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc
new file mode 100644
index 00000000000..50338575985
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc
@@ -0,0 +1,20 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
+^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when `__CPROVER_pointer_equals` is used in disjunctions,
+the program accepts models where `__CPROVER_pointer_equals` evaluates to
+false and the target pointer remains invalid.
diff --git a/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/main.c b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/main.c
new file mode 100644
index 00000000000..2c16b83c11a
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/main.c
@@ -0,0 +1,34 @@
+#include <stdlib.h>
+void foo(int *a, int *x, int *y)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(a, 8*sizeof(int)))
+  __CPROVER_requires(
+    (__CPROVER_pointer_in_range_dfcc(a, x, a+7) && y == NULL) ||
+    (x == NULL && __CPROVER_pointer_in_range_dfcc(a, y, a+7))
+  )
+  __CPROVER_assigns(y == NULL: *x)
+  __CPROVER_assigns(x == NULL: *y)
+// clang-format on
+{
+  if(y == NULL)
+  {
+    assert(0);
+    assert(__CPROVER_same_object(a, x));
+    *x = 0;
+  }
+  else
+  {
+    assert(0);
+    assert(x == NULL);
+    assert(__CPROVER_same_object(a, y));
+    *y = 0;
+  }
+}
+
+void main()
+{
+  int *a;
+  int *x;
+  int *y;
+  foo(a, x, y);
+}
diff --git a/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/test.desc b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/test.desc
new file mode 100644
index 00000000000..97ba8f9024d
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/test.desc
@@ -0,0 +1,32 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[foo.assertion.\d+\] line 15 assertion 0: FAILURE$
+^\[foo.assertion.\d+\] line 16 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$
+^\[foo.assigns.\d+\] line 17 Check that \*x is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer NULL in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer invalid in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 17 dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 17 dereference failure: dead object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 17 dereference failure: invalid integer address in \*x: SUCCESS$
+^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$
+^\[foo.assertion.\d+\] line 22 assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[foo.assertion.\d+\] line 23 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$
+^\[foo.assigns.\d+\] line 24 Check that \*y is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer NULL in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*y: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Illustrates the behaviour of `__CPROVER_pointer_in_range_dfcc` under disjunctions in assume contexts.
+The precondition of `foo` describes a disjunction of cases, either `x` is in range of `a` and `y` is null,
+or `x` is null and `y` is in range of `a`. The function `foo` branches on `y == NULL`.
+The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
+that both cases of the disjunction expressed in the requires clause are reachable.
diff --git a/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/main.c b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/main.c
new file mode 100644
index 00000000000..ffd3b7457af
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/main.c
@@ -0,0 +1,30 @@
+
+typedef struct
+{
+  int *a;
+  int *x;
+} ret_t;
+
+ret_t foo()
+  // clang-format off
+  __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, 8*sizeof(int)))
+  __CPROVER_ensures(
+    __CPROVER_pointer_in_range_dfcc(
+      __CPROVER_return_value.a,
+      __CPROVER_return_value.x,
+      __CPROVER_return_value.a + 7
+    ) || 1)
+  // clang-format on
+  ;
+
+void bar()
+{
+  ret_t ret = foo();
+  int *x = ret.x;
+  *x = 0; //expected to fail
+}
+
+void main()
+{
+  bar();
+}
diff --git a/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc
new file mode 100644
index 00000000000..b639707f5f5
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc
@@ -0,0 +1,17 @@
+CORE dfcc-only
+main.c
+--dfcc main --replace-call-with-contract foo
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when `__CPROVER_pointer_in_range_dfcc` is used in disjunctions,
+the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to
+false and the target pointer remains invalid.
diff --git a/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/main.c b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/main.c
new file mode 100644
index 00000000000..c2a62e7f31e
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/main.c
@@ -0,0 +1,51 @@
+#include <stdlib.h>
+typedef struct
+{
+  int *a;
+  int *x;
+  int *y;
+} ret_t;
+
+ret_t foo()
+  // clang-format off
+  __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, 8*sizeof(int)))
+  __CPROVER_ensures((
+      __CPROVER_pointer_in_range_dfcc(
+        __CPROVER_return_value.a,
+        __CPROVER_return_value.x,
+        __CPROVER_return_value.a + 7) &&
+      __CPROVER_return_value.y == NULL
+    ) || (
+      __CPROVER_return_value.x == NULL &&
+      __CPROVER_pointer_in_range_dfcc(
+        __CPROVER_return_value.a,
+        __CPROVER_return_value.y,
+        __CPROVER_return_value.a + 7)))
+  // clang-format on
+  ;
+
+void bar()
+{
+  ret_t ret = foo();
+  int *a = ret.a;
+  int *x = ret.x;
+  int *y = ret.y;
+  if(y == NULL)
+  {
+    assert(0);
+    assert(__CPROVER_same_object(x, a));
+    *x = 0;
+  }
+  else
+  {
+    assert(0);
+    assert(x == NULL);
+    assert(__CPROVER_same_object(y, a));
+    *y = 0;
+  }
+}
+
+void main()
+{
+  bar();
+}
diff --git a/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/test.desc b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/test.desc
new file mode 100644
index 00000000000..d0f29a67b8a
--- /dev/null
+++ b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/test.desc
@@ -0,0 +1,32 @@
+CORE dfcc-only
+main.c
+--dfcc main --replace-call-with-contract foo
+^\[bar.assertion.\d+\] line 35 assertion 0: FAILURE$
+^\[bar.assertion.\d+\] line 36 assertion __CPROVER_POINTER_OBJECT\(\(.*\)x\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
+^\[bar.assigns.\d+\] line 37 Check that \*x is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer NULL in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer invalid in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 37 dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 37 dereference failure: dead object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 37 dereference failure: invalid integer address in \*x: SUCCESS$
+^\[bar.assertion.\d+\] line 41 assertion 0: FAILURE$
+^\[bar.assertion.\d+\] line 42 assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[bar.assertion.\d+\] line 43 assertion __CPROVER_POINTER_OBJECT\(\(.*\)y\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
+^\[bar.assigns.\d+\] line 44 Check that \*y is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer NULL in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer invalid in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 44 dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 44 dereference failure: dead object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 44 dereference failure: invalid integer address in \*y: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Illustrates the behaviour of `__CPROVER_pointer_in_range` under disjunctions in assume contexts.
+The postcondition of `foo` describes a disjunction of cases: either `x` is in range of `a` and `y` is null,
+or `x` is null and `y` is in range of `a`. The function `bar` branches on `y == NULL`.
+The test succeeds if the two `assert(0)` are falsifiable, which which shows that
+both cases of the disjunction expressed in the ensures clause of `foo` are reachable.