diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp
index 90e8f4dafe5..d24a4a62449 100644
--- a/src/api/api_algebraic.cpp
+++ b/src/api/api_algebraic.cpp
@@ -134,7 +134,7 @@ extern "C" {
                 _am.set(_av, av.to_mpq());                              \
                 scoped_anum _r(_am);                                    \
                 _am.IRAT_OP(_av, bv, _r);                               \
-                r = au(c).mk_numeral(_r, false);                        \
+                r = au(c).mk_numeral(_am, _r, false);                   \
             }                                                           \
         }                                                               \
         else {                                                          \
@@ -145,13 +145,13 @@ extern "C" {
                 _am.set(_bv, bv.to_mpq());                              \
                 scoped_anum _r(_am);                                    \
                 _am.IRAT_OP(av, _bv, _r);                               \
-                r = au(c).mk_numeral(_r, false);                        \
+                r = au(c).mk_numeral(_am, _r, false);                   \
             }                                                           \
             else {                                                      \
                 algebraic_numbers::anum const & bv = get_irrational(c, b); \
                 scoped_anum _r(_am);                                    \
                 _am.IRAT_OP(av, bv, _r);                                \
-                r = au(c).mk_numeral(_r, false);                        \
+                r = au(c).mk_numeral(_am, _r, false);                   \
             }                                                           \
         }                                                               \
         mk_c(c)->save_ast_trail(r);                                     \
@@ -226,7 +226,7 @@ extern "C" {
             algebraic_numbers::anum const & av = get_irrational(c, a);
             _am.root(av, k, _r);
         }
-        expr * r = au(c).mk_numeral(_r, false);
+        expr * r = au(c).mk_numeral(_am, _r, false);
         mk_c(c)->save_ast_trail(r);
         RETURN_Z3(of_ast(r));
         Z3_CATCH_RETURN(nullptr);
@@ -248,7 +248,7 @@ extern "C" {
             algebraic_numbers::anum const & av = get_irrational(c, a);
             _am.power(av, k, _r);
         }
-        expr * r = au(c).mk_numeral(_r, false);
+        expr * r = au(c).mk_numeral(_am, _r, false);
         mk_c(c)->save_ast_trail(r);
         RETURN_Z3(of_ast(r));
         Z3_CATCH_RETURN(nullptr);
