From d0cf1458e3023ea62d1bf9e4288078662d944fe6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Oct 2019 04:12:06 -0700 Subject: [PATCH] fix #2630 Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/algebraic_numbers.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index ebe45ddfc..3a5fba27c 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -125,7 +125,8 @@ namespace algebraic_numbers { } bool acell_inv(algebraic_cell const& c) { - return c.m_sign_lower == (upm().eval_sign_at(c.m_p_sz, c.m_p, lower(&c)) == polynomial::sign_neg); + auto s = upm().eval_sign_at(c.m_p_sz, c.m_p, lower(&c)); + return s == polynomial::sign_zero || c.m_sign_lower == (s == polynomial::sign_neg); } void checkpoint() {