diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index e2fb7fe5a..102a96ac5 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -146,7 +146,7 @@ namespace Microsoft.Z3
         /// The query is satisfiable if there is an instance of some relation that is non-empty.
         /// The query is unsatisfiable if there are no derivations satisfying any of the relations.
         /// </summary>        
-        public Status Query(FuncDecl[] relations)
+        public Status Query(params FuncDecl[] relations)
         {
             Contract.Requires(relations != null);
             Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null));
@@ -262,7 +262,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Convert benchmark given as set of axioms, rules and queries to a string.
         /// </summary>                
-        public string ToString(BoolExpr[] queries)
+        public string ToString(params BoolExpr[] queries)
         {
 
             return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 364be8a77..89df04961 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -122,6 +122,7 @@ public:
     explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {}
     explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s.c_ptr()) {}
     explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {}
+    explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {}
     explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
     explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s).c_ptr()) {}
     explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 00ba93ccb..07c6fd06a 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -363,12 +363,12 @@ bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) {
 
 bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
     if (s == sP) return true;
-    unsigned i;
-    if (is_sort_param(sP, i)) {
-        if (binding.size() <= i) binding.resize(i+1);
-        if (binding[i] && (binding[i] != s)) return false;
-        TRACE("seq_verbose", tout << "setting binding @ " << i << " to " << mk_pp(s, *m_manager) << "\n";);
-        binding[i] = s;
+    unsigned idx;
+    if (is_sort_param(sP, idx)) {
+        if (binding.size() <= idx) binding.resize(idx+1);
+        if (binding[idx] && (binding[idx] != s)) return false;
+        TRACE("seq_verbose", tout << "setting binding @ " << idx << " to " << mk_pp(s, *m_manager) << "\n";);
+        binding[idx] = s;
         return true;
     }
 
@@ -376,7 +376,8 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
     if (s->get_family_id() == sP->get_family_id() &&
         s->get_decl_kind() == sP->get_decl_kind() &&
         s->get_num_parameters() == sP->get_num_parameters()) {
-        for (parameter const& p : s->parameters()) {
+		for (unsigned i = 0, sz = s->get_num_parameters(); i < sz; ++i) {
+			parameter const& p = s->get_parameter(i);
             if (p.is_ast() && is_sort(p.get_ast())) {
                 parameter const& p2 = sP->get_parameter(i);
                 if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false;
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 5417785d6..190f7f79e 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -28,6 +28,15 @@ Revision History:
 
 namespace smt {
 
+    void fresh_value_proc::get_dependencies(buffer<model_value_dependency>& result) { 
+        result.push_back(model_value_dependency(m_value)); 
+    }
+
+    std::ostream& operator<<(std::ostream& out, model_value_dependency const& src) {
+        if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx();
+        else return out << "#" << src.get_enode()->get_owner_id();
+    }
+
     model_generator::model_generator(ast_manager & m):
         m_manager(m),
         m_context(nullptr),
@@ -161,20 +170,20 @@ namespace smt {
                                          source2color & colors, 
                                          obj_hashtable<sort> & already_traversed, 
                                          svector<source> & todo) {
+
         if (src.is_fresh_value()) {
-            // there is an implicit dependency between a fresh value stub of sort S and the root enodes of sort S that are not associated with fresh values.
+            // there is an implicit dependency between a fresh value stub of 
+            // sort S and the root enodes of sort S that are not associated with fresh values.
+            //
             sort * s     = src.get_value()->get_sort();
             if (already_traversed.contains(s))
                 return true;
             bool visited = true;
-            unsigned sz  = roots.size();
-            for (unsigned i = 0; i < sz; i++) {
-                enode * r     = roots[i];
+            for (enode * r : roots) {
                 if (m_manager.get_sort(r->get_owner()) != s)
                     continue;
                 SASSERT(r == r->get_root());
-                model_value_proc * proc = nullptr;
-                root2proc.find(r, proc);
+                model_value_proc * proc = root2proc[r];
                 SASSERT(proc);
                 if (proc->is_fresh())
                     continue; // r is associated with a fresh value...
@@ -192,17 +201,12 @@ namespace smt {
         enode * n = src.get_enode();
         SASSERT(n == n->get_root());
         bool visited = true;
-        model_value_proc * proc = nullptr;
-        root2proc.find(n, proc);
-        SASSERT(proc);
+        model_value_proc * proc = root2proc[n];
         buffer<model_value_dependency> dependencies;
         proc->get_dependencies(dependencies);
         for (model_value_dependency const& dep : dependencies) {
             visit_child(dep, colors, todo, visited);
-            TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> ";
-                  if (dep.is_fresh_value()) tout << "fresh!" << dep.get_value()->get_idx();
-                  else tout << "#" << dep.get_enode()->get_owner_id();
-                  tout << "\n";);
+            TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> " << dep << " already visited: " << visited << "\n";);
         }
         return visited;
     }
@@ -215,9 +219,7 @@ namespace smt {
                                          svector<source> & todo,
                                          svector<source> & sorted_sources) {
         TRACE("mg_top_sort", tout << "process source, is_fresh: " << src.is_fresh_value() << " ";
-              if (src.is_fresh_value()) tout << "fresh!" << src.get_value()->get_idx();
-              else tout << "#" << src.get_enode()->get_owner_id();
-              tout << ", todo.size(): " << todo.size() << "\n";);
+              tout << src << ", todo.size(): " << todo.size() << "\n";);
         int color     = get_color(colors, src);
         SASSERT(color != Grey);
         if (color == Black)
@@ -227,17 +229,16 @@ namespace smt {
         while (!todo.empty()) {
             source curr = todo.back();
             TRACE("mg_top_sort", tout << "current source, is_fresh: " << curr.is_fresh_value() << " ";
-                  if (curr.is_fresh_value()) tout << "fresh!" << curr.get_value()->get_idx();
-                  else tout << "#" << curr.get_enode()->get_owner_id();
-                  tout << ", todo.size(): " << todo.size() << "\n";);
+                  tout << curr << ", todo.size(): " << todo.size() << "\n";);
             switch (get_color(colors, curr)) {
             case White:
                 set_color(colors, curr, Grey);
                 visit_children(curr, roots, root2proc, colors, already_traversed, todo);
                 break;
             case Grey:
-                SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo));
+                // SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo));
                 set_color(colors, curr, Black);
+                TRACE("mg_top_sort", tout << "append " << curr << "\n";);
                 sorted_sources.push_back(curr);
                 break;
             case Black:
@@ -266,18 +267,15 @@ namespace smt {
         // topological sort
 
         // traverse all extra fresh values...
-        unsigned sz = m_extra_fresh_values.size();
-        for (unsigned i = 0; i < sz; i++) {
-            extra_fresh_value * f = m_extra_fresh_values[i];
+        for (extra_fresh_value * f : m_extra_fresh_values) {
             process_source(source(f), roots, root2proc, colors, already_traversed, todo, sorted_sources);
         }
 
         // traverse all enodes that are associated with fresh values...
-        sz = roots.size();
+        unsigned sz = roots.size();
         for (unsigned i = 0; i < sz; i++) {
             enode * r     = roots[i];
-            model_value_proc * proc = nullptr;
-            root2proc.find(r, proc);
+            model_value_proc * proc = root2proc[r];
             SASSERT(proc);
             if (!proc->is_fresh())
                 continue;
@@ -303,43 +301,38 @@ namespace smt {
         TRACE("sorted_sources",
               for (source const& curr : sources) {
                   if (curr.is_fresh_value()) {
-                      tout << "fresh!" << curr.get_value()->get_idx() << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n";
+                      tout << curr << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n";
                   }
                   else {
                       enode * n = curr.get_enode();
                       SASSERT(n->get_root() == n);
                       sort * s = m_manager.get_sort(n->get_owner());
-                      tout << "#" << n->get_owner_id() << " " << mk_pp(s, m_manager);
-                      model_value_proc * proc = 0;
-                      root2proc.find(n, proc);
-                      SASSERT(proc);
-                      tout << " is_fresh: " << proc->is_fresh() << "\n";
+                      tout << curr << " " << mk_pp(s, m_manager);
+                      tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
                   }
               });
         for (source const& curr : sources) {
             if (curr.is_fresh_value()) {
                 sort * s = curr.get_value()->get_sort();
-                TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " : " << mk_pp(s, m_manager) << "\n";);
+                TRACE("model_fresh_bug", tout << curr << " : " << mk_pp(s, m_manager) << "\n";);
                 expr * val = m_model->get_fresh_value(s);
-                TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " := #" << (val == 0 ? UINT_MAX : val->get_id()) << "\n";);
+                TRACE("model_fresh_bug", tout << curr << " := #" << (val == nullptr ? UINT_MAX : val->get_id()) << "\n";);
                 m_asts.push_back(val);
                 curr.get_value()->set_value(val);
             }
             else {
                 enode * n = curr.get_enode();
                 SASSERT(n->get_root() == n);
-                TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << "\n";);
+                TRACE("mg_top_sort", tout << curr << "\n";);
                 dependencies.reset();
                 dependency_values.reset();
-                model_value_proc * proc = nullptr;
-                VERIFY(root2proc.find(n, proc));
+                model_value_proc * proc = root2proc[n];
                 SASSERT(proc);
                 proc->get_dependencies(dependencies);
                 for (model_value_dependency const& d : dependencies) {
                     if (d.is_fresh_value()) {
                         CTRACE("mg_top_sort", !d.get_value()->get_value(), 
-                               tout << "#" << n->get_owner_id() << " -> ";
-                               tout << "fresh!" << d.get_value()->get_idx() << "\n";);
+                               tout << "#" << n->get_owner_id() << " -> " << d << "\n";);
                         SASSERT(d.get_value()->get_value());
                         dependency_values.push_back(d.get_value()->get_value());
                     }
diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h
index 7466b8877..1f69eb324 100644
--- a/src/smt/smt_model_generator.h
+++ b/src/smt/smt_model_generator.h
@@ -100,14 +100,16 @@ namespace smt {
             extra_fresh_value * m_value; //!< When m_fresh == true, contains the sort of the fresh value
         };
     public:
-        model_value_dependency():m_fresh(true), m_value(nullptr) {}
-        model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {}
-        model_value_dependency(extra_fresh_value * v):m_fresh(true), m_value(v) {}
+        model_value_dependency():m_fresh(true), m_value(nullptr) { }
+        explicit model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {}
+        explicit model_value_dependency(extra_fresh_value * v) :m_fresh(true), m_value(v) { SASSERT(v); }
         bool is_fresh_value() const { return m_fresh; }
         enode * get_enode() const { SASSERT(!is_fresh_value()); return m_enode; }
         extra_fresh_value * get_value() const { SASSERT(is_fresh_value()); return m_value; }
     };
 
+    std::ostream& operator<<(std::ostream& out, model_value_dependency const& d);
+
     typedef model_value_dependency source;
 
     struct source_hash_proc {
@@ -166,7 +168,7 @@ namespace smt {
         extra_fresh_value * m_value;
     public:
         fresh_value_proc(extra_fresh_value * v):m_value(v) {}
-        void get_dependencies(buffer<model_value_dependency> & result) override { result.push_back(m_value); }
+        void get_dependencies(buffer<model_value_dependency> & result) override;
         app * mk_value(model_generator & m, ptr_vector<expr> & values) override { return to_app(values[0]); }
         bool is_fresh() const override { return true; }
     };
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3b6af0be5..a057ace03 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1120,7 +1120,7 @@ public:
             (v != null_theory_var) &&
             (v < static_cast<theory_var>(m_theory_var2var_index.size())) && 
             (UINT_MAX != m_theory_var2var_index[v]) &&
-            !m_variable_values.empty();
+            (!m_variable_values.empty() || m_solver->is_term(m_theory_var2var_index[v]));
     }
 
     bool can_get_bound(theory_var v) const {
@@ -1165,13 +1165,21 @@ public:
     }
         
     rational get_value(theory_var v) const {
-        if (!can_get_value(v)) return rational::zero();
+        
+        if (v == null_theory_var || 
+            v >= static_cast<theory_var>(m_theory_var2var_index.size())) {
+            TRACE("arith", tout << "Variable v" << v << " not internalized\n";);
+            return rational::zero();
+        }
+            
         lp::var_index vi = m_theory_var2var_index[v];
         if (m_variable_values.count(vi) > 0)
             return m_variable_values[vi];
         
-        if(!m_solver->is_term(vi))
+        if (!m_solver->is_term(vi)) {
+            TRACE("arith", tout << "not a term v" << v << "\n";);
             return rational::zero();
+        }
         
         m_todo_terms.push_back(std::make_pair(vi, rational::one()));
         rational result(0);
@@ -1203,6 +1211,7 @@ public:
         if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
             reset_variable_values();
             m_solver->get_model(m_variable_values);
+            TRACE("arith", display(tout););
         }
     }
 
@@ -2638,6 +2647,7 @@ public:
         }
         else {
             rational r = get_value(v);
+            TRACE("arith", tout << "v" << v << " := " << r << "\n";);
             if (a.is_int(o) && !r.is_int()) r = floor(r);
             return alloc(expr_wrapper_proc, m_factory->mk_value(r,  m.get_sort(o)));
         }
diff --git a/src/util/cooperate.cpp b/src/util/cooperate.cpp
index 2b2e7958e..df8f67968 100644
--- a/src/util/cooperate.cpp
+++ b/src/util/cooperate.cpp
@@ -16,6 +16,8 @@ Author:
 Notes:
 
 --*/
+
+#ifndef _NO_OMP_
 #include "util/cooperate.h"
 #include "util/trace.h"
 #include "util/debug.h"
@@ -36,7 +38,7 @@ struct cooperation_lock {
     }
 };
 
-cooperation_lock g_lock;
+static cooperation_lock g_lock;
 
 bool cooperation_ctx::g_cooperate = false;
 
@@ -59,29 +61,4 @@ void cooperation_ctx::checkpoint(char const * task) {
     }
 }
 
-cooperation_section::cooperation_section() {
-    SASSERT(!cooperation_ctx::enabled());
-    SASSERT(!omp_in_parallel());
-    cooperation_ctx::g_cooperate = true;
-}
-
-cooperation_section::~cooperation_section() {
-    SASSERT(cooperation_ctx::enabled());
-    cooperation_ctx::g_cooperate = false;
-}
-
-init_task::init_task(char const * task) {
-    SASSERT(cooperation_ctx::enabled());
-    SASSERT(omp_in_parallel());
-    cooperation_ctx::checkpoint(task);
-}
-
-init_task::~init_task() {
-    int  tid      = omp_get_thread_num();
-    if (g_lock.m_owner_thread == tid) {
-        g_lock.m_owner_thread = -1;
-        omp_unset_nest_lock(&(g_lock.m_lock));
-    }
-}
-
-
+#endif
diff --git a/src/util/cooperate.h b/src/util/cooperate.h
index af2cff55c..6220c4c51 100644
--- a/src/util/cooperate.h
+++ b/src/util/cooperate.h
@@ -19,10 +19,9 @@ Notes:
 #ifndef COOPERATE_H_
 #define COOPERATE_H_
 
-class cooperation_section;
+#ifndef _NO_OMP_
 
 class cooperation_ctx {
-    friend class cooperation_section;
     static bool g_cooperate;
 public:
     static bool enabled() { return g_cooperate; }
@@ -33,18 +32,8 @@ inline void cooperate(char const * task) {
     if (cooperation_ctx::enabled()) cooperation_ctx::checkpoint(task);
 }
 
-// must be declared before "#pragma parallel" to enable cooperation 
-class cooperation_section {
-public:
-    cooperation_section();
-    ~cooperation_section();
-};
-
-// must be first declaration inside "#pragma parallel for"
-class init_task {
-public:
-    init_task(char const * task);
-    ~init_task();
-};
+#else
+inline void cooperate(char const *) {}
+#endif
 
 #endif
diff --git a/src/util/lp/hnf_cutter.h b/src/util/lp/hnf_cutter.h
index 061b3a130..3f9038651 100644
--- a/src/util/lp/hnf_cutter.h
+++ b/src/util/lp/hnf_cutter.h
@@ -186,43 +186,41 @@ public:
 
     bool overflow() const { return m_overflow; }
     
-    lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper
-                        #ifdef Z3DEBUG
-                        ,
-                        const vector<mpq> & x0
-                        #endif
-                        ) {
+    lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper, const vector<mpq> & x0) {
         // we suppose that x0 has at least one non integer element 
+        (void)x0;
+
         init_matrix_A();
         svector<unsigned> basis_rows;
         mpq big_number = m_abs_max.expt(3);
         mpq d = hnf_calc::determinant_of_rectangular_matrix(m_A, basis_rows, big_number);
         
-        //        std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
-        //std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
+        // std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
+        // std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
 
         if (d >= big_number) {
             return lia_move::undef;
         }
         
-        if (m_settings.get_cancel_flag())
+        if (m_settings.get_cancel_flag()) {
             return lia_move::undef;
+        }
+
         if (basis_rows.size() < m_A.row_count()) {
             m_A.shrink_to_rank(basis_rows);
             shrink_explanation(basis_rows);
         }
         
-        hnf<general_matrix> h(m_A, d);
-        //  general_matrix A_orig = m_A;
-        
+        hnf<general_matrix> h(m_A, d);        
         vector<mpq> b = create_b(basis_rows);
         lp_assert(m_A * x0 == b);
-        // vector<mpq> bcopy = b;
         find_h_minus_1_b(h.W(), b);
-        // lp_assert(bcopy == h.W().take_first_n_columns(b.size()) * b);
         int cut_row = find_cut_row_index(b);
-        if (cut_row == -1)
+
+        if (cut_row == -1) {
             return lia_move::undef;
+        }
+
         // the matrix is not square - we can get
         // all integers in b's projection
         
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 1d0d20c33..2e744e3d6 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -578,17 +578,27 @@ lia_move int_solver::make_hnf_cut() {
         return lia_move::undef;
     }
     settings().st().m_hnf_cutter_calls++;
-    TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls;);
+    TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls << "\n";
+          for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
+              m_lar_solver->print_constraint(i, tout);
+          }              
+          m_lar_solver->print_constraints(tout);
+          );
 #ifdef Z3DEBUG
     vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(m_lar_solver->m_mpq_lar_core_solver.m_r_x);
+#else
+    vector<mpq> x0;
 #endif
-    lia_move r =  m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper
-#ifdef Z3DEBUG
-                                          , x0
-#endif
-                                          );
-    CTRACE("hnf_cut", r == lia_move::cut, tout<< "cut:"; m_lar_solver->print_term(*m_t, tout); tout << " <= " << *m_k << std::endl;);
-    if (r == lia_move::cut) {        
+    lia_move r =  m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper, x0);
+
+    if (r == lia_move::cut) {      
+        TRACE("hnf_cut",
+              m_lar_solver->print_term(*m_t, tout << "cut:"); 
+              tout << " <= " << *m_k << std::endl;
+              for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
+                  m_lar_solver->print_constraint(i, tout);
+              }              
+              );
         lp_assert(current_solution_is_inf_on_cut());
         settings().st().m_hnf_cuts++;
         m_ex->clear();        
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 72705dfb3..3735fbb9f 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -112,7 +112,7 @@ private:
     
 public :
     unsigned terms_start_index() const { return m_terms_start_index; }
-    const vector<lar_term*> terms() const { return m_terms; }
+    const vector<lar_term*> & terms() const { return m_terms; }
     const vector<lar_base_constraint*>& constraints() const {
         return m_constraints;
     }
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 b7bdbf400..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);
             }
         }
     }
@@ -814,12 +814,13 @@ public:
     bool is_even(mpz const & a) { return mpz_manager<SYNCH>::is_even(a); }
 public:
     bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
-
-    friend bool operator==(mpq const & a, mpq const & b) ;
-    friend bool operator>=(mpq const & a, mpq const & b);
 };
 
+#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;