From a05520f261e5e8f2086aefb57224a49741baa4b0 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 28 Feb 2026 22:36:34 +0000
Subject: [PATCH] Guard mod rewrite rule for y=0: skip when concrete zero, use
 ite for symbolic y

Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
---
 src/ast/rewriter/arith_rewriter.cpp | 28 ++++++++++++++++++++--------
 1 file changed, 20 insertions(+), 8 deletions(-)

diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 58261c5c9..7c2fa0441 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -914,18 +914,30 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
         }
     }
     // (mod (+ a (* -1 b)) m) = 0 ==> (mod a m) = (mod b m)
+    // guarded by ite(m = 0, original, rewritten) when m is symbolic,
+    // because mod is uninterpreted for divisor 0
     if (m_util.is_mod(arg1, x, y) && m_util.is_zero(arg2) && is_add(x) && to_app(x)->get_num_args() == 2) {
         expr* a = to_app(x)->get_arg(0);
         expr* b_neg = to_app(x)->get_arg(1);
         expr* b = nullptr;
-        rational coeff;
-        if (m_util.is_mul(b_neg, z, b) && m_util.is_numeral(z, coeff) && coeff.is_minus_one()) {
-            result = m.mk_eq(m_util.mk_mod(a, y), m_util.mk_mod(b, y));
-            return true;
-        }
-        // also handle (+ (* -1 a) b) = 0
-        if (m_util.is_mul(a, z, u) && m_util.is_numeral(z, coeff) && coeff.is_minus_one()) {
-            result = m.mk_eq(m_util.mk_mod(u, y), m_util.mk_mod(b_neg, y));
+        rational coeff, yval;
+        bool y_is_numeral = m_util.is_numeral(y, yval);
+        if (y_is_numeral && yval.is_zero())
+            return false;
+        expr_ref eq(m);
+        if (m_util.is_mul(b_neg, z, b) && m_util.is_numeral(z, coeff) && coeff.is_minus_one())
+            eq = m.mk_eq(m_util.mk_mod(a, y), m_util.mk_mod(b, y));
+        else if (m_util.is_mul(a, z, u) && m_util.is_numeral(z, coeff) && coeff.is_minus_one())
+            eq = m.mk_eq(m_util.mk_mod(u, y), m_util.mk_mod(b_neg, y));
+        if (eq) {
+            if (!y_is_numeral) {
+                // guard: when y = 0, mod is uninterpreted, so keep the original constraint
+                // use concrete zero so the then-branch is not re-rewritten by this rule
+                expr_ref zero(m_util.mk_int(0), m);
+                eq = m.mk_ite(m.mk_eq(y, zero),
+                              m.mk_eq(m_util.mk_mod(x, zero), arg2), eq);
+            }
+            result = eq;
             return true;
         }
     }