mirror of
https://github.com/Z3Prover/z3
synced 2026-03-07 13:54:53 +00:00
cfd087293c
The identity (a - b) mod m = 0 ⟺ a mod m = b mod m is a basic number theory fact. Without this rewrite, z3 could not solve formulas like (mod (- x y) m) = 0 ∧ (mod x m) ≠ (mod y m) with symbolic m, timing out instead of returning unsat. The rewrite is added to mk_eq_mod in the arith rewriter, matching the pattern (= (mod (+ a (* -1 b)) m) 0) in both argument orders. Fixes #1618. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||