From: Gereon Kremer <gkremer@stanford.edu>
Date: Sat, 4 Dec 2021 01:40:40 +0000 (-0800)
Subject: More robust fix for 32bit issues. (#7735)
X-Git-Tag: cvc5-1.0.0~725
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=930256658ba51dd20a0aaaf4077d1b9e8f032ad8;p=cvc5.git

More robust fix for 32bit issues. (#7735)

This PR implements a more robust fix for the 32bit issues with GMP. Relying on mpz_sizeinbase proves to be very tricky for the corner cases. This PR instead does a simple comparison against the min and max values of the respective types.
---

diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index f1d927d09..8d9f7d050 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -460,13 +460,17 @@ int64_t Integer::getSigned64() const
     {
       return getLong();
     }
-    // ensure there is no overflow.
-    // mpz_sizeinbase ignores the sign bit, thus at most 63 bits.
-    CheckArgument(mpz_sizeinbase(d_value.get_mpz_t(), 2) < 64,
-                  this,
-                  "Overflow detected in Integer::getSigned64().");
-    return std::stoll(toString());
+    try
+    {
+      return std::stoll(toString());
+    }
+    catch (const std::exception& e)
+    {
+      CheckArgument(
+          false, this, "Overflow detected in Integer::getSigned64().");
+    }
   }
+  return 0;
 }
 uint64_t Integer::getUnsigned64() const
 {
@@ -480,12 +484,19 @@ uint64_t Integer::getUnsigned64() const
     {
       return getUnsignedLong();
     }
-    // ensure there isn't overflow
-    CheckArgument(mpz_sizeinbase(d_value.get_mpz_t(), 2) <= 64,
-                  this,
-                  "Overflow detected in Integer::getUnsigned64().");
-    return std::stoull(toString());
+    try
+    {
+      CheckArgument(
+          sgn() >= 0, this, "Overflow detected in Integer::getUnsigned64().");
+      return std::stoull(toString());
+    }
+    catch (const std::exception& e)
+    {
+      CheckArgument(
+          false, this, "Overflow detected in Integer::getUnsigned64().");
+    }
   }
+  return 0;
 }
 
 size_t Integer::hash() const { return gmpz_hash(d_value.get_mpz_t()); }