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

Fix machine_div2k to not truncate when result doesn't fit in small (add assertion instead)

Browse source 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-13 13:48:38 +00:00
parent 5c61d08dc1
commit ded37fa012
1 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/util/mpz.cpp
View file

@ -2126,11 +2126,10 @@ void mpz_manager<SYNCH>::machine_div2k(mpz & a, unsigned k) {
if (k < 32) {
int64_t twok = 1ull << ((int64_t)k);
int64_t val = a.value64();
if (mpz::fits_in_small(val/twok)) {
a.set64(val/twok);
} else {
a.set((int)(val/twok));
}
int64_t result = val / twok;
// Division by power of 2 should keep us in small range
SASSERT(mpz::fits_in_small(result));
a.set64(result);
}
else if (k < 64) {
int64_t twok = 1ull << ((int64_t)k);