From 897034af0aa8a4d4eceeb0cba2b2a6e2bfb1f8e0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 24 Jun 2022 07:36:11 +0000
Subject: [PATCH] Simplify equality of address-of-string-constant

The back-end assumes that each string is a singleton and, therefore,
taking the address of a particular string constant will always result in
the same value. The simplifier can use this information.

Fixes: #6966
---
 src/util/simplify_expr_pointer.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 43d1f3ee195..a1083dbda8f 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -467,6 +467,12 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
   {
     return make_boolean_expr(expr.id() != ID_equal);
   }
+  else if(
+    tmp0_object.id() == ID_string_constant &&
+    tmp1_object.id() == ID_string_constant && tmp0_object == tmp1_object)
+  {
+    return make_boolean_expr(expr.id() == ID_equal);
+  }
 
   return unchanged(expr);
 }