From c808f7459163f372d92de177f3afdb3a21b96ace Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 12 Feb 2021 11:53:40 -0800
Subject: [PATCH] fix multiplier base for #5022

add also some C++ API shorthands for retrieving numerals
---
 src/api/c++/z3++.h | 5 +++++
 src/util/mpz.cpp   | 4 ++--
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 8b175a15c..91ba0c02a 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -825,6 +825,11 @@ namespace z3 {
         bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
         bool as_binary(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
 
+        double as_double() const { double d = 0; is_numeral(d); return d; }
+        uint64_t as_uint64() const { uint64_t r = 0; is_numeral_u64(r); return r; }
+        uint64_t as_int64() const { int64_t r = 0; is_numeral_i64(r); return r; }
+        
+
         /**
            \brief Return true if this expression is an application.
         */
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 17db5a227..8e08560d7 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1682,9 +1682,9 @@ double mpz_manager<SYNCH>::get_double(mpz const & a) const {
     for (unsigned i = 0; i < sz; i++) {
         r += d * static_cast<double>(digits(a)[i]);
         if (sizeof(digit_t) == sizeof(uint64_t))
-            d *= static_cast<double>(UINT64_MAX); // 64-bit version
+            d *= (1.0 + static_cast<double>(UINT64_MAX)); // 64-bit version, multiply by 2^64
         else
-            d *= static_cast<double>(UINT_MAX);   // 32-bit version
+            d *= (1.0 + static_cast<double>(UINT_MAX));   // 32-bit version, multiply by 2^32
     }
     if (!(r >= 0.0)) {
         r = static_cast<double>(UINT64_MAX); // some large number