mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

fix #6084

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-06-07 11:29:57 -07:00
parent fe08c9976e
commit 35986f3979
1 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1466,7 +1466,10 @@ namespace algebraic_numbers {
qm().add(il, nbv, il); qm().add(il, nbv, il);
qm().add(iu, nbv, iu); qm().add(iu, nbv, iu);
// (il, iu) is an isolating refinable (rational) interval for the new polynomial. // (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", TRACE("algebraic",
upm().display(tout, m_add_tmp.size(), m_add_tmp.data()); upm().display(tout, m_add_tmp.size(), m_add_tmp.data());
@ -1576,7 +1579,9 @@ namespace algebraic_numbers {
if (is_neg) if (is_neg)
qm().swap(il, iu); qm().swap(il, iu);
// (il, iu) is an isolating refinable (rational) interval for the new polynomial. // (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", TRACE("algebraic",
upm().display(tout, mulp.size(), mulp.data()); upm().display(tout, mulp.size(), mulp.data());
@ -1690,7 +1695,10 @@ namespace algebraic_numbers {
qm().swap(inv_lower, inv_upper); qm().swap(inv_lower, inv_upper);
TRACE("algebraic_bug", tout << "inv new_bounds: " << qm().to_string(inv_lower) << ", " << qm().to_string(inv_upper) << "\n";); 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 // 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";); TRACE("algebraic_bug", tout << "after inv: "; display_root(tout, a); tout << "\n"; display_interval(tout, a); tout << "\n";);
update_sign_lower(cell_a); update_sign_lower(cell_a);
SASSERT(acell_inv(*cell_a)); SASSERT(acell_inv(*cell_a));