From 35986f3979405d2cbbcdee61598e01ad2a9644e8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Jun 2022 11:29:57 -0700 Subject: [PATCH] fix #6084 Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/algebraic_numbers.cpp | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 57ce00e2c..1a4769ac3 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -1466,7 +1466,10 @@ namespace algebraic_numbers { qm().add(il, nbv, il); qm().add(iu, nbv, iu); // (il, iu) is an isolating refinable (rational) interval for the new polynomial. - upm().convert_q2bq_interval(m_add_tmp.size(), m_add_tmp.data(), il, iu, bqm(), l, u); + if (!upm().convert_q2bq_interval(m_add_tmp.size(), m_add_tmp.data(), il, iu, bqm(), l, u)) { + TRACE("algebraic", tout << "conversion failed\n"); + } + } TRACE("algebraic", upm().display(tout, m_add_tmp.size(), m_add_tmp.data()); @@ -1576,7 +1579,9 @@ namespace algebraic_numbers { if (is_neg) qm().swap(il, iu); // (il, iu) is an isolating refinable (rational) interval for the new polynomial. - upm().convert_q2bq_interval(mulp.size(), mulp.data(), il, iu, bqm(), l, u); + if (!upm().convert_q2bq_interval(mulp.size(), mulp.data(), il, iu, bqm(), l, u)) { + TRACE("algebraic", tout << "conversion failed\n"); + } } TRACE("algebraic", upm().display(tout, mulp.size(), mulp.data()); @@ -1690,7 +1695,10 @@ namespace algebraic_numbers { qm().swap(inv_lower, inv_upper); TRACE("algebraic_bug", tout << "inv new_bounds: " << qm().to_string(inv_lower) << ", " << qm().to_string(inv_upper) << "\n";); // convert isolating interval back as a binary rational bound - upm().convert_q2bq_interval(cell_a->m_p_sz, cell_a->m_p, inv_lower, inv_upper, bqm(), lower(cell_a), upper(cell_a)); + if (!upm().convert_q2bq_interval(cell_a->m_p_sz, cell_a->m_p, inv_lower, inv_upper, bqm(), lower(cell_a), upper(cell_a))) { + TRACE("algebraic_bug", tout << "root isolation failed\n"); + throw algebraic_exception("inversion of algebraic number failed"); + } TRACE("algebraic_bug", tout << "after inv: "; display_root(tout, a); tout << "\n"; display_interval(tout, a); tout << "\n";); update_sign_lower(cell_a); SASSERT(acell_inv(*cell_a));