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

Revert "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 11:16:34 +00:00 • committed by Nuno Lopes
parent cc7902ac50
commit c01062e93b
1 changed files with 2 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/util/mpz.h
View file

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