diff --git a/regression/cprover/pointers/allocate1.c b/regression/cprover/pointers/allocate1.c
new file mode 100644
index 00000000000..9bf9c490900
--- /dev/null
+++ b/regression/cprover/pointers/allocate1.c
@@ -0,0 +1,14 @@
+// Regression test for cprover establishing liveness of __CPROVER_allocate.
+// Before the fix the "pointer p safe" checks over the allocated object were
+// spuriously refuted; after the fix they are proved like for malloc.
+void *__CPROVER_allocate(__CPROVER_size_t, int);
+
+int *p;
+
+int main()
+{
+  p = __CPROVER_allocate(sizeof(int) * 10, 0);
+  p[2] = 123;
+  __CPROVER_assert(p[2] == 123, "property 1");
+  return 0;
+}
diff --git a/regression/cprover/pointers/allocate1.desc b/regression/cprover/pointers/allocate1.desc
new file mode 100644
index 00000000000..67427331684
--- /dev/null
+++ b/regression/cprover/pointers/allocate1.desc
@@ -0,0 +1,10 @@
+CORE
+allocate1.c
+--text --solve --inline
+^EXIT=0$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. S\d+\(ς\) ⇒ S\d+\(ς\[❝main::\$tmp::malloc_value❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[\d+\]\)\)\]\)$
+^\[main\.pointer\.1\] line \d+ pointer .* safe: SUCCESS$
+^\[main\.pointer\.2\] line \d+ pointer .* safe: SUCCESS$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+--
diff --git a/regression/cprover/pointers/allocate2.c b/regression/cprover/pointers/allocate2.c
new file mode 100644
index 00000000000..602aaccbc2f
--- /dev/null
+++ b/regression/cprover/pointers/allocate2.c
@@ -0,0 +1,13 @@
+// Soundness companion: an out-of-bounds access to an __CPROVER_allocate'd
+// object must still be refuted (the liveness fix must not mask it).
+void *__CPROVER_allocate(__CPROVER_size_t, int);
+
+int *p;
+
+int main()
+{
+  p = __CPROVER_allocate(sizeof(int), 0);
+  p[5] = 123;
+  __CPROVER_assert(p[5] == 123, "property 1");
+  return 0;
+}
diff --git a/regression/cprover/pointers/allocate2.desc b/regression/cprover/pointers/allocate2.desc
new file mode 100644
index 00000000000..5662b470707
--- /dev/null
+++ b/regression/cprover/pointers/allocate2.desc
@@ -0,0 +1,8 @@
+CORE
+allocate2.c
+--text --solve --inline
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.pointer\.1\] line \d+ pointer .* safe: REFUTED$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+--
diff --git a/regression/cprover/pointers/allocate3.c b/regression/cprover/pointers/allocate3.c
new file mode 100644
index 00000000000..567105ca10f
--- /dev/null
+++ b/regression/cprover/pointers/allocate3.c
@@ -0,0 +1,15 @@
+// Known limitation: __CPROVER_allocate(size, 1) is the calloc lowering and
+// requests zero-initialised memory, but the cprover state encoder drops the
+// zero-init operand and models nondeterministic contents (like malloc), so a
+// read of the freshly-allocated memory cannot be proven to be 0.  Documented
+// as a KNOWNBUG; promote to CORE if/when zeroing is modelled.
+void *__CPROVER_allocate(__CPROVER_size_t, int);
+
+int *p;
+
+int main()
+{
+  p = __CPROVER_allocate(sizeof(int), 1); // calloc-style: zero-initialised
+  __CPROVER_assert(p[0] == 0, "property 1");
+  return 0;
+}
diff --git a/regression/cprover/pointers/allocate3.desc b/regression/cprover/pointers/allocate3.desc
new file mode 100644
index 00000000000..cba01aa2828
--- /dev/null
+++ b/regression/cprover/pointers/allocate3.desc
@@ -0,0 +1,13 @@
+KNOWNBUG
+allocate3.c
+--text --solve --inline
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+--
+--
+The calloc lowering __CPROVER_allocate(size, 1) requests zero-initialised
+memory, but the cprover state encoder drops the zero-init operand and models
+nondeterministic contents (matching malloc/posix_memalign/realloc), so
+`p[0] == 0` is currently REFUTED rather than SUCCESS.  Marked KNOWNBUG to
+document the limitation; promote to CORE if/when zeroing is modelled.
diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp
index 39e89cb0d45..decbfe4bc1d 100644
--- a/src/cprover/state_encoding.cpp
+++ b/src/cprover/state_encoding.cpp
@@ -338,6 +338,32 @@ exprt state_encodingt::evaluate_expr_rec(
   }
   else if(what.id() == ID_side_effect)
   {
+    const auto &side_effect = to_side_effect_expr(what);
+    if(
+      side_effect.get_statement() == ID_allocate &&
+      side_effect.operands().size() == 2 &&
+      side_effect.type().id() == ID_pointer)
+    {
+      // __CPROVER_allocate is handled like the malloc call (see the malloc
+      // handling in function_call_symbol below): tie the allocation to the
+      // current state so its result is a live dynamic object. Without this,
+      // the generic allocate side effect leaves liveness unestablished, and
+      // "pointer safe" properties over the allocated object are spuriously
+      // refuted.  c_typecheck_expr rejects an ID_allocate without exactly two
+      // operands (size, zero-init flag), so the size() == 2 check documents
+      // that invariant rather than building an allocation from a partial
+      // operand list; the side effect's type is always void *, so the
+      // ID_pointer conjunct is defensive only.
+      //
+      // NOTE: operands()[1] is the zero-initialisation flag (calloc lowers to
+      // __CPROVER_allocate(size, 1)); like the malloc/posix_memalign/realloc
+      // cases this backend does not model zeroing, so the allocated contents
+      // are left nondeterministic.  TODO: model zeroing.
+      auto size_evaluated = evaluate_expr_rec(
+        loc, state, side_effect.operands().front(), bound_symbols);
+      return allocate_exprt{
+        state, size_evaluated, to_pointer_type(side_effect.type())};
+    }
     // leave as is
     return what;
   }