Simplify inequality over pointers

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.c

@@ -2,8 +2,8 @@
 
 int main()
 {
-  int i = 12;
-  int *x = &i;
+  int i[2] = {12, 13};
+  int *x = &i[0] + 1;
   int *y = x + 1;
   int *z = x - 1;
 

regression/cbmc/Pointer_comparison4/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int A[5] = {0, 1, 2, 3, 4};
+  for(int *iter = &A[0]; iter < &A[5]; ++iter)
+    __CPROVER_assert(*iter == iter - &A[0], "values match");
+}

regression/cbmc/Pointer_comparison4/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--unwind 10 --unwinding-assertions
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+Unwinding loop .* iteration 6
+^warning: ignoring
+--
+Simplification and constant propagation should ensure that unwinding the loop
+stops when reaching the array bound.

src/util/simplify_expr_int.cpp

@@ -1587,12 +1587,24 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
   if(expr.op0().type().id() == ID_floatbv)
     return unchanged(expr);
 
-  // simplifications below require same-object, which we don't check for
-  if(
-    expr.op0().type().id() == ID_pointer && expr.id() != ID_equal &&
-    expr.id() != ID_notequal)
+  if(expr.op0().type().id() == ID_pointer)
   {
-    return unchanged(expr);
+    exprt ptr_op0 = simplify_object(expr.op0()).expr;
+    exprt ptr_op1 = simplify_object(expr.op1()).expr;
+
+    if(ptr_op0 == ptr_op1)
+    {
+      pointer_offset_exprt offset_op0{expr.op0(), size_type()};
+      pointer_offset_exprt offset_op1{expr.op1(), size_type()};
+
+      return changed(simplify_rec(binary_relation_exprt{
+        std::move(offset_op0), expr.id(), std::move(offset_op1)}));
+    }
+    // simplifications below require same-object, which we don't check for
+    else if(expr.id() != ID_equal && expr.id() != ID_notequal)
+    {
+      return unchanged(expr);
+    }
   }
 
   // eliminate strict inequalities
@@ -1651,19 +1663,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
       new_expr.rhs() = simplify_node(new_expr.rhs());
       return changed(simplify_inequality(new_expr)); // recursive call
     }
-    else if(expr.op0().type().id() == ID_pointer)
-    {
-      exprt ptr_op0 = simplify_object(expr.op0()).expr;
-      exprt ptr_op1 = simplify_object(expr.op1()).expr;
-
-      if(ptr_op0 == ptr_op1)
-      {
-        pointer_offset_exprt offset_op0{expr.op0(), size_type()};
-        pointer_offset_exprt offset_op1{expr.op1(), size_type()};
-
-        return changed(simplify_rec(equal_exprt{offset_op0, offset_op1}));
-      }
-    }
   }
 
   return unchanged(expr);