From 996dc723007e6440ca000e5c5245e51102c2036b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Mar 2026 11:26:57 -1000 Subject: [PATCH] Fix assertion violation in isolate_roots for nested calls (#6871) 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> --- src/math/polynomial/algebraic_numbers.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 7c72ffd63..bc654b7c4 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -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) {