diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp
index e00a25b1b..8ca2e983f 100644
--- a/src/util/mpff.cpp
+++ b/src/util/mpff.cpp
@@ -376,9 +376,11 @@ void mpff_manager::set(mpff & n, unsynch_mpz_manager & m, mpz const & v) {
     set_core(n, m, v); 
 }
 
+#ifndef _NO_OMP_
 void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) { 
     set_core(n, m, v); 
 }
+#endif
 
 template<bool SYNCH>
 void mpff_manager::set_core(mpff & n, mpq_manager<SYNCH> & m, mpq const & v) {
@@ -397,9 +399,11 @@ void mpff_manager::set(mpff & n, unsynch_mpq_manager & m, mpq const & v) {
     set_core(n, m, v); 
 }
 
+#ifndef _NO_OMP_
 void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) { 
     set_core(n, m, v); 
 }
+#endif
 
 bool mpff_manager::eq(mpff const & a, mpff const & b) const {
     if (is_zero(a) && is_zero(b))
@@ -1077,9 +1081,11 @@ void mpff_manager::significand(mpff const & n, unsynch_mpz_manager & m, mpz & t)
     significand_core(n, m, t);
 }
 
+#ifndef _NO_OMP_
 void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) {
     significand_core(n, m, t);
 }
+#endif
 
 template<bool SYNCH>
 void mpff_manager::to_mpz_core(mpff const & n, mpz_manager<SYNCH> & m, mpz & t) {
@@ -1109,9 +1115,11 @@ void mpff_manager::to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t) {
     to_mpz_core(n, m, t);
 }
 
+#ifndef _NO_OMP_
 void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) {
     to_mpz_core(n, m, t);
 }
+#endif
 
 template<bool SYNCH>
 void mpff_manager::to_mpq_core(mpff const & n, mpq_manager<SYNCH> & m, mpq & t) {
@@ -1154,9 +1162,11 @@ void mpff_manager::to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t) {
     to_mpq_core(n, m, t);
 }
 
+#ifndef _NO_OMP_
 void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) {
     to_mpq_core(n, m, t);
 }
+#endif
 
 void mpff_manager::display_raw(std::ostream & out, mpff const & n) const {
     if (is_neg(n))
diff --git a/src/util/mpff.h b/src/util/mpff.h
index 8023053d2..6f1e9d23c 100644
--- a/src/util/mpff.h
+++ b/src/util/mpff.h
@@ -58,9 +58,14 @@ class mpz;
 class mpq;
 template<bool SYNCH> class mpz_manager;
 template<bool SYNCH> class mpq_manager;
+#ifndef _NO_OMP_
 typedef mpz_manager<true>  synch_mpz_manager;
-typedef mpz_manager<false> unsynch_mpz_manager;
 typedef mpq_manager<true>  synch_mpq_manager;
+#else
+typedef mpz_manager<false>  synch_mpz_manager;
+typedef mpq_manager<false>  synch_mpq_manager;
+#endif
+typedef mpz_manager<false> unsynch_mpz_manager;
 typedef mpq_manager<false> unsynch_mpq_manager;
 
 class mpff_manager {
@@ -213,7 +218,9 @@ public:
        \brief Return the significand as a mpz numeral.
     */
     void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r);
+#ifndef _NO_OMP_
     void significand(mpff const & n, synch_mpz_manager & m, mpz & r);
+#endif
 
     /**
        \brief Return true if n is negative
@@ -378,9 +385,11 @@ public:
     void set(mpff & n, int64_t num, uint64_t den);
     void set(mpff & n, mpff const & v);
     void set(mpff & n, unsynch_mpz_manager & m, mpz const & v);
-    void set(mpff & n, synch_mpz_manager & m, mpz const & v); 
     void set(mpff & n, unsynch_mpq_manager & m, mpq const & v);
+#ifndef _NO_OMP_
     void set(mpff & n, synch_mpq_manager & m, mpq const & v);
+    void set(mpff & n, synch_mpz_manager & m, mpz const & v);
+#endif
     void set_plus_epsilon(mpff & n);
     void set_minus_epsilon(mpff & n);
     void set_max(mpff & n);
@@ -420,6 +429,7 @@ public:
     */
     void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t);
 
