mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 10:35:36 +00:00
Code Activity

Improve exp_delta clamping to handle negative values symmetrically

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-28 17:43:39 +00:00
parent 8ab64672f3
commit 1c4f8f17f3
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/util/mpf.cpp
View file

@ -1368,11 +1368,11 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
// Clamp exp_delta to safe range for casting to int/unsigned
// When exp_delta > INT_MAX, it will trigger the exp_delta > sbits+5 branch
// When exp_delta < INT_MIN, clamp it to prevent overflow when negating
// When exp_delta is very negative, cap it to avoid extremely large multiplications
if (exp_delta > INT_MAX)
exp_delta = INT_MAX;
else if (exp_delta < INT_MIN)
exp_delta = INT_MIN + 1;
else if (exp_delta < -(sbits + 5))
exp_delta = -(sbits + 5); // Cap negative values symmetrically
scoped_mpz minuend(m_mpz_manager), subtrahend(m_mpz_manager);