From c2cbaadbcb65795a5d6f772ff0b3479f3d87bcee Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 3 Feb 2022 12:33:53 +0000
Subject: [PATCH] Simplify overflow-mult when one operand is 1

1 (one) is a neutral element for multiplication.
---
 src/util/simplify_expr.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index e3b1ba6da54..b11fe680833 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -2174,7 +2174,8 @@ simplify_exprt::simplify_complex(const unary_exprt &expr)
 simplify_exprt::resultt<>
 simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr)
 {
-  // zero is a neutral element for all operations supported here
+  // When one operand is zero, an overflow can only occur for a subtraction from
+  // zero.
   if(
     expr.op1().is_zero() ||
     (expr.op0().is_zero() && expr.id() != ID_overflow_minus))
@@ -2182,6 +2183,14 @@ simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr)
     return false_exprt{};
   }
 
+  // One is neutral element for multiplication
+  if(
+    expr.id() == ID_overflow_mult &&
+    (expr.op0().is_one() || expr.op1().is_one()))
+  {
+    return false_exprt{};
+  }
+
   // we only handle the case of same operand types
   if(expr.op0().type() != expr.op1().type())
     return unchanged(expr);