mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-26 22:35:46 +00:00
Code Activity

Fix crashes: avoid re-entering factor_sqf_pp from factor_n_sqf_pp

Browse source 
Calling factor_sqf_pp recursively on Hensel-lifted factors corrupts
shared mutable state in the polynomial manager, m_m2pos, m_som_buffer,
m_cheap_som_buffer, m_tmp1, etc., causing assertion violations:
  - polynomial.cpp:473 id < m_m2pos.size()
  - upolynomial.cpp:2624 sign_a == -sign_b

Use factor_1_sqf_pp/factor_2_sqf_pp for small degrees, push directly
for larger degrees. These don't conflict with the outer call's buffers.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-22 11:43:00 -10:00 • committed by Lev Nachmanson
parent 5bae864d6e
commit 09339c82ab
1 changed files with 31 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/math/polynomial/polynomial.cpp
View file

@ -7360,9 +7360,20 @@ namespace polynomial {
F2 = translate(F2, lift_var, neg_a);
if (n_eval == 0) {
// p is bivariate, factors are exact
factor_sqf_pp(F1, r, x, k, factor_params());
factor_sqf_pp(F2, r, x, k, factor_params());
// p is bivariate, factors verified by try_bivar_hensel_lift.
// Use specialized handlers for small degrees to avoid
// re-entering factor_sqf_pp which corrupts shared buffers.
polynomial_ref bivar_fs[] = { F1, F2 };
for (polynomial_ref & bf : bivar_fs) {
if (is_const(bf) || degree(bf, x) == 0) continue;
unsigned d = degree(bf, x);
if (d == 1)
factor_1_sqf_pp(bf, r, x, k);
else if (d == 2 && is_primitive(bf, x) && is_square_free(bf, x))
factor_2_sqf_pp(bf, r, x, k);
else
r.push_back(bf, k);
}
return;
}
@ -7382,11 +7393,23 @@ namespace polynomial {
polynomial_ref check(pm());
check = mul(cand, Q_div);
if (eq(check, p)) {
factor_sqf_pp(cand, r, x, k, factor_params());
if (!is_const(Q_div) && degree(Q_div, x) > 0)
factor_sqf_pp(Q_div, r, x, k, factor_params());
else if (is_const(Q_div))
acc_constant(r, Q_div->a(0));
// Push factors directly, using specialized handlers
// for small degrees only.
polynomial_ref parts[] = { cand, Q_div };
for (polynomial_ref & part : parts) {
if (is_const(part)) {
acc_constant(r, part->a(0));
continue;
}
if (degree(part, x) == 0) continue;
unsigned d = degree(part, x);
if (d == 1)
factor_1_sqf_pp(part, r, x, k);
else if (d == 2 && is_primitive(part, x) && is_square_free(part, x))
factor_2_sqf_pp(part, r, x, k);
else
r.push_back(part, k);
}
return;
}
}