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

Add assertion to set() method and simplify get_sign_cell by removing redundant SMALL_INT_MIN case

Browse source 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-09 18:30:29 +00:00
parent 940910efb6
commit 46bc45d904
1 changed files with 2 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/util/mpz.h
View file

@ -185,6 +185,7 @@ public:
}
void set(int v) {
SASSERT(is_small());
m_value = static_cast<uintptr_t>(static_cast<intptr_t>(v)) << 1;
}
@ -408,20 +409,7 @@ class mpz_manager {
if (is_small(a)) {
int64_t val = a.value64();
cell = reserve;
if (val == mpz::SMALL_INT_MIN) {
sign = -1;
uint64_t abs_val = static_cast<uint64_t>(-val);
if (sizeof(digit_t) == sizeof(uint64_t)) {
cell->m_size = 1;
cell->m_digits[0] = static_cast<digit_t>(abs_val);
}
else {
cell->m_digits[0] = static_cast<unsigned>(abs_val);
cell->m_digits[1] = static_cast<unsigned>(abs_val >> 32);
cell->m_size = (abs_val >> 32) == 0 ? 1 : 2;
}
}
else if (val < 0) {
if (val < 0) {
sign = -1;
uint64_t abs_val = static_cast<uint64_t>(-val);
if (sizeof(digit_t) == sizeof(uint64_t)) {