+#ifndef _NO_OMP_
     /**
        \brief Convert n into a mpz numeral.
        
@@ -428,6 +438,7 @@ public:
        \remark if exponent(n) is too big, we may run out of memory.
     */
     void to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t);
+#endif
 
     /**
        \brief Convert n into a mpq numeral.
@@ -436,13 +447,15 @@ public:
     */
     void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t);
 
+#ifndef _NO_OMP_
     /**
        \brief Convert n into a mpq numeral.
 
        \remark if exponent(n) is too big, we may run out of memory.
     */
     void to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t);
-    
+#endif
+
     /**
        \brief Return n as an int64.
 
diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp
index 2ebc54840..8ed16ec68 100644
--- a/src/util/mpfx.cpp
+++ b/src/util/mpfx.cpp
@@ -272,9 +272,11 @@ void mpfx_manager::set(mpfx & n, unsynch_mpz_manager & m, mpz const & v) {
     set_core(n, m, v);
 }
 
+#ifndef _NO_OMP_
 void mpfx_manager::set(mpfx & n, synch_mpz_manager & m, mpz const & v) {
     set_core(n, m, v);
 }
+#endif
 
 template<bool SYNCH>
 void mpfx_manager::set_core(mpfx & n, mpq_manager<SYNCH> & m, mpq const & v) {
@@ -309,9 +311,11 @@ void mpfx_manager::set(mpfx & n, unsynch_mpq_manager & m, mpq const & v) {
     set_core(n, m, v);
 }
 
+#ifndef _NO_OMP_
 void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & v) {
     set_core(n, m, v);
 }
+#endif
 
 bool mpfx_manager::eq(mpfx const & a, mpfx const & b) const {
     if (is_zero(a) && is_zero(b))
@@ -714,9 +718,11 @@ void mpfx_manager::to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t) {
     to_mpz_core(n, m, t);
 }
 
+#ifndef _NO_OMP_
 void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t) {
     to_mpz_core(n, m, t);
 }
+#endif
 
 template<bool SYNCH>
 void mpfx_manager::to_mpq_core(mpfx const & n, mpq_manager<SYNCH> & m, mpq & t) {
@@ -738,9 +744,11 @@ void mpfx_manager::to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t) {
     to_mpq_core(n, m, t);
 }
 
+#ifndef _NO_OMP_
 void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) {
     to_mpq_core(n, m, t);
 }
+#endif
 
 void mpfx_manager::display_raw(std::ostream & out, mpfx const & n) const {
     if (is_neg(n))
diff --git a/src/util/mpfx.h b/src/util/mpfx.h
index a8e93f0b0..6de3f251b 100644
--- a/src/util/mpfx.h
+++ b/src/util/mpfx.h
@@ -51,9 +51,14 @@ class mpz;
 class mpq;
 template<bool SYNCH> class mpz_manager;
 template<bool SYNCH> class mpq_manager;
+#ifndef _NO_OMP_
 typedef mpz_manager<true>  synch_mpz_manager;
-typedef mpz_manager<false> unsynch_mpz_manager;
 typedef mpq_manager<true>  synch_mpq_manager;
+#else
+typedef mpz_manager<false>  synch_mpz_manager;
+typedef mpq_manager<false>  synch_mpq_manager;
+#endif
+typedef mpz_manager<false> unsynch_mpz_manager;
 typedef mpq_manager<false> unsynch_mpq_manager;
 
 class mpfx_manager {
@@ -312,9 +317,11 @@ public:
     void set(mpfx & n, int64_t num, uint64_t den);
     void set(mpfx & n, mpfx const & v);
     void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v);
-    void set(mpfx & n, synch_mpz_manager & m, mpz const & v); 
     void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v);
+#ifndef _NO_OMP_
+    void set(mpfx & n, synch_mpz_manager & m, mpz const & v);
     void set(mpfx & n, synch_mpq_manager & m, mpq const & v);
+#endif
 
     /** 
         \brief Set n to the smallest representable numeral greater than zero.
@@ -359,22 +366,26 @@ public:
     */
     void to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t);
 
+#ifndef _NO_OMP_
     /**
        \brief Convert n into a mpz numeral.
        
        \pre is_int(n)
     */
     void to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t);
+#endif
 
     /**
        \brief Convert n into a mpq numeral.
     */
     void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t);
 
