From fe2ceab7b5bfacc9d3b242648dd5124f3c910beb Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 7 Mar 2026 00:02:37 +0000 Subject: [PATCH] Address code review: rename r_val->r, add comment for <= 0 break condition Co-authored-by: levnach <5377127+levnach@users.noreply.github.com> --- src/util/mpz.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 98570269a..2b86abb26 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -1141,8 +1141,8 @@ void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { SASSERT(ge(a1, b1)); if (is_small(b1)) { if (is_small(a1)) { - unsigned r_val = u_gcd(a1.m_val, b1.m_val); - set(c, r_val); + unsigned r = u_gcd(a1.m_val, b1.m_val); + set(c, r); break; } else { @@ -1196,6 +1196,10 @@ void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { A = 1; B = 0; C = 0; D = 1; while (true) { + // Break if either denominator is zero or negative. + // With signed 64-bit approximations, cofactors C and D can + // become large negative values; a non-positive denominator + // would produce a wrong quotient and must be avoided. if (b_hat + C <= 0 || b_hat + D <= 0) break; q = (a_hat + A) / (b_hat + C);