From f359f238851d8c1a5db11a95d4ded3639813db9a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 8 Oct 2017 15:47:06 -0700
Subject: [PATCH] another fix for #1288

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/mpz.cpp | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 9569ac280..7cf87b24b 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -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 {