mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 18:40:51 +00:00
Code Activity

Fix assertion violation in mpf.cpp by clamping exp_delta to safe range

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:35:20 +00:00
parent 02b50068cc
commit 88d3488559
1 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/util/mpf.cpp
View file

@ -1365,7 +1365,15 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
scoped_mpz X_YQ_sig(m_mpz_manager);
mpf_exp_t exp_delta = exp(x) - YQ_exp;
TRACE(mpf_dbg_rem, tout << "exp_delta=" << exp_delta << std::endl;);
SASSERT(INT_MIN < exp_delta && exp_delta <= INT_MAX);
// 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
if (exp_delta > INT_MAX)
exp_delta = INT_MAX;
else if (exp_delta < INT_MIN)
exp_delta = INT_MIN + 1;
scoped_mpz minuend(m_mpz_manager), subtrahend(m_mpz_manager);
scoped_mpz x_sig_lrg(m_mpz_manager);