diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 363d562c4f..b22ce62738 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -1435,8 +1435,9 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
             result = arg1;
             return BR_DONE;
         }
-        // Symbolic modulus: mod (mod x y) y = ite(y = 0, mod (mod x 0) 0, mod x y).
-        // Valid for all y: for y != 0, idempotency holds; for y = 0, both sides are mod0(mod0(x,0),0).
+        // Symbolic modulus: mod (mod x y) y → ite(y = 0, mod (mod x 0) 0, mod x y).
+        // Valid for all y: for y != 0, idempotency holds, returning mod x y (arg1);
+        // for y = 0, both sides evaluate to mod0(mod0(x,0),0).
         if (!is_num2 && m_util.is_int(arg2)) {
             expr_ref zero(m_util.mk_int(0), m);
             result = m.mk_ite(m.mk_eq(arg2, zero),
@@ -1503,6 +1504,8 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
         }
         if (change) {
             expr_ref new_arg1(m);
+            // When all summands are multiples of the modulus, the sum reduces to 0.
+            // mod(0, y) will be further simplified by subsequent rewrites.
             if (args.empty())
                 new_arg1 = m_util.mk_int(0);
             else
diff --git a/src/test/arith_rewriter.cpp b/src/test/arith_rewriter.cpp
index 47730e8424..0c098fc927 100644
--- a/src/test/arith_rewriter.cpp
+++ b/src/test/arith_rewriter.cpp
@@ -84,17 +84,17 @@ void tst_arith_rewriter() {
     std::cout << "consecutive product (minus) >= 0: " << mk_pp(fml, m) << "\n";
     ENSURE(m.is_true(fml));
 
-    // Issue #7403: mod (a + b) b should simplify to mod a b for symbolic b
+    // Issue #7403: mod (a + y) y should simplify to mod a y for symbolic y
     // i.e. (= (mod (+ I S) S) (mod I S)) should reduce to true
     fml = parse_int_fml(m, "(= (mod (+ I S) S) (mod I S))");
     rw(fml);
-    std::cout << "mod (a+b) b = mod a b: " << mk_pp(fml, m) << "\n";
+    std::cout << "mod (a+y) y = mod a y: " << mk_pp(fml, m) << "\n";
     ENSURE(m.is_true(fml));
 
-    // mod (a + 2*b) b should simplify to mod a b (multiple of modulus dropped)
+    // mod (a + 2*y) y should simplify to mod a y (multiple of modulus dropped)
     fml = parse_int_fml(m, "(= (mod (+ I (* 2 S)) S) (mod I S))");
     rw(fml);
-    std::cout << "mod (a+2b) b = mod a b: " << mk_pp(fml, m) << "\n";
+    std::cout << "mod (a+2y) y = mod a y: " << mk_pp(fml, m) << "\n";
     ENSURE(m.is_true(fml));
 
     // mod (mod a b) b should simplify for non-zero numeral b