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