From 810d63c246706cd8f3cf466eee8be84f016d2a92 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Jul 2018 06:54:50 -0700
Subject: [PATCH] put mpz_cell under ifdef _NO_GMP

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

diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 3ab033358..2d7ed96d3 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -196,6 +196,7 @@ mpz_manager<SYNCH>::~mpz_manager() {
         omp_destroy_nest_lock(&m_lock);
 }
 
+#ifndef _MP_GMP
 template<bool SYNCH>
 mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
     SASSERT(capacity >= m_init_cell_capacity);
@@ -215,6 +216,15 @@ void mpz_manager<SYNCH>::deallocate(bool is_heap, mpz_cell * ptr) {
     }
 }
 
+template<bool SYNCH>
+mpz_manager<SYNCH>::sign_cell::sign_cell(mpz_manager& m, mpz const& a): 
+    m_local(reinterpret_cast<mpz_cell*>(m_bytes)), m_a(a) {
+    m_local.m_ptr->m_capacity = capacity;
+    m.get_sign_cell(a, m_sign, m_cell, m_local.m_ptr);
+}
+
+
+#endif
 
 
 template<bool SYNCH>
@@ -1119,12 +1129,6 @@ unsigned mpz_manager<SYNCH>::size_info(mpz const & a) {
 #endif
 }
 
-template<bool SYNCH>
-mpz_manager<SYNCH>::sign_cell::sign_cell(mpz_manager& m, mpz const& a): 
-    m_local(reinterpret_cast<mpz_cell*>(m_bytes)), m_a(a) {
-    m_local.m_ptr->m_capacity = capacity;
-    m.get_sign_cell(a, m_sign, m_cell, m_local.m_ptr);
-}
 
 
 template<bool SYNCH>
diff --git a/src/util/mpz.h b/src/util/mpz.h
index bba373369..163594047 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -183,6 +183,13 @@ class mpz_manager {
 
     void clear(mpz& n) { }
 
+    /**
+       \brief Set \c a with the value stored at src, and the given sign.
+       \c sz is an overapproximation of the size of the number stored at \c src.
+    */
+    void set(mpz_cell& src, mpz & a, int sign, unsigned sz); 
+
+
 #else
     // GMP code
     mpz_t     m_tmp, m_tmp2;
@@ -215,11 +222,6 @@ class mpz_manager {
 
     mpz                     m_two64;
 
-    /**
-       \brief Set \c a with the value stored at src, and the given sign.
-       \c sz is an overapproximation of the size of the number stored at \c src.
-    */
-    void set(mpz_cell& src, mpz & a, int sign, unsigned sz); 
 
     static int64_t i64(mpz const & a) { return static_cast<int64_t>(a.m_val); }