Fix non-termination in mod rewriter for symbolic modulus (#10105)

Combining `mod0`/`div0` quantifier axioms with a mod-idempotency
quantifier caused Z3 to loop forever. The core issue was that
`mk_mod_core` in `arith_rewriter.cpp` only handled rewrite rules for
*numeral* moduli, leaving two gaps for symbolic `y`:

1. `mod(a + k*y, y)` was not reduced to `mod(a, y)`, so `(not (= (mod (+
a b) b) (mod a b)))` stayed unreduced and caused the nlsat solver to
spin.
2. The E-matching pattern `(mod (mod x y) y)` fired on every new term it
produced, creating an unbounded chain of nested `mod` expressions.

```lisp
; Previously non-terminating, now returns unsat immediately
(assert (forall ((x Int)) (! (= (mod0 x 0) 0) :pattern ((mod0 x 0)))))
(assert (forall ((x Int)) (! (= (div0 x 0) 0) :pattern ((div0 x 0)))))
(assert (forall ((x Int) (y Int))
  (! (= (mod (mod x y) y) (mod x y)) :pattern ((mod (mod x y) y)))))
(assert (not (= (mod (+ a b) b) (mod a b))))
(check-sat)
```

## Changes

- **`src/ast/rewriter/arith_rewriter.cpp` — symbolic summand
elimination**: In `mk_mod_core`, when the modulus is a non-numeral
integer and the dividend is an `add`, strip any summand equal to the
modulus or an integer multiple of it. Soundness: `k*0 = 0` for all `k`,
so the rule holds even at `y = 0`. This immediately collapses the
reported formula to `false`.

- **`src/ast/rewriter/arith_rewriter.cpp` — symbolic idempotency via
ite**: Extend the existing `mod(mod(x,y), y) → mod(x,y)` rule
(previously numeral-only) to symbolic `y` by rewriting to `ite(y=0,
mod(mod(x,0),0), mod(x,y))`. The `y=0` branch uses a numeral divisor,
which is excluded by the `!v2.is_zero()` guard, halting the E-matching
chain.

- **`src/test/arith_rewriter.cpp`**: Regression tests for `mod(a+y, y) =
mod(a,y)`, `mod(a+2y, y) = mod(a,y)`, and `mod(mod(a,3),3) = mod(a,3)`.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>

src/ast/rewriter/arith_rewriter.cpp

@@ -1430,9 +1430,21 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
 
     // mod is idempotent on non-zero modulus.
     expr* t1, *t2;
-    if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && is_num2 && is_int && !v2.is_zero()) {
-        result = arg1;
-        return BR_DONE;
+    if (m_util.is_mod(arg1, t1, t2) && t2 == arg2) {
+        if (is_num2 && is_int && !v2.is_zero()) {
+            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, 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),
+                              m_util.mk_mod(m_util.mk_mod(t1, zero), zero),
+                              arg1);
+            return BR_REWRITE2;
+        }
     }
 
     // propagate mod inside only if there is something to reduce.
@@ -1465,6 +1477,44 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
         }
     }
 
+    // For symbolic modulus: remove summands that are multiples of the modulus.
+    // mod (a + k*y) y = mod a y  (valid for all y, including y=0 since k*0 = 0).
+    if (!is_num2 && m_util.is_int(arg2) && is_add(arg1)) {
+        expr_ref_buffer args(m);
+        bool change = false;
+        for (expr* arg : *to_app(arg1)) {
+            if (arg == arg2) {
+                // summand equals the modulus y: drop it (y ≡ 0 mod y for all y)
+                change = true;
+            }
+            else if (m_util.is_mul(arg, t1, t2)) {
+                rational coeff;
+                if ((m_util.is_numeral(t1, coeff) && t2 == arg2) ||
+                    (m_util.is_numeral(t2, coeff) && t1 == arg2)) {
+                    // summand is k*y for some numeral k: drop it
+                    change = true;
+                }
+                else {
+                    args.push_back(arg);
+                }
+            }
+            else {
+                args.push_back(arg);
+            }
+        }
+        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
+                new_arg1 = m_util.mk_add(args.size(), args.data());
+            result = m_util.mk_mod(new_arg1, 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)));        

src/test/arith_rewriter.cpp

@@ -83,4 +83,23 @@ void tst_arith_rewriter() {
     rw(fml);
     std::cout << "consecutive product (minus) >= 0: " << mk_pp(fml, m) << "\n";
     ENSURE(m.is_true(fml));
+
+    // 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+y) y = mod a y: " << mk_pp(fml, m) << "\n";
+    ENSURE(m.is_true(fml));
+
+    // 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+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
+    fml = parse_int_fml(m, "(= (mod (mod I 3) 3) (mod I 3))");
+    rw(fml);
+    std::cout << "mod (mod a 3) 3 = mod a 3: " << mk_pp(fml, m) << "\n";
+    ENSURE(m.is_true(fml));
 }