mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-16 20:15:43 +00:00
Code Activity

Fix MSVC mul_overflows sign extension check

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-15 05:36:17 +00:00 • committed by GitHub
parent 4c8c511b40
commit e22487e8c4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/util/mpz.cpp
View file

@ -20,6 +20,9 @@ Revision History:
#include <numeric>
#include <sstream>
#include <iomanip>
#if defined(_MSC_VER)
#include <intrin.h>
#endif
#include "util/mpz.h"
#include "util/buffer.h"
#include "util/trace.h"
@ -36,7 +39,7 @@ static bool mul_overflows(int64_t a, int64_t b, int64_t & result) {
__int64 high;
result = _mul128(a, b, &high);
// Overflow if high bits are not the sign extension of result
return high != (result >> 63);
return high != (result < 0 ? -1 : 0);
#elif defined(_MSC_VER)
// Extract magnitudes without ever evaluating -INT64_MIN.
uint64_t x = a < 0 ? static_cast<uint64_t>(-(a + 1)) + 1 : static_cast<uint64_t>(a);