@@ -380,7 +380,7 @@ extern "C" {
         Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(result);
         for (unsigned i = 0; i < roots.size(); i++) {
-            result->m_ast_vector.push_back(au(c).mk_numeral(roots.get(i), false));
+            result->m_ast_vector.push_back(au(c).mk_numeral(_am, roots.get(i), false));
         }
         RETURN_Z3(of_ast_vector(result));
         Z3_CATCH_RETURN(nullptr);
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 3bcaf10b513..0ac922ecfda 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -39,11 +39,11 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
 
     unsigned mk_id(algebraic_numbers::anum const & val) {
         SASSERT(!m_amanager.is_rational(val));
-        unsigned new_id = m_id_gen.mk();
-        m_nums.reserve(new_id+1);
-        m_amanager.set(m_nums[new_id], val);
-        TRACE("algebraic2expr", tout << "mk_id -> " << new_id << "\n"; m_amanager.display(tout, val); tout << "\n";);
-        return new_id;
+        unsigned idx = m_id_gen.mk();
+        m_nums.reserve(idx+1);
+        m_amanager.set(m_nums[idx], val);
+        TRACE("algebraic2expr", tout << "mk_id -> " << idx << "\n"; m_amanager.display(tout, val); tout << "\n";);
+        return idx;
     }
 
     void recycle_id(unsigned idx) {
@@ -66,8 +66,8 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
 };
 
 arith_decl_plugin::algebraic_numbers_wrapper & arith_decl_plugin::aw() const {
-    if (m_aw == nullptr)
-        const_cast<arith_decl_plugin*>(this)->m_aw = alloc(algebraic_numbers_wrapper, m_manager->limit());
+    if (m_aw == nullptr) 
+        const_cast<arith_decl_plugin*>(this)->m_aw = alloc(algebraic_numbers_wrapper, m_manager->limit());    
     return *m_aw;
 }
 
@@ -75,10 +75,10 @@ algebraic_numbers::manager & arith_decl_plugin::am() const {
     return aw().m_amanager;
 }
 
-app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is_int) {
-    if (am().is_rational(val)) {
+app * arith_decl_plugin::mk_numeral(algebraic_numbers::manager& m, algebraic_numbers::anum const & val, bool is_int) {
+    if (m.is_rational(val)) {
         rational rval;
-        am().to_rational(val, rval);
+        m.to_rational(val, rval);
         return mk_numeral(rval, is_int);
     }
     else {
@@ -103,7 +103,7 @@ app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is
 app * arith_decl_plugin::mk_numeral(sexpr const * p, unsigned i) {
     scoped_anum r(am());
     am().mk_root(p, i, r);
-    return mk_numeral(r, false);
+    return mk_numeral(am(), r, false);
 }
 
 void arith_decl_plugin::del(parameter const & p) {
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index d62d385c717..ada150e2748 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -195,7 +195,7 @@ class arith_decl_plugin : public decl_plugin {
 
     app * mk_numeral(rational const & n, bool is_int);
 
-    app * mk_numeral(algebraic_numbers::anum const & val, bool is_int);
+    app * mk_numeral(algebraic_numbers::manager& m, algebraic_numbers::anum const & val, bool is_int);
 
     // Create a (real) numeral that is the i-th root of the polynomial encoded using the given sexpr.
     app * mk_numeral(sexpr const * p, unsigned i);
@@ -401,8 +401,8 @@ class arith_util : public arith_recognizers {
         SASSERT(is_int(s) || is_real(s));
         return mk_numeral(val, is_int(s));
     }
-    app * mk_numeral(algebraic_numbers::anum const & val, bool is_int) {
-        return plugin().mk_numeral(val, is_int);
+    app * mk_numeral(algebraic_numbers::manager& m, algebraic_numbers::anum const & val, bool is_int) {
+        return plugin().mk_numeral(m, val, is_int);
     }
     app * mk_numeral(sexpr const * p, unsigned i) {
         return plugin().mk_numeral(p, i);
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 4ec0b388342..9c2dad734aa 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -755,7 +755,7 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex
         for (unsigned i = 0; i < num_args; i ++) {
             unsigned d = am.degree(r);
             if (d > 1 && d > m_max_degree) {
-                new_args.push_back(m_util.mk_numeral(r, false));
+                new_args.push_back(m_util.mk_numeral(am, r, false));
                 am.set(r, 0);
             }
 
@@ -777,11 +777,11 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex
         }
 
         if (new_args.empty()) {
-            result = m_util.mk_numeral(r, false);
+            result = m_util.mk_numeral(am, r, false);
             return BR_DONE;
         }
 
-        new_args.push_back(m_util.mk_numeral(r, false));
+        new_args.push_back(m_util.mk_numeral(am, r, false));
         br_status st = poly_rewriter<arith_rewriter_core>::mk_add_core(new_args.size(), new_args.c_ptr(), result);
         if (st == BR_FAILED) {
             result = m().mk_app(get_fid(), OP_ADD, new_args.size(), new_args.c_ptr());
@@ -805,7 +805,7 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex
         for (unsigned i = 0; i < num_args; i ++) {
             unsigned d = am.degree(r);
             if (d > 1 && d > m_max_degree) {
-                new_args.push_back(m_util.mk_numeral(r, false));
+                new_args.push_back(m_util.mk_numeral(am, r, false));
                 am.set(r, 1);
             }
 
@@ -826,10 +826,10 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex
         }
 
         if (new_args.empty()) {
-            result = m_util.mk_numeral(r, false);
+            result = m_util.mk_numeral(am, r, false);
             return BR_DONE;
         }
-        new_args.push_back(m_util.mk_numeral(r, false));
+        new_args.push_back(m_util.mk_numeral(am, r, false));
 
         br_status st = poly_rewriter<arith_rewriter_core>::mk_mul_core(new_args.size(), new_args.c_ptr(), result);
         if (st == BR_FAILED) {
@@ -857,7 +857,7 @@ br_status arith_rewriter::mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref &
     am.set(val2, rval2.to_mpq());
     scoped_anum r(am);
     am.div(val1, val2, r);
-    result = m_util.mk_numeral(r, false);
+    result = m_util.mk_numeral(am, r, false);
     return BR_DONE;
 }
 
@@ -873,7 +873,7 @@ br_status arith_rewriter::mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref &
     anum const & val2  = m_util.to_irrational_algebraic_numeral(arg2);
     scoped_anum r(am);
     am.div(val1, val2, r);
-    result = m_util.mk_numeral(r, false);
+    result = m_util.mk_numeral(am, r, false);
     return BR_DONE;
 }
 
@@ -890,7 +890,7 @@ br_status arith_rewriter::mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref
         return BR_FAILED;
     scoped_anum r(am);
     am.div(val1, val2, r);
-    result = m_util.mk_numeral(r, false);
+    result = m_util.mk_numeral(am, r.get(), false);
     return BR_DONE;
 }
 
@@ -1351,7 +1351,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
             am.root(r, u_den_y, r);
             if (is_neg_y)
                 am.inv(r);
-            result = m_util.mk_numeral(r, false);
+            result = m_util.mk_numeral(am, r, false);
             return BR_DONE;
         }
         return BR_FAILED;
@@ -1370,7 +1370,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
     am.root(r, u_den_y, r);
     if (is_neg_y)
         am.inv(r);
-    result = m_util.mk_numeral(r, false);
+    result = m_util.mk_numeral(am, r, false);
     return BR_DONE;
 }
 
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 09343dbf984..779a07d2ddc 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -449,7 +449,7 @@ namespace algebraic_numbers {
         }
 
         void copy_poly(algebraic_cell * c, unsigned sz, mpz const * p) {
-            SASSERT(c->m_p == 0);
+            SASSERT(c->m_p == nullptr);
             SASSERT(c->m_p_sz == 0);
             c->m_p_sz = sz;
             c->m_p    = static_cast<mpz*>(m_allocator.allocate(sizeof(mpz)*sz));
@@ -476,7 +476,7 @@ namespace algebraic_numbers {
             target->m_sign_lower   = source->m_sign_lower;
             target->m_not_rational = source->m_not_rational;
             target->m_i            = source->m_i;
-            SASSERT(acell_inv(*source));
+            //SASSERT(acell_inv(*source)); source could be owned by a different manager
             SASSERT(acell_inv(*target));
         }
 
diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp
index 10286520a4e..8de4781992b 100644
--- a/src/nlsat/tactic/nlsat_tactic.cpp
+++ b/src/nlsat/tactic/nlsat_tactic.cpp
@@ -105,13 +105,13 @@ class nlsat_tactic : public tactic {
                     continue;
                 expr * v;
                 try {
-                    v = util.mk_numeral(m_solver.value(x), util.is_int(t));
+                    v = util.mk_numeral(m_solver.am(), m_solver.value(x), util.is_int(t));
                 }
                 catch (z3_error & ex) {
                     throw ex;
                 }
                 catch (z3_exception &) {
-                    v = util.mk_to_int(util.mk_numeral(m_solver.value(x), false));
+                    v = util.mk_to_int(util.mk_numeral(m_solver.am(), m_solver.value(x), false));
                     ok = false;
                 }
                 md->register_decl(to_app(t)->get_decl(), v);
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 5fdd2a1d77a..a332a651cfa 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -796,13 +796,13 @@ namespace qe {
                     continue;
                 expr * v;
                 try {
-                    v = util.mk_numeral(s.m_rmodel0.value(x), util.is_int(t));
+                    v = util.mk_numeral(s.m_solver.am(), s.m_rmodel0.value(x), util.is_int(t));
                 }
                 catch (z3_error & ex) {
                     throw ex;
                 }
                 catch (z3_exception &) {
-                    v = util.mk_to_int(util.mk_numeral(s.m_rmodel0.value(x), false));
+                    v = util.mk_to_int(util.mk_numeral(s.m_solver.am(), s.m_rmodel0.value(x), false));
                     ok = false;
                 }
                 md->register_decl(to_app(t)->get_decl(), v);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 101f74bf925..a4df8e81a0a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3454,7 +3454,7 @@ class theory_lra::imp {
             if (a.is_int(o) && !m_nla->am().is_int(an)) {
                 return alloc(expr_wrapper_proc, a.mk_numeral(rational::zero(), a.is_int(o)));
             }
-            return alloc(expr_wrapper_proc, a.mk_numeral(nl_value(v, *m_a1), a.is_int(o)));
+            return alloc(expr_wrapper_proc, a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o)));
         }
         else {
             rational r = get_value(v);
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 9f0cf5369b3..22147af6396 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -31,6 +31,7 @@ class mpq {
     mpq():m_den(1) {}
     mpq(mpq &&) noexcept = default;
     mpq & operator=(mpq&&) = default;
+    mpq & operator=(mpq const&) = delete;
     void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); }
     mpz const & numerator() const { return m_num; }
     mpz const & denominator() const { return m_den; }
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 3a7922e1333..17db5a2279d 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -202,12 +202,14 @@ mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
     }
 #endif
     cell->m_capacity = capacity;
+
     return cell;
 }
 
 template<bool SYNCH>
 void mpz_manager<SYNCH>::deallocate(bool is_heap, mpz_cell * ptr) { 
     if (is_heap) {
+
 #ifdef SINGLE_THREAD
         m_allocator.deallocate(cell_size(ptr->m_capacity), ptr); 
 #else
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 36e6709ee31..28fa2880bdd 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -106,6 +106,7 @@ class mpz {
         std::swap(m_ptr, other.m_ptr);
     }
 
+    mpz& operator=(mpz const& other) = delete;
     mpz& operator=(mpz &&other) {
         swap(other);
         return *this;
@@ -535,13 +536,6 @@ class mpz_manager {
         }
     }
 
-    void set(mpz & target, mpz && source) {
-        target.m_val = source.m_val;
-        std::swap(target.m_ptr, source.m_ptr);
-        auto o = target.m_owner; target.m_owner = source.m_owner; source.m_owner = o;
-        auto k = target.m_kind; target.m_kind = source.m_kind; source.m_kind = k;
-    }
-
     void set(mpz & a, int val) {
         a.m_val = val;
         a.m_kind = mpz_small;
@@ -724,6 +718,7 @@ class mpz_manager {
     
     // Store the digits of n into digits, and return the sign.
     bool decompose(mpz const & n, svector<digit_t> & digits);
+
 };
 
 #ifndef SINGLE_THREAD