diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp
index a9f9ca757..fc2177ca2 100644
--- a/src/test/mpz.cpp
+++ b/src/test/mpz.cpp
@@ -293,6 +293,19 @@ void tst_int_min_bug() {
     m.del(r);
 }
 
+void tst_int64_min_bug() {
+    synch_mpz_manager m;
+    mpz intmin;
+    mpz test;
+    m.set(test, "-9223372036854775808");
+    m.set(intmin, std::numeric_limits<int64_t>::min());
+    std::cout << "minint: " << m.to_string(intmin) << "\n";
+    ENSURE(m.eq(test, intmin));
+    m.del(intmin);
+    m.del(test);
+}
+
+
 void tst_scoped() {
     synch_mpz_manager m;
     scoped_synch_mpz a(m);
@@ -504,6 +517,7 @@ void tst_mpz() {
     // tst_gcd();
     tst_scoped();
     tst_int_min_bug();
+    tst_int64_min_bug();
     bug4();
     bug3();
     bug1();
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index cda4b599a..8188c8be2 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -272,7 +272,12 @@ void mpz_manager<SYNCH>::set_big_i64(mpz & c, int64_t v) {
     c.m_kind = mpz_large;
     SASSERT(capacity(c) >= m_init_cell_capacity);
     uint64_t _v;
-    if (v < 0) {
+    if (v == std::numeric_limits<int64_t>::min()) {
+        // min-int is even
+        _v = -(v/2);
+        c.m_val = -1;
+    }
+    else if (v < 0) {
         _v = -v;
         c.m_val = -1;
     }
@@ -298,14 +303,15 @@ void mpz_manager<SYNCH>::set_big_i64(mpz & c, int64_t v) {
     }
     c.m_kind = mpz_large;
     uint64_t _v;
-    bool sign;
-    if (v < 0) {
+    bool sign = v < 0;
+    if (v == std::numeric_limits<int64_t>::min()) {
+        _v = -(v/2);
+    }
+    else if (v < 0) {
         _v   = -v;
-        sign = true;
     }
     else {
         _v   = v;
-        sign = false;
     }
     mpz_set_ui(*c.m_ptr, static_cast<unsigned>(_v));
     MPZ_BEGIN_CRITICAL();
@@ -316,6 +322,9 @@ void mpz_manager<SYNCH>::set_big_i64(mpz & c, int64_t v) {
     if (sign)
         mpz_neg(*c.m_ptr, *c.m_ptr);
 #endif
+    if (v == std::numeric_limits<int64_t>::min()) {
+        big_add(c, c, c);
+    }
 }
 
 template<bool SYNCH>