+#ifndef _NO_OMP_
     /**
        \brief Convert n into a mpq numeral.
     */
     void to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t);
+#endif
 
     /**
        \brief Return the biggest k s.t. 2^k <= a.
diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp
index 30ac0f410..207614ee0 100644
--- a/src/util/mpq.cpp
+++ b/src/util/mpq.cpp
@@ -26,12 +26,12 @@ mpq_manager<SYNCH>::mpq_manager() {
 
 template<bool SYNCH>
 mpq_manager<SYNCH>::~mpq_manager() {
-    del(m_n_tmp);
-    del(m_add_tmp1);
-    del(m_add_tmp2);
-    del(m_lt_tmp1);
-    del(m_lt_tmp2);
-    del(m_addmul_tmp);
+    del(m_tmp1);
+    del(m_tmp2);
+    del(m_tmp3);
+    del(m_tmp4);
+    del(m_q_tmp1);
+    del(m_q_tmp2);
 }
 
 
@@ -68,9 +68,9 @@ bool mpq_manager<SYNCH>::rat_lt(mpq const & a, mpq const & b) {
         return r;
     }
     else {
-        mul(na, db, m_lt_tmp1);
-        mul(nb, da, m_lt_tmp2);
-        return lt(m_lt_tmp1, m_lt_tmp2);
+        mul(na, db, m_q_tmp1);
+        mul(nb, da, m_q_tmp2);
+        return lt(m_q_tmp1, m_q_tmp2);
     }
 }
 
@@ -384,8 +384,7 @@ void mpq_manager<SYNCH>::rat_mul(mpq const & a, mpq const & b, mpq & c) {
         del(tmp2);
     }
     else {
-        mpz& g1 = m_n_tmp, &g2 = m_addmul_tmp.m_num, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2;
-        rat_mul(a, b, c, g1, g2, tmp1, tmp2);
+        rat_mul(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
     }
     STRACE("rat_mpq", tout << to_string(c) << "\n";);
 }
@@ -402,8 +401,7 @@ void mpq_manager<SYNCH>::rat_add(mpq const & a, mpq const & b, mpq & c) {
         del(g);
     }
     else {
-        mpz& g = m_n_tmp, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2, &tmp3 = m_addmul_tmp.m_num;
-        lin_arith_op<false>(a, b, c, g, tmp1, tmp2, tmp3);
+        lin_arith_op<false>(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
     }
     STRACE("rat_mpq", tout << to_string(c) << "\n";);
 }
@@ -420,13 +418,13 @@ void mpq_manager<SYNCH>::rat_sub(mpq const & a, mpq const & b, mpq & c) {
         del(g);
     }
     else {
-        mpz& g = m_n_tmp, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2, &tmp3 = m_addmul_tmp.m_num;
-        lin_arith_op<true>(a, b, c, g, tmp1, tmp2, tmp3);
+        lin_arith_op<true>(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
     }
     STRACE("rat_mpq", tout << to_string(c) << "\n";);
 }
 
 
+#ifndef _NO_OMP_
 template class mpq_manager<true>;
+#endif
 template class mpq_manager<false>;
-
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 77301371d..20802f786 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -41,12 +41,12 @@ inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
 
 template<bool SYNCH = true>
 class mpq_manager : public mpz_manager<SYNCH> {
-    mpz m_n_tmp;
-    mpz m_add_tmp1;
-    mpz m_add_tmp2;
-    mpq m_addmul_tmp;
-    mpq m_lt_tmp1;
-    mpq m_lt_tmp2;
+    mpz m_tmp1;
+    mpz m_tmp2;
+    mpz m_tmp3;
+    mpz m_tmp4;
+    mpq m_q_tmp1;
+    mpq m_q_tmp2;
 
     void reset_denominator(mpq & a) {
         del(a.m_den);
@@ -66,11 +66,11 @@ class mpq_manager : public mpz_manager<SYNCH> {
             del(tmp);
         }
         else {
-            gcd(a.m_num, a.m_den, m_n_tmp);
-            if (is_one(m_n_tmp))
+            gcd(a.m_num, a.m_den, m_tmp1);
+            if (is_one(m_tmp1))
                 return;
-            div(a.m_num, m_n_tmp, a.m_num);
-            div(a.m_den, m_n_tmp, a.m_den);
+            div(a.m_num, m_tmp1, a.m_num);
+            div(a.m_den, m_tmp1, a.m_den);
         }
     }
 
@@ -87,9 +87,9 @@ class mpq_manager : public mpz_manager<SYNCH> {
             del(tmp1);
         }
         else {
-            mul(b, a.m_den, m_add_tmp1);
+            mul(b, a.m_den, m_tmp1);
             set(c.m_den, a.m_den);
-            add(a.m_num, m_add_tmp1, c.m_num);
+            add(a.m_num, m_tmp1, c.m_num);
             normalize(c);
         }
         STRACE("rat_mpq", tout << to_string(c) << "\n";);
@@ -320,8 +320,8 @@ public:
                 del(tmp);
             }
             else {
-                mul(b,c,m_addmul_tmp);
-                add(a, m_addmul_tmp, d);
+                mul(b, c, m_q_tmp1);
+                add(a, m_q_tmp1, d);
             }
         }
     }
@@ -342,8 +342,8 @@ public:
                 del(tmp);
             }
             else {
-                mul(b,c,m_addmul_tmp);
-                add(a, m_addmul_tmp, d);
+                mul(b,c, m_q_tmp1);
+                add(a, m_q_tmp1, d);
             }
         }
     }
@@ -365,8 +365,8 @@ public:
                 del(tmp);
             }
             else {
-                mul(b,c,m_addmul_tmp);
-                sub(a, m_addmul_tmp, d);
+                mul(b,c, m_q_tmp1);
+                sub(a, m_q_tmp1, d);
             }
         }
     }
@@ -387,8 +387,8 @@ public:
                 del(tmp);
             }
             else {
-                mul(b,c,m_addmul_tmp);
-                sub(a, m_addmul_tmp, d);
+                mul(b,c, m_q_tmp1);
+                sub(a, m_q_tmp1, d);
             }
         }
     }
@@ -816,7 +816,11 @@ public:
     bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
 };
 
+#ifndef _NO_OMP_
 typedef mpq_manager<true> synch_mpq_manager;
+#else
+typedef mpq_manager<false> synch_mpq_manager;
+#endif
 typedef mpq_manager<false> unsynch_mpq_manager;
 
 typedef _scoped_numeral<unsynch_mpq_manager> scoped_mpq;
diff --git a/src/util/mpq_inf.cpp b/src/util/mpq_inf.cpp
index c6c160941..69de425cf 100644
--- a/src/util/mpq_inf.cpp
+++ b/src/util/mpq_inf.cpp
@@ -39,5 +39,7 @@ std::string mpq_inf_manager<SYNCH>::to_string(mpq_inf const & a) {
 }
 
 
+#ifndef _NO_OMP_
 template class mpq_inf_manager<true>;
+#endif
 template class mpq_inf_manager<false>;
diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h
index 7b866994d..c7bd261e6 100644
--- a/src/util/mpq_inf.h
+++ b/src/util/mpq_inf.h
@@ -279,7 +279,11 @@ public:
     mpq_manager<SYNCH>& get_mpq_manager() { return m; }
 };
 
+#ifndef _NO_OMP_
 typedef mpq_inf_manager<true>  synch_mpq_inf_manager;
+#else
+typedef mpq_inf_manager<false> synch_mpq_inf_manager;
+#endif
 typedef mpq_inf_manager<false> unsynch_mpq_inf_manager;
 
 #endif
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 7ad4797b7..32a074eb3 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -2369,5 +2369,7 @@ bool mpz_manager<SYNCH>::divides(mpz const & a, mpz const & b) {
     return r;
 }
 
+#ifndef _NO_OMP_
 template class mpz_manager<true>;
+#endif
 template class mpz_manager<false>;
diff --git a/src/util/mpz.h b/src/util/mpz.h
index f480b097e..187532a87 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -692,7 +692,11 @@ public:
     bool decompose(mpz const & n, svector<digit_t> & digits);
 };
 
+#ifndef _NO_OMP_
 typedef mpz_manager<true> synch_mpz_manager;
+#else
+typedef mpz_manager<false> synch_mpz_manager;
+#endif
 typedef mpz_manager<false> unsynch_mpz_manager;
 
 typedef _scoped_numeral<unsynch_mpz_manager> scoped_mpz;