NULL compares equal to 0

regression/cbmc/union13/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  union {
+    intptr_t i;
+    int *p;
+  } u;
+  u.i = 0;
+  assert(u.p == 0);
+}

regression/cbmc/union13/no-arch.desc

@@ -0,0 +1,9 @@
+CORE broken-smt-backend
+main.c
+--arch none --little-endian
+(Starting CEGAR Loop|^Generated 1 VCC\(s\), 1 remaining after simplification$)
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/union13/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/util/simplify_expr_int.cpp

@@ -1357,8 +1357,23 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
   {
     if(expr.id() == ID_equal || expr.id() == ID_notequal)
     {
-
+      // two constants compare equal when there values (as strings) are the same
+      // or both of them are pointers and both represent NULL in some way
       bool equal = (tmp0_const->get_value() == tmp1_const->get_value());
+      if(
+        !equal && tmp0_const->type().id() == ID_pointer &&
+        tmp1_const->type().id() == ID_pointer)
+      {
+        if(
+          !config.ansi_c.NULL_is_zero && (tmp0_const->get_value() == ID_NULL ||
+                                          tmp1_const->get_value() == ID_NULL))
+        {
+          // if NULL is not zero on this platform, we really don't know what it
+          // is and therefore cannot simplify
+          return true;
+        }
+        equal = tmp0_const->is_zero() && tmp1_const->is_zero();
+      }
       expr.make_bool(expr.id() == ID_equal ? equal : !equal);
       return false;
     }