mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #4110

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-26 14:13:58 -07:00
parent d3094291d3
commit dc852a6f83
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -292,7 +292,7 @@ namespace algebraic_numbers {
return false; // we know for sure a is not a rational return false; // we know for sure a is not a rational
TRACE("algebraic_bug", tout << "is_rational(a):\n"; display_root(tout, a); tout << "\n"; display_interval(tout, a); tout << "\n";); TRACE("algebraic_bug", tout << "is_rational(a):\n"; display_root(tout, a); tout << "\n"; display_interval(tout, a); tout << "\n";);
algebraic_cell * c = a.to_algebraic(); algebraic_cell * c = a.to_algebraic();
save_intervals saved_a(*this, c); save_intervals saved_a(*this, a);
mpz & a_n = c->m_p[c->m_p_sz - 1]; mpz & a_n = c->m_p[c->m_p_sz - 1];
scoped_mpz & abs_a_n = m_is_rational_tmp; scoped_mpz & abs_a_n = m_is_rational_tmp;
qm().set(abs_a_n, a_n); qm().set(abs_a_n, a_n);
@ -965,6 +965,7 @@ namespace algebraic_numbers {
if (m_num.is_basic()) if (m_num.is_basic())
return; // m_num is not algebraic anymore return; // m_num is not algebraic anymore
algebraic_cell * cell = m_num.to_algebraic(); algebraic_cell * cell = m_num.to_algebraic();
if (m_owner.magnitude(cell) < m_owner.m_min_magnitude) { if (m_owner.magnitude(cell) < m_owner.m_min_magnitude) {
// restore old interval // restore old interval
m_owner.bqim().swap(cell->m_interval, m_old_interval); m_owner.bqim().swap(cell->m_interval, m_old_interval);