mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 13:54:53 +00:00
Code Activity

Fix set_big_i64/set_big_ui64 zero handling: zero is always represented as small

Browse source 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-16 09:09:18 +00:00 • committed by Nuno Lopes
parent 957ba91fa6
commit cc7902ac50
1 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/util/mpz.h
View file

@ -605,7 +605,11 @@ public:
void set(mpz & a, unsigned val) { set(a, (uint64_t)val); }
void set(mpz & a, int64_t val) {
if (mpz::fits_in_small(val) && is_small(a)) {
if (val == 0) {
// Zero is always represented as small
reset(a);
}
else if (mpz::fits_in_small(val) && is_small(a)) {
a.set(val);
}
else {
@ -614,7 +618,11 @@ public:
}
void set(mpz & a, uint64_t val) {
if (mpz::fits_in_small(val) && is_small(a)) {
if (val == 0) {
// Zero is always represented as small
reset(a);
}
else if (mpz::fits_in_small(val) && is_small(a)) {
a.set(static_cast<int64_t>(val));
}
else {