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) {