From 2f9e5581e250fa6ac4d15299e5510733ee7fa6b0 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 10 Feb 2026 22:47:15 +0000
Subject: [PATCH] Fix uses of value() that should be value64() for 64-bit small
 integers

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
---
 src/util/mpz.cpp | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index b877c700b..b807c5886 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1121,7 +1121,7 @@ void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
             SASSERT(ge(a1, b1));
             if (is_small(b1)) {
                 if (is_small(a1)) {
-                    unsigned r = u_gcd(a1.value(), b1.value());
+                    uint64_t r = u64_gcd(static_cast<uint64_t>(a1.value64()), static_cast<uint64_t>(b1.value64()));
                     set(c, r);
                     break;
                 }
@@ -1401,7 +1401,7 @@ void mpz_manager<SYNCH>::bitwise_or(mpz const & a, mpz const & b, mpz & c) {
     SASSERT(is_nonneg(b));
     TRACE(mpz, tout << "is_small(a): " << is_small(a) << ", is_small(b): " << is_small(b) << "\n";);
     if (is_small(a) && is_small(b)) {
-        c.set(a.value() | b.value());
+        c.set64(a.value64() | b.value64());
     }
     else {
 #ifndef _MP_GMP
@@ -1446,7 +1446,7 @@ void mpz_manager<SYNCH>::bitwise_and(mpz const & a, mpz const & b, mpz & c) {
     SASSERT(is_nonneg(a));
     SASSERT(is_nonneg(b));
     if (is_small(a) && is_small(b)) {
-        c.set(a.value() & b.value());
+        c.set64(a.value64() & b.value64());
     }
     else {
 #ifndef _MP_GMP
@@ -2336,11 +2336,16 @@ template<bool SYNCH>
 unsigned mpz_manager<SYNCH>::mlog2(mpz const & a) {
     if (is_nonneg(a))
         return 0;
-    if (is_small(a) && a.value() == INT_MIN)
-        return ::log2((unsigned)a.value());
-        
-    if (is_small(a))
-        return ::log2((unsigned)-a.value());
+    if (is_small(a)) {
+        int64_t v = a.value64();
+        if (v == mpz::SMALL_INT_MIN) {
+            // Special case: negating SMALL_INT_MIN would overflow
+            // For 32-bit: SMALL_INT_MIN = -2^30, so log2(2^30) = 30
+            // For 64-bit: SMALL_INT_MIN = -2^62, so log2(2^62) = 62
+            return mpz::SMALL_BITS - 1;
+        }
+        return uint64_log2(static_cast<uint64_t>(-v));
+    }
 #ifndef _MP_GMP
     static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");
     mpz_cell * c     = a.ptr();