From bc577b93ae3e88e2e34443b68aca66491f5efe03 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 30 Apr 2024 16:58:22 -0700
Subject: [PATCH] refine precision before taking closest integral value.

---
 src/math/polynomial/algebraic_numbers.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 06b4465d7..a10e0dc98 100644
--- 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);