3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00

throw an algebraic exception on a failure of m_limit.inc() instead of returning sign_zero

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-14 07:17:13 -10:00
parent 888d2fc480
commit ece691285e

View file

@ -1821,7 +1821,7 @@ namespace algebraic_numbers {
}
if (!m_limit.inc())
return sign_zero;
throw algebraic_exception(m_limit.get_cancel_msg());
// make sure that intervals of a and b have the same magnitude
int a_m = magnitude(a_lower, a_upper);