diff --git a/src/test/rational.cpp b/src/test/rational.cpp
index 9cbcdb00e..834aab92f 100644
--- a/src/test/rational.cpp
+++ b/src/test/rational.cpp
@@ -171,7 +171,7 @@ static void tst2() {
 
 
     rational int64_max("9223372036854775807");
-    rational int64_min(-int64_max - rational(1));
+    rational int64_min((-int64_max) - rational(1));
     // is_int64
     SASSERT(int64_max.is_int64());
     SASSERT(int64_min.is_int64());
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 9473621cf..a7c904c64 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -128,6 +128,8 @@ mpz_manager<SYNCH>::mpz_manager():
     mpz_mul(m_int64_max, m_tmp, m_int64_max);
     mpz_set_ui(m_tmp, max_l);
     mpz_add(m_int64_max, m_tmp, m_int64_max);
+    mpz_neg(m_int64_min, m_int64_max);
+    mpz_sub_ui(m_int64_min, m_int64_min, 1);
 #endif
     
     mpz one(1);
@@ -152,6 +154,7 @@ mpz_manager<SYNCH>::~mpz_manager() {
     deallocate(m_arg[1]);
     mpz_clear(m_uint64_max);
     mpz_clear(m_int64_max);
+    mpz_clear(m_int64_min);
 #endif
     if (SYNCH)
         omp_destroy_nest_lock(&m_lock);
@@ -1317,7 +1320,7 @@ bool mpz_manager<SYNCH>::is_int64(mpz const & a) const {
     }
 #else
     // GMP version
-    return mpz_cmp(*a.m_ptr, m_int64_max) <= 0;
+    return mpz_cmp(m_int64_min, *a.m_ptr) <= 0 && mpz_cmp(*a.m_ptr, m_int64_max) <= 0;
 #endif
 }
 
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 7b40a89f5..923d5b3a7 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -168,6 +168,7 @@ class mpz_manager {
     mpz_t  *  m_arg[2];
     mpz_t     m_uint64_max;
     mpz_t     m_int64_max;
+    mpz_t     m_int64_min;
 
     mpz_t * allocate() {
         mpz_t * cell = reinterpret_cast<mpz_t*>(m_allocator.allocate(sizeof(mpz_t)));