From 89ed19a7196f9201d61d9995b1ba503003cdc3b9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Jul 2021 11:20:16 -0700
Subject: [PATCH] #5420

---
 src/sat/smt/fpa_solver.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
index 3589c37c8..42e3f8726 100644
--- a/src/sat/smt/fpa_solver.cpp
+++ b/src/sat/smt/fpa_solver.cpp
@@ -312,7 +312,9 @@ namespace fpa {
             if (!wrapped) wrapped = m_converter.wrap(e);
             return expr2enode(wrapped) != nullptr;
         };
-        if (m_fpa_util.is_fp(e)) {
+        if (m_fpa_util.is_rm_numeral(e) || m_fpa_util.is_numeral(e)) 
+            value = e;
+        else if (m_fpa_util.is_fp(e)) {
             SASSERT(n->num_args() == 3);
             expr* a = values.get(n->get_arg(0)->get_root_id());
             expr* b = values.get(n->get_arg(1)->get_root_id());