diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index cac12413e..9116c5d95 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -768,7 +768,7 @@ func_decl * basic_decl_plugin::mk_compressed_proof_decl(char const * name, basic
 
 func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, ptr_vector<func_decl> & cache) {
     if (num_parents >= cache.size()) {
-        cache.resize(num_parents+1, 0);
+        cache.resize(num_parents+1);
     }
     if (cache[num_parents] == 0) {
         cache[num_parents] = mk_proof_decl(name, k, num_parents);
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 4eb43d30b..54f8f5e62 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -121,6 +121,20 @@ public:
     explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
     parameter(parameter const&);
 
+    parameter(parameter && other) noexcept : m_kind(other.m_kind) {
+        switch (other.m_kind) {
+        case PARAM_INT: m_int = other.get_int(); break;
+        case PARAM_AST: m_ast = other.get_ast(); break;
+        case PARAM_SYMBOL: m_symbol = other.m_symbol; break;
+        case PARAM_RATIONAL: m_rational = 0; std::swap(m_rational, other.m_rational); break;
+        case PARAM_DOUBLE: m_dval = other.m_dval; break;
+        case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
+        default:
+            UNREACHABLE();
+            break;
+        }
+    }
+
     ~parameter();
 
     parameter& operator=(parameter const& other);
diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp
index 770832d1f..628c777d3 100644
--- a/src/ast/pattern/expr_pattern_match.cpp
+++ b/src/ast/pattern/expr_pattern_match.cpp
@@ -179,11 +179,11 @@ expr_pattern_match::compile(expr* q)
     }
 
     if (m_regs.size() <= max_reg) {
-        m_regs.resize(max_reg+1, 0);
+        m_regs.resize(max_reg+1);
     }
     if (m_bound_dom.size() <= num_bound) {
-        m_bound_dom.resize(num_bound+1, 0);
-        m_bound_rng.resize(num_bound+1, 0);
+        m_bound_dom.resize(num_bound+1);
+        m_bound_rng.resize(num_bound+1);
     }
     
     instr.m_kind = YIELD;
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index cd66a5124..a80994f6c 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -272,7 +272,7 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
         zero = m().mk_false();
 
         vector< expr_ref_vector > pps;
-        pps.resize(sz, m());
+        pps.resize(sz, expr_ref_vector(m()));
                
         for (unsigned i = 0; i < sz; i++) {
             checkpoint();
diff --git a/src/ast/substitution/substitution_tree.cpp b/src/ast/substitution/substitution_tree.cpp
index 9befb582f..20d5f1590 100644
--- a/src/ast/substitution/substitution_tree.cpp
+++ b/src/ast/substitution/substitution_tree.cpp
@@ -256,7 +256,7 @@ void substitution_tree::insert(expr * new_expr) {
         sort * s    = to_var(new_expr)->get_sort();
         unsigned id = s->get_decl_id();
         if (id >= m_vars.size())
-            m_vars.resize(id+1, 0);
+            m_vars.resize(id+1);
         if (m_vars[id] == 0)
             m_vars[id] = alloc(var_ref_vector, m_manager);
         var_ref_vector * v = m_vars[id];
@@ -277,7 +277,7 @@ void substitution_tree::insert(app * new_expr) {
     unsigned id   = d->get_decl_id();
     
     if (id >= m_roots.size()) 
-        m_roots.resize(id+1, 0);
+        m_roots.resize(id+1);
 
     if (!m_roots[id]) {
         // there is no tree for the function symbol heading new_expr
diff --git a/src/ast/used_vars.cpp b/src/ast/used_vars.cpp
index a1cd65feb..a3030f087 100644
--- a/src/ast/used_vars.cpp
+++ b/src/ast/used_vars.cpp
@@ -58,7 +58,7 @@ void used_vars::process(expr * n, unsigned delta) {
             if (idx >= delta) {
                 idx = idx - delta;
                 if (idx >= m_found_vars.size())
-                    m_found_vars.resize(idx + 1, 0);
+                    m_found_vars.resize(idx + 1);
                 m_found_vars[idx] = to_var(n)->get_sort();
             }
             break;
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 22b50326b..9484c3c83 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -2632,10 +2632,14 @@ namespace algebraic_numbers {
                 scoped_mpz neg_n(qm());
                 qm().set(neg_n, v.numerator());
                 qm().neg(neg_n);
-                mpz const coeffs[2] = { neg_n.get(), v.denominator() };
+                unsynch_mpz_manager zmgr;
+                // FIXME: remove these copies
+                mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
                 out << "(";
                 upm().display(out, 2, coeffs, "#");
                 out << ", 1)"; // first root of the polynomial d*# - n
+                zmgr.del(coeffs[0]);
+                zmgr.del(coeffs[1]);
             }
             else {
                 algebraic_cell * c = a.to_algebraic();
@@ -2678,10 +2682,14 @@ namespace algebraic_numbers {
                 scoped_mpz neg_n(qm());
                 qm().set(neg_n, v.numerator());
                 qm().neg(neg_n);
-                mpz const coeffs[2] = { neg_n.get(), v.denominator() };
+                unsynch_mpz_manager zmgr;
+                // FIXME: remove these copies
+                mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
                 out << "(root-obj ";
                 upm().display_smt2(out, 2, coeffs, "x");
                 out << " 1)"; // first root of the polynomial d*# - n
+                zmgr.del(coeffs[0]);
+                zmgr.del(coeffs[1]);
             }
             else {
                 algebraic_cell * c = a.to_algebraic();
diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index 7adaf9adb..d6d392148 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -4822,10 +4822,9 @@ namespace polynomial {
 
         polynomial * mk_x_minus_y(var x, var y) {
             numeral zero(0);
-            numeral one(1);
             numeral minus_one; // It is not safe to initialize with -1 when numeral_manager is GF_2
             m_manager.set(minus_one, -1);
-            numeral as[2] = { one, minus_one };
+            numeral as[2] = { numeral(1), std::move(minus_one) };
             var     xs[2] = { x, y };
             return mk_linear(2, as, xs, zero);
         }
@@ -4845,8 +4844,7 @@ namespace polynomial {
 
         polynomial * mk_x_plus_y(var x, var y) {
             numeral zero(0);
-            numeral one(1);
-            numeral as[2] = { one, one };
+            numeral as[2] = { numeral(1), numeral(1) };
             var     xs[2] = { x, y };
             return mk_linear(2, as, xs, zero);
         }
diff --git a/src/math/polynomial/upolynomial_factorization_int.h b/src/math/polynomial/upolynomial_factorization_int.h
index 640c5ad5c..ea2b51d8f 100644
--- a/src/math/polynomial/upolynomial_factorization_int.h
+++ b/src/math/polynomial/upolynomial_factorization_int.h
@@ -45,7 +45,7 @@ namespace upolynomial {
         for (unsigned i = 0; i < p.size(); ++ i) {
             numeral p_i; // no need to delete, we keep it pushed in zp_p
             zp_nm.set(p_i, p[i]);
-            zp_p.push_back(p_i);
+            zp_p.push_back(std::move(p_i));
         }
         zp_upm.trim(zp_p);
     }
diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h
index dc4ce8695..63bbe9e78 100644
--- a/src/math/simplex/sparse_matrix.h
+++ b/src/math/simplex/sparse_matrix.h
@@ -35,7 +35,7 @@ namespace simplex {
         struct row_entry {
             numeral         m_coeff;
             var_t           m_var;
-            row_entry(numeral const& c, var_t v): m_coeff(c), m_var(v) {}
+            row_entry(numeral && c, var_t v) noexcept : m_coeff(std::move(c)), m_var(v) {}
         };
 
     private:
@@ -61,7 +61,7 @@ namespace simplex {
                 int     m_col_idx;
                 int     m_next_free_row_entry_idx;
             };            
-            _row_entry(numeral const & c, var_t v): row_entry(c, v), m_col_idx(0) {}
+            _row_entry(numeral && c, var_t v) : row_entry(std::move(c), v), m_col_idx(0) {}
             _row_entry() : row_entry(numeral(), dead_id), m_col_idx(0) {}
             bool is_dead() const { return row_entry::m_var == dead_id; }
         };
diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h
index 108b6aac3..3574787d8 100644
--- a/src/math/subpaving/subpaving_t_def.h
+++ b/src/math/subpaving/subpaving_t_def.h
@@ -739,7 +739,7 @@ void context_t<C>::del_sum(polynomial * p) {
 
 template<typename C>
 var context_t<C>::mk_sum(numeral const & c, unsigned sz, numeral const * as, var const * xs) {
-    m_num_buffer.reserve(num_vars(), numeral());
+    m_num_buffer.reserve(num_vars());
     for (unsigned i = 0; i < sz; i++) {
         SASSERT(xs[i] < num_vars());
         nm().set(m_num_buffer[xs[i]], as[i]);
diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index 6699ef0e2..e458cc4b0 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -117,7 +117,7 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
         (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity)))
         return false;
 
-    args.resize(m_arity, 0);
+    args.resize(m_arity);
     for (unsigned i = 0; i < m_arity; i++) {
         expr * ci = (m_arity == 1 && i == 0) ? c : to_app(c)->get_arg(i);
 
diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h
index c29681f37..56dd249a5 100644
--- a/src/muz/rel/dl_instruction.h
+++ b/src/muz/rel/dl_instruction.h
@@ -128,7 +128,7 @@ namespace datalog {
         void set_reg(reg_idx i, reg_type val) {
             if (i >= m_registers.size()) {
                 check_overflow(i);
-                m_registers.resize(i+1,0);
+                m_registers.resize(i+1);
             }
             if (m_registers[i]) {
                 m_registers[i]->deallocate();
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index fd13978d2..c4fb57eeb 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -465,7 +465,7 @@ namespace datalog {
 
             unsigned sz = r.get_signature().size();
             ptr_vector<expr> subst_arg;
-            subst_arg.resize(sz, 0);
+            subst_arg.resize(sz);
             unsigned ofs = sz-1;
             for (unsigned i=0; i<sz; i++) {
                 SASSERT(!r.is_undefined(i) || !contains_var(m_new_rule, i));
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index dd54f4441..061f403e3 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1272,7 +1272,7 @@ namespace qe {
         family_id fid = p->get_family_id();
         SASSERT(fid != null_family_id);
         if (static_cast<int>(m_plugins.size()) <= fid) {
-            m_plugins.resize(fid+1,0);
+            m_plugins.resize(fid+1);
         }
         SASSERT(!m_plugins[fid]);
         m_plugins[fid] = p;
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 497aab8db..96334e3ce 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1999,7 +1999,7 @@ namespace smt {
             m_ast_manager(ctx.get_manager()),
             m_mam(m),
             m_use_filters(use_filters) {
-            m_args.resize(INIT_ARGS_SIZE, 0);
+            m_args.resize(INIT_ARGS_SIZE);
         }
 
         ~interpreter() {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index ac7b1f44b..48d02da26 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1286,7 +1286,7 @@ namespace smt {
         else {
             if (depth >= m_almost_cg_tables.size()) {
                 unsigned old_sz = m_almost_cg_tables.size();
-                m_almost_cg_tables.resize(depth+1, 0);
+                m_almost_cg_tables.resize(depth+1);
                 for (unsigned i = old_sz; i < depth + 1; i++)
                     m_almost_cg_tables[i] = alloc(almost_cg_table);
             }
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 1f519dfda..21df02c76 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -617,8 +617,8 @@ namespace smt {
         m_else_values.reset();
         m_parents.reset();
         m_parents.resize(num_vars, -1);
-        m_defaults.resize(num_vars, 0);
-        m_else_values.resize(num_vars, 0);
+        m_defaults.resize(num_vars);
+        m_else_values.resize(num_vars);
     
         if (m_use_unspecified_default)
             return;
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 616314117..bbed6840d 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -620,7 +620,7 @@ namespace smt {
         sort * s     = recognizer->get_decl()->get_domain(0);
         if (d->m_recognizers.empty()) {
             SASSERT(m_util.is_datatype(s));
-            d->m_recognizers.resize(m_util.get_datatype_num_constructors(s), 0);
+            d->m_recognizers.resize(m_util.get_datatype_num_constructors(s));
         }
         SASSERT(d->m_recognizers.size() == m_util.get_datatype_num_constructors(s));
         unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl());
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index 064bdd433..78fb4d03d 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -914,6 +914,8 @@ namespace smt {
                    }
                    verbose_stream() << " + " << m_objective_consts[v] << "\n";);
 
+        unsynch_mpq_manager mgr;
+        unsynch_mpq_inf_manager inf_mgr;
         unsigned num_nodes = get_num_vars();
         unsigned num_edges = m_edges.size();
         S.ensure_var(num_nodes + num_edges + m_objectives.size());
@@ -921,8 +923,9 @@ namespace smt {
             numeral const& a = m_assignment[i];
             rational fin = a.get_rational().to_rational();
             rational inf = a.get_infinitesimal().to_rational();
-            mpq_inf q(fin.to_mpq(), inf.to_mpq());
+            mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
             S.set_value(i, q);
+            inf_mgr.del(q);
         }
         for (unsigned i = 0; i < num_nodes; ++i) {
             enode * n = get_enode(i);
@@ -933,7 +936,6 @@ namespace smt {
             }
         }
         svector<unsigned> vars;
-        unsynch_mpq_manager mgr;
         scoped_mpq_vector coeffs(mgr);
         coeffs.push_back(mpq(1));
         coeffs.push_back(mpq(-1));
@@ -954,8 +956,9 @@ namespace smt {
             numeral const& w = e.m_offset;
             rational fin = w.get_rational().to_rational();
             rational inf = w.get_infinitesimal().to_rational();
-            mpq_inf q(fin.to_mpq(),inf.to_mpq());
+            mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
             S.set_upper(base_var, q);            
+            inf_mgr.del(q);
         }
         unsigned w = num_nodes + num_edges + v;
 
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index a7153234c..203dd24d2 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -1107,6 +1107,8 @@ unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
 
 template<typename Ext> 
 void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
+    unsynch_mpq_manager mgr;
+    unsynch_mpq_inf_manager inf_mgr;
     unsigned num_nodes = m_graph.get_num_nodes();
     vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
     S.ensure_var(num_simplex_vars());
@@ -1114,13 +1116,13 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
         numeral const& a = m_graph.get_assignment(i);
         rational fin = a.get_rational().to_rational();
         rational inf = a.get_infinitesimal().to_rational();
-        mpq_inf q(fin.to_mpq(), inf.to_mpq());
+        mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
         S.set_value(node2simplex(i), q);
+        inf_mgr.del(q);
     }
     S.set_lower(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
     S.set_upper(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
     svector<unsigned> vars;
-    unsynch_mpq_manager mgr;
     scoped_mpq_vector coeffs(mgr);
     coeffs.push_back(mpq(1));
     coeffs.push_back(mpq(-1));
@@ -1145,8 +1147,9 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
             numeral const& w = e.get_weight();
             rational fin = w.get_rational().to_rational();
             rational inf = w.get_infinitesimal().to_rational();
-            mpq_inf q(fin.to_mpq(),inf.to_mpq());
+            mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
             S.set_upper(base_var, q);
+            inf_mgr.del(q);
         }
         else {
             S.unset_upper(base_var);
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 4b52d7950..9d2059f55 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -806,8 +806,9 @@ namespace smt {
         if (c != 0) {
             if (m_enable_simplex) {
                 row_info const& info = m_ineq_row_info.find(v);
+                unsynch_mpq_manager mgr;
                 scoped_eps_numeral coeff(m_mpq_inf_mgr);
-                coeff = std::make_pair(info.m_bound.to_mpq(), mpq(0));
+                coeff = std::make_pair(mgr.dup(info.m_bound.to_mpq()), mpq(0));
                 unsigned slack = info.m_slack;
                 if (is_true) {
                     update_bound(slack, literal(v), true, coeff);
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 7f530e5b0..662378bdf 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -279,7 +279,6 @@ namespace smt {
         //
         void compile_ineq(ineq& c);
         void inc_propagations(ineq& c);
-        unsigned get_compilation_threshold(ineq& c);
 
         //
         // Conflict resolution, cutting plane derivation.
diff --git a/src/tactic/sls/bvsls_opt_engine.cpp b/src/tactic/sls/bvsls_opt_engine.cpp
index e8547fdfd..502bcbde6 100644
--- a/src/tactic/sls/bvsls_opt_engine.cpp
+++ b/src/tactic/sls/bvsls_opt_engine.cpp
@@ -238,7 +238,7 @@ bool bvsls_opt_engine::what_if(
 
 mpz bvsls_opt_engine::find_best_move(
     ptr_vector<func_decl> & to_evaluate,
-    mpz score,
+    mpz & score,
     unsigned & best_const,
     mpz & best_value,
     unsigned & new_bit,
diff --git a/src/tactic/sls/bvsls_opt_engine.h b/src/tactic/sls/bvsls_opt_engine.h
index 67d9a5d02..9487130d3 100644
--- a/src/tactic/sls/bvsls_opt_engine.h
+++ b/src/tactic/sls/bvsls_opt_engine.h
@@ -61,7 +61,7 @@ protected:
     bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, 
                  mpz & best_score, unsigned & best_const, mpz & best_value);
 
-    mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz score,
+    mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz & score,
                        unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
                        mpz const & max_score, expr * objective);
 
diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h
index 4ad5c65f4..b4969f433 100644
--- a/src/tactic/sls/sls_tracker.h
+++ b/src/tactic/sls/sls_tracker.h
@@ -41,7 +41,20 @@ class sls_tracker {
         
     struct value_score { 
     value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), score_prune(0.0), has_pos_occ(0), has_neg_occ(0), distance(0), touched(1) {};
+        value_score(value_score && other) :
+            m(other.m),
+            value(std::move(other.value)),
+            score(other.score),
+            score_prune(other.score_prune),
+            has_pos_occ(other.has_pos_occ),
+            has_neg_occ(other.has_neg_occ),
+            distance(other.distance),
+            touched(other.touched) {}
         ~value_score() { if (m) m->del(value); }
+        void operator=(value_score && other) {
+            this->~value_score();
+            new (this) value_score(std::move(other));
+        }
         unsynch_mpz_manager * m;
         mpz value;
         double score;
@@ -50,15 +63,6 @@ class sls_tracker {
         unsigned has_neg_occ;
         unsigned distance; // max distance from any root
         unsigned touched;
-        value_score & operator=(const value_score & other) {
-            SASSERT(m == 0 || m == other.m);
-            if (m) m->set(value, 0); else m = other.m;
-            m->set(value, other.value);
-            score = other.score;
-            distance = other.distance;
-            touched = other.touched;
-            return *this;
-        }
     };
 
 public:
@@ -294,7 +298,7 @@ public:
         if (!m_scores.contains(n)) {
             value_score vs;
             vs.m = & m_mpz_manager;
-            m_scores.insert(n, vs);
+            m_scores.insert(n, std::move(vs));
         }
 
         // Update uplinks
@@ -539,7 +543,7 @@ public:
                     rational r_val;
                     unsigned bv_sz;
                     m_bv_util.is_numeral(val, r_val, bv_sz);
-                    mpq q = r_val.to_mpq();
+                    const mpq& q = r_val.to_mpq();
                     SASSERT(m_mpz_manager.is_one(q.denominator()));
                     set_value(fd, q.numerator());
                 }
@@ -630,7 +634,7 @@ public:
         if (m_bv_util.is_bv_sort(s))
             return get_random_bv(s);
         else if (m_manager.is_bool(s))
-            return get_random_bool();
+            return m_mpz_manager.dup(get_random_bool());
         else
             NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now.
     }    
@@ -653,9 +657,7 @@ public:
         TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
 
         for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
-            mpz temp = m_zero;
-            set_value(it->m_value, temp);
-            m_mpz_manager.del(temp);
+            set_value(it->m_value, m_zero);
         }
     }              
 
@@ -931,7 +933,7 @@ public:
             rational q;
             if (!m_bv_util.is_numeral(n, q, bv_sz))
                 NOT_IMPLEMENTED_YET();
-            mpq temp = q.to_mpq();
+            const mpq& temp = q.to_mpq();
             SASSERT(m_mpz_manager.is_one(temp.denominator()));
             m_mpz_manager.set(result, temp.numerator());
         }
@@ -1039,7 +1041,6 @@ public:
         unsigned pos = -1;
         if (m_ucb)
         {
-            value_score vscore;
             double max = -1.0;
             // Andreas: Commented things here might be used for track_unsat data structures as done in SLS for SAT. But seems to have no benefit.
             /* for (unsigned i = 0; i < m_where_false.size(); i++) {
@@ -1048,7 +1049,7 @@ public:
                 expr * e = as[i];
                 if (m_mpz_manager.neq(get_value(e), m_one))
                 {
-                    vscore = m_scores.find(e);
+                    value_score & vscore = m_scores.find(e);
                     // Andreas: Select the assertion with the greatest ucb score. Potentially add some noise.
                     // double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched);
                     double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8); 
diff --git a/src/util/buffer.h b/src/util/buffer.h
index 503788fa0..c64e23d8b 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -149,6 +149,13 @@ public:
         new (m_buffer + m_pos) T(elem);
         m_pos++;
     }
+
+    void push_back(T && elem) {
+        if (m_pos >= m_capacity)
+            expand();
+        new (m_buffer + m_pos) T(std::move(elem));
+        m_pos++;
+    }
     
     void pop_back() {
         if (CallDestructors) {
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index 020c47b2b..fa9fef180 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -54,7 +54,7 @@ public:
     bool is_used() const { return m_state == HT_USED; }
     T & get_data()             { return m_data; }
     const T & get_data() const { return m_data; }
-    void set_data(const T & d) { m_data = d; m_state = HT_USED; }
+    void set_data(T && d) { m_data = std::move(d); m_state = HT_USED; }
     void set_hash(unsigned h)  { m_hash = h; }
     void mark_as_deleted() { m_state = HT_DELETED; }
     void mark_as_free() { m_state = HT_FREE; }
@@ -187,10 +187,42 @@ protected:
         } 
     }
 
+    static void move_table(entry * source, unsigned source_capacity, entry * target, unsigned target_capacity) {
+        SASSERT(target_capacity >= source_capacity);
+        unsigned target_mask = target_capacity - 1;
+        entry *  source_end = source + source_capacity;
+        entry *  target_end = target + target_capacity;
+        for (entry * source_curr = source; source_curr != source_end; ++source_curr) {
+            if (source_curr->is_used()) {
+                unsigned hash = source_curr->get_hash();
+                unsigned idx = hash & target_mask;
+                entry * target_begin = target + idx;
+                entry * target_curr = target_begin;
+                for (; target_curr != target_end; ++target_curr) {
+                    SASSERT(!target_curr->is_deleted());
+                    if (target_curr->is_free()) {
+                        *target_curr = std::move(*source_curr);
+                        goto end;
+                    }
+                }
+                for (target_curr = target; target_curr != target_begin; ++target_curr) {
+                    SASSERT(!target_curr->is_deleted());
+                    if (target_curr->is_free()) {
+                        *target_curr = std::move(*source_curr);
+                        goto end;
+                    }
+                }
+                UNREACHABLE();
+            end:
+                ;
+            }
+        }
+    }
+
     void expand_table() {
         unsigned new_capacity = m_capacity << 1;
         entry *  new_table    = alloc_table(new_capacity);
-        copy_table(m_table, m_capacity, new_table, new_capacity);
+        move_table(m_table, m_capacity, new_table, new_capacity);
         delete_table();
         m_table       = new_table;
         m_capacity    = new_capacity;
@@ -202,7 +234,7 @@ protected:
         if (memory::is_out_of_memory())
             return;
         entry * new_table = alloc_table(m_capacity);
-        copy_table(m_table, m_capacity, new_table, m_capacity);
+        move_table(m_table, m_capacity, new_table, m_capacity);
         delete_table();
         m_table       = new_table;
         m_num_deleted = 0;
@@ -321,7 +353,7 @@ public:
 #define INSERT_LOOP_BODY() {                                                            \
         if (curr->is_used()) {                                                          \
             if (curr->get_hash() == hash && equals(curr->get_data(), e)) {              \
-                curr->set_data(e);                                                      \
+                curr->set_data(std::move(e));                                           \
                 return;                                                                 \
             }                                                                           \
             HS_CODE(m_st_collision++;);                                                 \
@@ -330,7 +362,7 @@ public:
             entry * new_entry;                                                          \
             if (del_entry) { new_entry = del_entry; m_num_deleted--; }                  \
             else { new_entry = curr; }                                                  \
-            new_entry->set_data(e);                                                     \
+            new_entry->set_data(std::move(e));                                          \
             new_entry->set_hash(hash);                                                  \
             m_size++;                                                                   \
             return;                                                                     \
@@ -342,7 +374,7 @@ public:
         }                                                                               \
     } ((void) 0)
 
-    void insert(data const & e) {
+    void insert(data && e) {
         if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) {
             // if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
             expand_table();
@@ -363,6 +395,11 @@ public:
         UNREACHABLE();
     }
 
+    void insert(const data & e) {
+        data tmp(e);
+        insert(std::move(tmp));
+    }
+
 #define INSERT_LOOP_CORE_BODY() {                                               \
         if (curr->is_used()) {                                                  \
             if (curr->get_hash() == hash && equals(curr->get_data(), e)) {      \
@@ -375,7 +412,7 @@ public:
             entry * new_entry;                                                  \
             if (del_entry) { new_entry = del_entry; m_num_deleted--; }          \
             else { new_entry = curr; }                                          \
-            new_entry->set_data(e);                                             \
+            new_entry->set_data(std::move(e));                                  \
             new_entry->set_hash(hash);                                          \
             m_size++;                                                           \
             et = new_entry;                                                     \
@@ -393,7 +430,7 @@ public:
        Return true if it is a new element, and false otherwise.
        Store the entry/slot of the table in et.
     */
-    bool insert_if_not_there_core(data const & e, entry * & et) {
+    bool insert_if_not_there_core(data && e, entry * & et) {
         if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) {
             // if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
             expand_table();
@@ -415,6 +452,11 @@ public:
         return 0;
     }
 
+    bool insert_if_not_there_core(const data & e, entry * & et) {
+        data temp(e);
+        return insert_if_not_there_core(std::move(temp), et);
+    }
+
     /**
        \brief Insert the element e if it is not in the table.
        Return a reference to e or to an object identical to e
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 5aa3ca083..b34e9afae 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -31,11 +31,10 @@ class mpq {
 public:
     mpq(int v):m_num(v), m_den(1) {}
     mpq():m_den(1) {}
+    mpq(mpq && other) noexcept : m_num(std::move(other.m_num)), m_den(std::move(other.m_den)) {}
     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; }
-
-    double get_double() const;
 };
 
 inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
@@ -745,6 +744,12 @@ public:
         reset_denominator(a); 
     }
 
+    mpq dup(const mpq & source) {
+        mpq temp;
+        set(temp, source);
+        return temp;
+    }
+
     void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); }
 
     void swap(mpq & a, mpq & b) {
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 7001b9a42..bdfbc8061 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -94,6 +94,9 @@ class mpz {
 public:
     mpz(int v):m_val(v), m_ptr(0) {}
     mpz():m_val(0), m_ptr(0) {}
+    mpz(mpz && other) noexcept : m_val(other.m_val), m_ptr(0) {
+        std::swap(m_val, other.m_val);
+    }
     void swap(mpz & other) { 
         std::swap(m_val, other.m_val);
         std::swap(m_ptr, other.m_ptr);
@@ -668,6 +671,12 @@ public:
         }
     }
 
+    void set(mpz & target, mpz && source) {
+        del(target);
+        target.m_val = source.m_val;
+        std::swap(target.m_ptr, source.m_ptr);
+    }
+
     void set(mpz & a, int val) {
         del(a);
         a.m_val = val;
@@ -700,6 +709,12 @@ public:
 
     void set(mpz & target, unsigned sz, digit_t const * digits);
 
+    mpz dup(const mpz & source) {
+        mpz temp;
+        set(temp, source);
+        return temp;
+    }
+
     void reset(mpz & a) {
         del(a);
         a.m_val = 0;
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index 189d1e1a0..df279383b 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -69,6 +69,10 @@ public:
             m_key(k),
             m_value(v) {
         }
+        key_data(Key * k, Value && v) :
+            m_key(k),
+            m_value(std::move(v)) {
+        }
         Value const & get_value() const { return m_value; }
         Key & get_key () const { return *m_key; }
         unsigned hash() const { return m_key->hash(); }
@@ -86,7 +90,7 @@ public:
         bool is_used() const { return m_data.m_key != reinterpret_cast<Key *>(0) && m_data.m_key != reinterpret_cast<Key *>(1); }
         key_data const & get_data() const { return m_data; }
         key_data & get_data() { return m_data; }
-        void set_data(key_data const & d) { m_data = d; }
+        void set_data(key_data && d) { m_data = std::move(d); }
         void set_hash(unsigned h) { SASSERT(h == m_data.hash()); }
         void mark_as_deleted() { m_data.m_key = reinterpret_cast<Key *>(1); }
         void mark_as_free() { m_data.m_key = 0; }
@@ -137,6 +141,10 @@ public:
     void insert(Key * const k, Value const & v) {
         m_table.insert(key_data(k, v));
     }
+
+    void insert(Key * const k, Value && v) {
+        m_table.insert(key_data(k, std::move(v)));
+    }
     
     key_data const & insert_if_not_there(Key * k, Value const & v) {
         return m_table.insert_if_not_there(key_data(k, v));
diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index 469183b76..9b7657fb2 100644
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@@ -63,7 +63,7 @@ public:
     void resize(unsigned sz) {
         if (sz < m_nodes.size())
             dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
-        m_nodes.resize(sz, 0);
+        m_nodes.resize(sz);
     }
 
     void resize(unsigned sz, T * d) {
@@ -80,7 +80,7 @@ public:
     void reserve(unsigned sz) {
         if (sz <= m_nodes.size())
             return;
-        m_nodes.resize(sz, 0);
+        m_nodes.resize(sz);
     }
 
     void shrink(unsigned sz) {
diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h
index fdf63bf35..cb9a6b4fd 100644
--- a/src/util/scoped_numeral_vector.h
+++ b/src/util/scoped_numeral_vector.h
@@ -63,8 +63,7 @@ public:
         unsigned old_sz = this->size();
         if (sz <= old_sz)
             shrink(sz);
-        typename Manager::numeral zero(0);
-        svector<typename Manager::numeral>::resize(sz, zero);
+        svector<typename Manager::numeral>::resize(sz, 0);
     }
 };
 
diff --git a/src/util/util.h b/src/util/util.h
index 1f753099c..f8c464197 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -322,7 +322,7 @@ bool compare_arrays(const T * array1, const T * array2, unsigned size) {
 template<typename T>
 void force_ptr_array_size(T & v, unsigned sz) {
     if (sz > v.size()) {
-        v.resize(sz, 0);
+        v.resize(sz);
     }
 }
 
diff --git a/src/util/vector.h b/src/util/vector.h
index 2d499a900..c21d33bab 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -26,6 +26,7 @@ Revision History:
 
 #include "util/debug.h"
 #include<algorithm>
+#include<type_traits>
 #include<memory.h>
 #include "util/memory_manager.h"
 #include "util/hash.h"
@@ -74,9 +75,24 @@ class vector {
             if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
                 throw default_exception("Overflow encountered when expanding vector");
             }
-            SZ *mem = (SZ*)memory::reallocate(reinterpret_cast<SZ*>(m_data)-2, new_capacity_T);
+            SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
+            if (std::is_trivially_copyable<T>::value) {
+                mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
+            } else {
+                mem = (SZ*)memory::allocate(new_capacity_T);
+            }
+            auto old_data = m_data;
+            auto old_size = size();
             *mem    = new_capacity;
             m_data  = reinterpret_cast<T *>(mem + 2);
+            if (!std::is_trivially_copyable<T>::value) {
+                static_assert(std::is_move_constructible<T>::value, "");
+                int i = 0;
+                for (auto I = old_data; I != old_data + old_size; ++I) {
+                    new (&m_data[i++]) T(std::move(*I));
+                }
+                memory::deallocate(old_mem);
+            }
         }
     }
 
@@ -148,6 +164,10 @@ public:
         SASSERT(size() == source.size());
     }
 
+    vector(vector&& other) noexcept : m_data(0) {
+        std::swap(m_data, other.m_data);
+    }
+
     vector(SZ s, T const * data):
         m_data(0) {
         for (SZ i = 0; i < s; i++) {
@@ -179,6 +199,16 @@ public:
         return *this;
     }
 
+    vector & operator=(vector && source) {
+        if (this == &source) {
+            return *this;
+        }
+        destroy();
+        m_data = 0;
+        std::swap(m_data, source.m_data);
+        return *this;
+    }
+
     void reset() { 
         if (m_data) {
             if (CallDestructors) {
@@ -292,6 +322,11 @@ public:
         m_data[idx] = val;
     }
 
+    void set(SZ idx, T && val) {
+        SASSERT(idx < size());
+        m_data[idx] = std::move(val);
+    }
+
     T & back() { 
         SASSERT(!empty()); 
         return operator[](size() - 1); 
@@ -318,6 +353,14 @@ public:
         reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
     }
 
+    void push_back(T && elem) {
+        if (m_data == 0 || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
+            expand_vector();
+        }
+        new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(std::move(elem));
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
+    }
+
     void insert(T const & elem) {
         push_back(elem);
     }
@@ -357,7 +400,8 @@ public:
         }
     }
 
-    void resize(SZ s, T const & elem=T()) {
+    template<typename Args>
+    void resize(SZ s, Args args...) {
         SZ sz = size();
         if (s <= sz) { shrink(s); return; }
         while (s > capacity()) {
@@ -367,8 +411,23 @@ public:
         reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
         iterator it  = m_data + sz;
         iterator end = m_data + s;
-        for(; it != end; ++it) {
-            new (it) T(elem);
+        for (; it != end; ++it) {
+            new (it) T(std::forward<Args>(args));
+        }
+    }
+
+    void resize(SZ s) {
+        SZ sz = size();
+        if (s <= sz) { shrink(s); return; }
+        while (s > capacity()) {
+            expand_vector();
+        }
+        SASSERT(m_data != 0);
+        reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
+        iterator it  = m_data + sz;
+        iterator end = m_data + s;
+        for (; it != end; ++it) {
+            new (it) T();
         }
     }
 
@@ -439,10 +498,15 @@ public:
         return m_data[idx];
     }
 
-    void reserve(SZ s, T const & d = T()) {
+    void reserve(SZ s, T const & d) {
         if (s > size())
             resize(s, d);
     }
+
+    void reserve(SZ s) {
+        if (s > size())
+            resize(s);
+    }
 };
 
 template<typename T>
@@ -452,7 +516,12 @@ public:
     ptr_vector(unsigned s):vector<T *, false>(s) {}
     ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
     ptr_vector(ptr_vector const & source):vector<T *, false>(source) {}
+    ptr_vector(ptr_vector && other) noexcept : vector<T*, false>(std::move(other)) {}
     ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
+    ptr_vector & operator=(ptr_vector const & source) {
+        vector<T *, false>::operator=(source);
+        return *this;
+    }
 };
 
 template<typename T, typename SZ = unsigned>
@@ -462,7 +531,12 @@ public:
     svector(SZ s):vector<T, false, SZ>(s) {}
     svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
     svector(svector const & source):vector<T, false, SZ>(source) {}
+    svector(svector && other) noexcept : vector<T, false, SZ>(std::move(other)) {}
     svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
+    svector & operator=(svector const & source) {
+        vector<T, false, SZ>::operator=(source);
+        return *this;
+    }
 };
 
 typedef svector<int> int_vector;
@@ -494,23 +568,4 @@ struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> >
 template<typename Hash>
 struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
 
-#include <vector>
-// Specialize vector<std::string> to be an instance of std::vector instead.
-// This will catch any regression of issue #564 and #420.
-
-template <>
-class vector<std::string, true, unsigned> : public std::vector<std::string> {
-public:
-    vector(vector<std::string, true, unsigned> const& other): std::vector<std::string>(other) {}
-    vector(size_t sz, char const* s): std::vector<std::string>(sz, s) {}
-    vector() {}
-
-    void reset() { clear(); }
-   
-    
-};
-
-
-
 #endif /* VECTOR_H_ */
-