diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 6aba9f842..c944200cf 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -765,7 +765,30 @@ extern "C" {
         mpqm.display_decimal(ss, q, sbits);
         return mk_c(c)->mk_external_string(ss.str());
         Z3_CATCH_RETURN("");
+    }
 
+    Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
+        fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
+        scoped_mpf val(mpfm);
+        bool r = plugin->is_numeral(to_expr(t), val);
+        if (!r) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        const mpz & z = mpfm.sig(val);
+        if (!mpzm.is_uint64(z)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        *n = mpzm.get_uint64(z);
+        return 1;
+        Z3_CATCH_RETURN(0);
     }
 
     Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index e1bd67d66..01908e358 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -858,6 +858,20 @@ extern "C" {
     */
     Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
 
+    /**
+    \brief Return the significand value of a floating-point numeral as a uint64.
+
+    \param c logical context
+    \param t a floating-point numeral
+
+    Remarks: This function extracts the significand bits in `t`, without the 
+    hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the 
+    signicand does not fit into a uint64.
+
+    def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n);
+
     /**
         \brief Return the exponent value of a floating-point numeral as a string