Upgrade internal Lehmer GCD to 2-digit (64-bit) approximation

[Copilot]

Z3's internal big-integer GCD (used when building without libgmp) used a 1-digit (32-bit) Lehmer approximation, limiting each outer matrix application to ~30 simulated Euclidean steps. This upgrades to 2-digit (64-bit) approximations, roughly doubling the simulation depth per iteration and halving the number of expensive big-integer operations.

Changes (src/util/mpz.cpp)

• 2-digit approximation: Build â/b̂ from the top two 32-bit digits combined into a 62-bit int64_t (shifted right by 2 to preserve sign bit headroom), vs. the previous single leading digit:

  // Before: 32-bit approximation
  a_hat = a1.m_ptr->m_digits[a_sz - 1];
  
  // After: 62-bit approximation from top two digits
  uint64_t ah = (uint64_t)a1.m_ptr->m_digits[a_sz - 1];
  uint64_t al = (a_sz >= 2) ? (uint64_t)a1.m_ptr->m_digits[a_sz - 2] : 0;
  a_hat = (int64_t)(((ah << 32) | al) >> 2);

• Overflow safety via __int128: Cofactor products (q·C, q·D) can overflow int64_t with 62-bit approximations. Uses __int128 arithmetic with an explicit overflow check on GCC/Clang; exits the inner loop safely if overflow is detected.

• b_sz == a_sz - 1 alignment: When b1 has one fewer digit than a1, its leading digit is placed in the lower 32 bits of the 64-bit window to maintain correct relative scale.

• <= 0 break condition: The denominator check is upgraded from == 0 to <= 0; with signed 64-bit cofactors, a negative denominator is equally invalid.

• 1-digit fallback: The original 32-bit path is preserved under #else for MSVC and other compilers without __int128.

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.

[levnach]

According to the test at http://mtzguido.tplinkdns.com:8081/z3/compare_stats.html the new algorithm does not improve, but keep performance the same. Try to improve performance by improving the implementation of the new GCD algorithm, or try another method.