From 1c4f8f17f3a9c428e69462aee92116c6b28cf6ed Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 28 Jan 2026 17:43:39 +0000 Subject: [PATCH] Improve exp_delta clamping to handle negative values symmetrically Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/util/mpf.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index a807fa007..7dd1596d6 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -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);