mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 05:44:51 +00:00
Code Activity

Fix soundness bug: guard mod rewrite with ite when modulus is symbolic or zero

Browse source 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-28 22:51:58 +00:00
parent 0960af405e
commit cc5e5e062b
1 changed files with 23 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/ast/rewriter/arith_rewriter.cpp
View file

@ -913,19 +913,39 @@ 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)
// (mod (+ a (* -1 b)) m) = 0 ==> (mod a m) = (mod b m) when m != 0
// when m is symbolic, guard with ite(m = 0, original, rewritten) for soundness
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;
bool y_is_numeral = m_util.is_numeral(y, p);
if (y_is_numeral && p.is_zero())
return false;
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));
expr_ref rewritten(m.mk_eq(m_util.mk_mod(a, y), m_util.mk_mod(b, y)), m);
if (y_is_numeral)
result = rewritten;
else {
// use mk_int(0) as the modulus in the then-branch so the zero-guard
// in mk_eq_mod stops recursion when the rewriter normalizes the ite
expr_ref zero(m_util.mk_int(0), m);
expr_ref then_branch(m.mk_eq(m_util.mk_mod(x, zero), zero), m);
result = m.mk_ite(m.mk_eq(y, zero), then_branch, rewritten);
}
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));
expr_ref rewritten(m.mk_eq(m_util.mk_mod(u, y), m_util.mk_mod(b_neg, y)), m);
if (y_is_numeral)
result = rewritten;
else {
expr_ref zero(m_util.mk_int(0), m);
expr_ref then_branch(m.mk_eq(m_util.mk_mod(x, zero), zero), m);
result = m.mk_ite(m.mk_eq(y, zero), then_branch, rewritten);
}
return true;
}
}