Regression test for null-pointer optimisation

This is to guard against the regression earlier introduced in #4444 (and
reverted in #4656).

Author: tautschnig

regression/cbmc/null4/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  void *ptr;
+  if(ptr == 0)
+  {
+    return 0;
+  }
+  __CPROVER_assert(ptr != 0, "null");
+}

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).