From fa5567fa1fb3c0c687b495d6f67257e17c573424 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Dec 2020 14:00:05 -0800 Subject: [PATCH] fix #4905 Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 3619a142a..23a583702 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -196,6 +196,11 @@ namespace api { } e = m_datalog_util.mk_numeral(n.get_uint64(), s); } + else if (fid == m_fpa_fid) { + scoped_mpf tmp(fpautil().fm()); + fpautil().fm().set(tmp, fpautil().get_ebits(s), fpautil().get_sbits(s), n.get_double()); + e = fpautil().mk_value(tmp); + } else { invoke_error_handler(Z3_INVALID_ARG); }