mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 11:35:42 +00:00
Code Activity

Fix Windows ARM64 overflow detection build

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-15 05:12:57 +00:00 • committed by GitHub
parent 468a1cb658
commit 685ca67c64
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 23 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/util/mpz.cpp
View file

@ -31,12 +31,33 @@ static bool mul_overflows(int64_t a, int64_t b, int64_t & result) {
return std::ckd_mul(&result, a, b);
#elif defined(__GNUC__)
return __builtin_mul_overflow(a, b, &result);
#elif defined(_MSC_VER)
// MSVC _mul128 intrinsic
#elif defined(_MSC_VER) && !defined(_M_ARM64)
// MSVC _mul128 intrinsic is unavailable when targeting ARM64.
__int64 high;
result = _mul128(a, b, &high);
// Overflow if high bits are not the sign extension of result
return high != (result >> 63);
#elif defined(_MSC_VER)
if (a > 0) {
if (b > 0) {
if (a > INT64_MAX / b)
return true;
}
else if (b < INT64_MIN / a) {
return true;
}
}
else if (a < 0) {
if (b > 0) {
if (a < INT64_MIN / b)
return true;
}
else if (b < 0 && b < INT64_MAX / a) {
return true;
}
}
result = a * b;
return false;
#else
static_assert(false);
#endif