mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

another fix for #1288

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-08 15:47:06 -07:00
parent d2ec927844
commit f359f23885
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/util/mpz.cpp
View file

@ -558,14 +558,13 @@ void mpz_manager<SYNCH>::big_rem(mpz const & a, mpz const & b, mpz & c) {
template<bool SYNCH>
void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
if (is_small(a) && is_small(b)) {
COMPILE_TIME_ASSERT(sizeof(a.m_val) == sizeof(int));
if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) {
int _a = a.m_val;
int _b = b.m_val;
if (_a < 0) _a = -_a;
if (_b < 0) _b = -_b;
unsigned r = u_gcd(_a, _b);
// Remark: r is (INT_MAX + 1)
// If a == b == INT_MIN
set(c, r);
}
else {