mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-14 04:41:48 +00:00
Code Activity

Fix uses of value() that should be value64() for 64-bit small integers

Browse source 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-10 22:47:15 +00:00
parent f2ae873fde
commit 2f9e5581e2
1 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/util/mpz.cpp
View file

@ -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();