From 03c1b24dea7a5eec1747968a829ae7e014aa4809 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 8 Apr 2013 14:25:25 -0700
Subject: [PATCH] Fix get_int64 and is_int64 methods in mpz. Fix INT64_MAX
 constant definition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/mpz.cpp | 15 ++++-----------
 src/util/mpz.h   | 24 ++++++++++++++++++++++++
 src/util/util.h  |  2 +-
 3 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index c77978647..9473621cf 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1299,9 +1299,9 @@ bool mpz_manager<SYNCH>::is_int64(mpz const & a) const {
     if (is_small(a))
         return true;
 #ifndef _MP_GMP
-    if (!is_uint64(a)) 
+    if (!is_abs_uint64(a)) 
         return false;
-    uint64 num = get_uint64(a);
+    uint64 num = big_abs_to_uint64(a);
     uint64 msb = static_cast<uint64>(1) << 63;
     uint64 msb_val = msb & num;
     if (a.m_val >= 0) {
@@ -1327,14 +1327,7 @@ uint64 mpz_manager<SYNCH>::get_uint64(mpz const & a) const {
         return static_cast<uint64>(a.m_val);
 #ifndef _MP_GMP
     SASSERT(a.m_ptr->m_size > 0);
-    if (a.m_ptr->m_size == 1)
-        return digits(a)[0];
-    if (sizeof(digit_t) == sizeof(uint64))
-        // 64-bit machine
-        return digits(a)[0];
-    else 
-        // 32-bit machine
-        return ((static_cast<uint64>(digits(a)[1]) << 32) | (static_cast<uint64>(digits(a)[0])));
+    return big_abs_to_uint64(a);
 #else
     // GMP version
     if (sizeof(uint64) == sizeof(unsigned long)) {
@@ -1359,7 +1352,7 @@ int64 mpz_manager<SYNCH>::get_int64(mpz const & a) const {
         return static_cast<int64>(a.m_val);
 #ifndef _MP_GMP
     SASSERT(is_int64(a));
-    uint64 num = get_uint64(a);
+    uint64 num = big_abs_to_uint64(a);
     if (a.m_val < 0) {
         if (num != 0 && (num << 1) == 0)
             return INT64_MIN;
diff --git a/src/util/mpz.h b/src/util/mpz.h
index b5c301d82..7b40a89f5 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -211,6 +211,30 @@ class mpz_manager {
 
     static digit_t * digits(mpz const & c) { return c.m_ptr->m_digits; }
 
+    // Return true if the absolute value fits in a UINT64
+    static bool is_abs_uint64(mpz const & a) {
+        if (is_small(a))
+            return true;
+        if (sizeof(digit_t) == sizeof(uint64))
+            return size(a) <= 1;
+        else
+            return size(a) <= 2;
+    }
+    
+    // CAST the absolute value into a UINT64
+    static uint64 big_abs_to_uint64(mpz const & a) {
+        SASSERT(is_abs_uint64(a));
+        SASSERT(!is_small(a));
+        if (a.m_ptr->m_size == 1)
+            return digits(a)[0];
+        if (sizeof(digit_t) == sizeof(uint64))
+            // 64-bit machine
+            return digits(a)[0];
+        else 
+            // 32-bit machine
+            return ((static_cast<uint64>(digits(a)[1]) << 32) | (static_cast<uint64>(digits(a)[0])));
+    }
+
     template<int IDX>
     void get_sign_cell(mpz const & a, int & sign, mpz_cell * & cell) {
         if (is_small(a)) {
diff --git a/src/util/util.h b/src/util/util.h
index 8bcbce4a3..0aa8f881d 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -45,7 +45,7 @@ COMPILE_TIME_ASSERT(sizeof(int64) == 8);
 #define INT64_MIN static_cast<int64>(0x8000000000000000ull)
 #endif
 #ifndef INT64_MAX
-#define INT64_MAX static_cast<int64>(0x0fffffffffffffffull)
+#define INT64_MAX static_cast<int64>(0x7fffffffffffffffull)
 #endif                              
 #ifndef UINT64_MAX
 #define UINT64_MAX 0xffffffffffffffffull