refine precision before taking closest integral value.

Z3Prover · Apr 30, 2024 · bc577b9 · bc577b9
1 parent 2ad9f22
commit bc577b9
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
@@ -2599,6 +2599,7 @@ namespace algebraic_numbers {
                 qm().dec(v);
             }
             else {
+                refine_until_prec(const_cast<numeral&>(a), 1);
                 bqm().floor(qm(), lower(a.to_algebraic()), v);
             }
             m_wrapper.set(b, v);
@@ -2611,6 +2612,7 @@ namespace algebraic_numbers {
                 qm().inc(v);
             }
             else {
+                refine_until_prec(const_cast<numeral&>(a), 1);
                 bqm().ceil(qm(), upper(a.to_algebraic()), v);
             }
             m_wrapper.set(b, v);