diff --git a/regression/cbmc/null4/main.c b/regression/cbmc/null4/main.c
new file mode 100644
index 00000000000..a0fc5489923
--- /dev/null
+++ b/regression/cbmc/null4/main.c
@@ -0,0 +1,9 @@
+int main()
+{
+  void *ptr;
+  if(ptr == 0)
+  {
+    return 0;
+  }
+  __CPROVER_assert(ptr != 0, "null");
+}
diff --git a/regression/cbmc/null4/test.desc b/regression/cbmc/null4/test.desc
new file mode 100644
index 00000000000..926be8072d2
--- /dev/null
+++ b/regression/cbmc/null4/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Pull request #4444 introduced optimisations during symbolic execution that
+caused this test to spuriously fail (as the branch `ptr == 0` was removed).