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);