From b1fcc9ab5c4478ccb459731eca77d8596e5237e0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 23 May 2021 22:58:51 +0000
Subject: [PATCH] simplify_inequality_address_of only supports (not)equal

Invoking it for arbitrary binary comparisons resulted in an invariant
failure.
---
 regression/cbmc/Pointer_comparison3/main.c    | 9 +++++++++
 regression/cbmc/Pointer_comparison3/test.desc | 8 ++++++++
 src/util/simplify_expr_int.cpp                | 3 ++-
 3 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/Pointer_comparison3/main.c
 create mode 100644 regression/cbmc/Pointer_comparison3/test.desc

diff --git a/regression/cbmc/Pointer_comparison3/main.c b/regression/cbmc/Pointer_comparison3/main.c
new file mode 100644
index 00000000000..1b11452b31e
--- /dev/null
+++ b/regression/cbmc/Pointer_comparison3/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *p1 = malloc(sizeof(int));
+
+  assert(p1 < p1 + 1);
+}
diff --git a/regression/cbmc/Pointer_comparison3/test.desc b/regression/cbmc/Pointer_comparison3/test.desc
new file mode 100644
index 00000000000..278f468e130
--- /dev/null
+++ b/regression/cbmc/Pointer_comparison3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index c53d2c8f1f0..cc2731f3f4f 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1242,7 +1242,8 @@ simplify_exprt::simplify_inequality(const binary_relation_exprt &expr)
   // see if we are comparing pointers that are address_of
   if(
     skip_typecast(tmp0).id() == ID_address_of &&
-    skip_typecast(tmp1).id() == ID_address_of)
+    skip_typecast(tmp1).id() == ID_address_of &&
+    (expr.id() == ID_equal || expr.id() == ID_notequal))
   {
     return simplify_inequality_address_of(expr);
   }