From 4220adee62f4639b1e23f7aeffbfd26731035fe6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 1 Apr 2026 18:45:43 +0000
Subject: [PATCH] Simplify (x * n) % n

For unbounded integer/natural types, (x * n) % n is always zero.
For bitvector types, this only holds when n divides 2^width (i.e.,
n is a power of two that fits in the bit-width), because otherwise
the multiplication may wrap and the remainder is no longer zero.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 src/util/simplify_expr_int.cpp | 35 ++++++++++++++++++++++++++++++++++
 unit/util/simplify_expr.cpp    | 35 ++++++++++++++++++++++++++++++++++
 2 files changed, 70 insertions(+)

diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index f789bfdfb37..7d9ea7016e5 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -397,6 +397,41 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mod(const mod_exprt &expr)
         mp_integer result = *int_value0 % *int_value1;
         return from_integer(result, expr.type());
       }
+
+      // (x * n) % n is zero for mathematical integers (regardless of
+      // sign, since n always divides x * n). For bitvector types,
+      // multiplication wraps modulo 2^width, so the identity only holds
+      // when n divides 2^width — this is both necessary and sufficient,
+      // and is equivalent to n being a power of two within the width.
+      if(int_value1.has_value() && *int_value1 != 0)
+      {
+        const auto &type_id = expr.type().id();
+        bool can_simplify = (type_id == ID_integer || type_id == ID_natural);
+
+        if(
+          !can_simplify &&
+          (type_id == ID_unsignedbv || type_id == ID_signedbv) &&
+          *int_value1 > 0)
+        {
+          const auto width = to_bitvector_type(expr.type()).get_width();
+          can_simplify = (power(2, width) % *int_value1 == 0);
+        }
+
+        if(
+          can_simplify && expr.op0().id() == ID_mult &&
+          expr.op0().operands().size() == 2)
+        {
+          const auto &mul = to_mult_expr(expr.op0());
+          const auto c0 = numeric_cast<mp_integer>(mul.op0());
+          const auto c1 = numeric_cast<mp_integer>(mul.op1());
+          if(
+            (c0.has_value() && *c0 == *int_value1) ||
+            (c1.has_value() && *c1 == *int_value1))
+          {
+            return from_integer(0, expr.type());
+          }
+        }
+      }
     }
   }
 
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 061af0534ae..f3d54290823 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -652,3 +652,38 @@ TEST_CASE("Simplify quantifier", "[core][util]")
     REQUIRE(simplify_expr(forall_exprt{a, true_exprt{}}, ns) == true_exprt{});
   }
 }
+
+TEST_CASE("Simplify (x * n) % n", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  SECTION("Integer type: always simplifies")
+  {
+    const integer_typet int_type;
+    const symbol_exprt x{"x", int_type};
+    const auto n = from_integer(7, int_type);
+    REQUIRE(
+      simplify_expr(mod_exprt{mult_exprt{x, n}, n}, ns) ==
+      from_integer(0, int_type));
+  }
+
+  SECTION("Unsigned bitvector with power-of-two modulus: simplifies")
+  {
+    const unsignedbv_typet u32{32};
+    const symbol_exprt x{"x", u32};
+    const auto n = from_integer(8, u32);
+    REQUIRE(
+      simplify_expr(mod_exprt{mult_exprt{x, n}, n}, ns) ==
+      from_integer(0, u32));
+  }
+
+  SECTION("Unsigned bitvector with non-power-of-two modulus: no simplification")
+  {
+    const unsignedbv_typet u32{32};
+    const symbol_exprt x{"x", u32};
+    const auto n = from_integer(7, u32);
+    const mod_exprt mod{mult_exprt{x, n}, n};
+    REQUIRE(simplify_expr(mod, ns) == mod);
+  }
+}