fix #4905

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 18, 2020 · fa5567f · fa5567f
1 parent 727095c
commit fa5567f
Showing 1 changed file with 5 additions and 0 deletions.
diff --git 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);
         }