mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 22:04:53 +00:00
Code Activity

Address code review: rename r_val->r, add comment for <= 0 break condition

Browse source 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-07 00:02:37 +00:00
parent fe9b246624
commit fe2ceab7b5
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/util/mpz.cpp
View file

@ -1141,8 +1141,8 @@ void mpz_manager<SYNCH>::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<SYNCH>::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);