From cfd087293c885b637c807d73476a65912f8f2f0f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 28 Feb 2026 12:00:24 -1000 Subject: [PATCH] Add rewrite rule: (mod (- a b) m) = 0 ==> (mod a m) = (mod b m) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- src/ast/rewriter/arith_rewriter.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 6fb848b5d..58261c5c9 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -913,6 +913,22 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) { return true; } } + // (mod (+ a (* -1 b)) m) = 0 ==> (mod a m) = (mod b m) + 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)); + return true; + } + } return false; }