mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 06:07:46 +00:00
Code Activity

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

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-14 07:17:13 -10:00 • committed by Nikolaj Bjorner
parent a3440f1567
commit 8266de787c
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1821,7 +1821,7 @@ namespace algebraic_numbers {
} }
if (!m_limit.inc()) 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 // make sure that intervals of a and b have the same magnitude
int a_m = magnitude(a_lower, a_upper); int a_m = magnitude(a_lower, a_upper);