Simplify equality over address-of with offset

regression/cbmc/Pointer_comparison5/main.c

@@ -0,0 +1,16 @@
+int main()
+{
+  int A[2];
+  int b;
+
+  int *ptr = &A[1];
+
+  if(ptr == &b)
+  {
+    __CPROVER_assert(0, "unreachable");
+  }
+  else if((unsigned long long)ptr == (unsigned long long)&b)
+  {
+    __CPROVER_assert(0, "unreachable");
+  }
+}

regression/cbmc/Pointer_comparison5/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+
+^Generated \d+ VCC\(s\), 1 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Simplification and constant propagation make the comparison over (unrelated)
+pointers trivially false; the corresponding comparison over pointers cast to
+integers is not simplified as the simplifier need not know how pointers convert
+to integers (except for NULL).

src/util/simplify_expr_int.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include "rational_tools.h"
 #include "simplify_utils.h"
 #include "std_expr.h"
+#include "threeval.h"
 
 #include <algorithm>
 
@@ -1605,6 +1606,38 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
     {
       return unchanged(expr);
     }
+    else if(
+      expr.id() == ID_equal && ptr_op0.id() == ID_address_of &&
+      ptr_op1.id() == ID_address_of)
+    {
+      // comparing pointers: if both are address-of-plus-some-constant such that
+      // the resulting pointer remains within object bounds then they can never
+      // be equal
+      auto in_bounds = [this](const exprt &object_ptr, const exprt &expr_op) {
+        auto object_size =
+          size_of_expr(to_address_of_expr(object_ptr).object().type(), ns);
+
+        if(object_size.has_value())
+        {
+          pointer_offset_exprt offset{expr_op, object_size->type()};
+          exprt in_object_bounds =
+            simplify_rec(binary_relation_exprt{
+                           std::move(offset), ID_lt, std::move(*object_size)})
+              .expr;
+          if(in_object_bounds.is_constant())
+            return tvt{in_object_bounds.is_true()};
+        }
+
+        return tvt::unknown();
+      };
+
+      if(
+        in_bounds(ptr_op0, expr.op0()).is_true() &&
+        in_bounds(ptr_op1, expr.op1()).is_true())
+      {
+        return false_exprt{};
+      }
+    }
   }
 
   // eliminate strict inequalities