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 undefined behavior when negating SMALL_INT_MIN in power_of_two_multiple

Browse source 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-13 16:48:50 +00:00
parent f9ec57947c
commit 23fe87612a
1 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/util/mpz.cpp
View file

@ -2273,7 +2273,16 @@ unsigned mpz_manager<SYNCH>::power_of_two_multiple(mpz const & a) {
if (val == 0) return 0;
// Work with absolute value for counting trailing zeros
uint64_t v = (val < 0) ? static_cast<uint64_t>(-val) : static_cast<uint64_t>(val);
// Handle SMALL_INT_MIN specially to avoid overflow
uint64_t v;
if (val == mpz::SMALL_INT_MIN) {
// SMALL_INT_MIN = -2^(SMALL_BITS-1), so it has (SMALL_BITS-1) trailing zeros
return mpz::SMALL_BITS - 1;
} else if (val < 0) {
v = static_cast<uint64_t>(-val);
} else {
v = static_cast<uint64_t>(val);
}
if ((v & 0xFFFFFFFF) == 0) {
r += 32;