From dfdf7a0e4aa0b532317dd3a3b8b02cc4081c16d8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Jul 2018 18:31:05 -0700
Subject: [PATCH] update mpz for NO_GMP

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/mpz.cpp |  2 +-
 src/util/mpz.h   | 19 +++++++++----------
 2 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index da584eabf..7ad4797b7 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -356,7 +356,7 @@ void mpz_manager<SYNCH>::set_big_ui64(mpz & c, uint64_t v) {
 #ifdef _MP_GMP
 
 template<bool SYNCH>
-mpz_manager<SYNCH>::ensure_mpz_t(mpz const& a) {
+mpz_manager<SYNCH>::ensure_mpz_t::ensure_mpz_t(mpz const& a) {
     if (is_small(a)) {
         m_result = &m_local;
         mpz_init(m_local);
diff --git a/src/util/mpz.h b/src/util/mpz.h
index ab57de109..f480b097e 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -150,14 +150,6 @@ class mpz_manager {
     }
 
     mpz_cell * allocate(unsigned capacity);
-
-    void deallocate(mpz& n) {
-        if (n.m_ptr) {
-            deallocate(n.m_owner == mpz_self, n.m_ptr);
-            n.m_ptr = nullptr;
-            n.m_kind = mpz_small;
-        }
-    }
     
     // make sure that n is a big number and has capacity equal to at least c.
     void allocate_if_needed(mpz & n, unsigned c) {
@@ -181,7 +173,7 @@ class mpz_manager {
 
     void normalize(mpz & a);
 
-    void clear(mpz& n) { }
+    void clear(mpz& n) { reset(n); }
 
     /**
        \brief Set \c a with the value stored at src, and the given sign.
@@ -216,9 +208,16 @@ class mpz_manager {
         }
     }
 
-    void clear(mpz& n) { if (n.m_ptr) mpz_clear(*n.m_ptr); }
+    void clear(mpz& n) { if (n.m_ptr) { mpz_clear(*n.m_ptr); }}
 #endif
 
+    void deallocate(mpz& n) {
+        if (n.m_ptr) {
+            deallocate(n.m_owner == mpz_self, n.m_ptr);
+            n.m_ptr = nullptr;
+            n.m_kind = mpz_small;
+        }
+    }
 
     mpz                     m_two64;