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>
The arith rewriter now recognizes that x * (x + 1) >= 0 for all
integers, since no integer lies strictly between -1 and 0.
Two changes:
1. is_non_negative: detect products where unpaired factors are
consecutive integer expressions (differ by exactly 1), handling
both +1 and -1 offsets and n-ary additions
2. is_separated: return true for (>= non_negative_mul 0), restricted
to multiplication expressions to avoid disrupting other theories
Also adds regression tests for the new simplification.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
