From bb9a714124b1badf3ff1865d978c4fad8a39cb3d Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 12 May 2026 23:52:29 +0000
Subject: [PATCH] Fix: add mod simplification rule for (mod (+ ... k*y ...) y)
 = (mod (+ ...) y)

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/16d3a058-5225-44d4-8080-d1a641c181ff

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/rewriter/arith_rewriter.cpp | 35 +++++++++++++++++++++++++++++
 src/test/arith_rewriter.cpp         | 15 +++++++++++++
 2 files changed, 50 insertions(+)

diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 6fb848b5d..955bbbc2c 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -1465,6 +1465,41 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
         }
     }
 
+    // (mod (+ ... k*y ...) y) = (mod (+ ...) y) for integer k
+    // Remove summands that are integer multiples of arg2 from the sum.
+    if (!is_num2 && m_util.is_int(arg2) && is_add(arg1)) {
+        expr_ref_buffer new_args(m);
+        bool change = false;
+        for (expr* arg : *to_app(arg1)) {
+            expr* s1 = nullptr, *s2 = nullptr;
+            rational k;
+            if (arg == arg2) {
+                // summand equals the modulus (k=1 case), drop it
+                change = true;
+            }
+            else if (m_util.is_mul(arg, s1, s2) &&
+                     ((m_util.is_numeral(s1, k) && s2 == arg2) ||
+                      (m_util.is_numeral(s2, k) && s1 == arg2))) {
+                // k * arg2 or arg2 * k, drop it
+                change = true;
+            }
+            else {
+                new_args.push_back(arg);
+            }
+        }
+        if (change) {
+            expr_ref sum(m);
+            if (new_args.empty())
+                sum = m_util.mk_int(0);
+            else if (new_args.size() == 1)
+                sum = expr_ref(new_args[0], m);
+            else
+                sum = m.mk_app(to_app(arg1)->get_decl(), new_args.size(), new_args.data());
+            result = m_util.mk_mod(sum, arg2);
+            return BR_REWRITE3;
+        }
+    }
+
     expr* x = nullptr, * y = nullptr, * z = nullptr;
     if (is_num2 && v2.is_pos() && m_util.is_mul(arg1, x, y) && m_util.is_numeral(x, v1, is_int) && v1 > 0 && divides(v1, v2)) {
         result = m_util.mk_mul(m_util.mk_int(v1), m_util.mk_mod(y, m_util.mk_int(v2/v1)));        
diff --git a/src/test/arith_rewriter.cpp b/src/test/arith_rewriter.cpp
index fc8d503af..b50788c17 100644
--- a/src/test/arith_rewriter.cpp
+++ b/src/test/arith_rewriter.cpp
@@ -40,6 +40,8 @@ static expr_ref parse_int_fml(ast_manager& m, char const* str) {
     std::ostringstream buffer;
     buffer << "(declare-const I Int)\n"
            << "(declare-const S Int)\n"
+           << "(declare-const x Int)\n"
+           << "(declare-const y Int)\n"
            << "(assert " << str << ")\n";
     std::istringstream is(buffer.str());
     VERIFY(parse_smt2_commands(ctx, is));
@@ -83,4 +85,17 @@ void tst_arith_rewriter() {
     rw(fml);
     std::cout << "consecutive product (minus) >= 0: " << mk_pp(fml, m) << "\n";
     ENSURE(m.is_true(fml));
+
+    // Issue: (mod (+ x y) y) should simplify to (mod x y)
+    // This is the key identity: (a + k*b) mod b = a mod b
+    fml = parse_int_fml(m, "(= (mod (+ x y) y) (mod x y))");
+    rw(fml);
+    std::cout << "mod congruence (mod (+ x y) y) = (mod x y): " << mk_pp(fml, m) << "\n";
+    ENSURE(m.is_true(fml));
+
+    // (mod (+ x (* 3 y)) y) should simplify to (mod x y)
+    fml = parse_int_fml(m, "(= (mod (+ x (* 3 y)) y) (mod x y))");
+    rw(fml);
+    std::cout << "mod congruence (mod (+ x (* 3 y)) y) = (mod x y): " << mk_pp(fml, m) << "\n";
+    ENSURE(m.is_true(fml));
 }