mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-22 12:38:52 +00:00
Code Activity

Fix assertion violation in isolate_roots for nested calls (#6871)

Browse source 
resultant vanishes during a nested isolate_roots call. The mathematical
invariant that the resultant cannot vanish again after recovery does not
hold in all cases, e.g. with certain nonlinear real arithmetic formulas.

The algebraic_exception propagates cleanly through the nlsat solver and
tactic layers which already catch z3_exception.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-19 11:26:57 -10:00
parent 47cbc746b5
commit 996dc72300
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polynomial/algebraic_numbers.cpp
View file

@ -2620,7 +2620,8 @@ namespace algebraic_numbers {
TRACE(isolate_roots, tout << "resultant loop i: " << i << ", y: x" << y << "\np_y: " << p_y << "\n";
tout << "q: " << q << "\n";);
if (ext_pm.is_zero(q)) {
SASSERT(!nested_call);
if (nested_call)
throw algebraic_exception("resultant vanished during nested isolate_roots call");
break;
}
}
@ -2632,7 +2633,8 @@ namespace algebraic_numbers {
// until we find one that is not zero at x2v.
// In the process we will copy p_prime to the local polynomial manager, since we will need to create
// an auxiliary variable.
SASSERT(!nested_call);
if (nested_call)
throw algebraic_exception("resultant vanished during nested isolate_roots call");
unsigned n = ext_pm.degree(p_prime, x);
SASSERT(n > 0);
if (n == 1) {