diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 341e26c36..4aeda7a5c 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -3410,7 +3410,7 @@ bool ast_manager::is_hyper_resolve(
             SASSERT(params[i+1].is_int());
             unsigned x = static_cast<unsigned>(params[i].get_int());
             unsigned y = static_cast<unsigned>(params[i+1].get_int());
-            positions.push_back(std::move(std::make_pair(x, y)));
+            positions.push_back(std::make_pair(x, y));
             substs.push_back(expr_ref_vector(*this));
             ++i;
         }
diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp
index 5553a6e9b..2b7e72a91 100644
--- a/src/ast/ast_pp_util.cpp
+++ b/src/ast/ast_pp_util.cpp
@@ -57,7 +57,7 @@ void ast_pp_util::display_decls(std::ostream& out) {
     recfun::util u(m);
     for (unsigned i = m_rec_decls; i < n; ++i) {
         func_decl* f = coll.get_rec_decls()[i];
-        recfuns.push_back(std::move(std::make_pair(f, u.get_def(f).get_rhs())));
+        recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs()));
     }
     if (!recfuns.empty())
         ast_smt2_pp_recdefs(out, recfuns, m_env);
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index aa67973b3..d601635be 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -538,7 +538,7 @@ class smt2_printer {
         m_expr2alias->insert(n, idx);
         m_aliased_exprs.push_back(n);
         m_aliased_pps.push_back(nf);
-        m_aliased_lvls_names.push_back(std::move(std::make_pair(lvl, name)));
+        m_aliased_lvls_names.push_back(std::make_pair(lvl, name));
     }
 
     void push_frame(expr * n, bool use_alias) {
diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp
index 1300e90d7..00d9c0726 100644
--- a/src/ast/euf/euf_mam.cpp
+++ b/src/ast/euf/euf_mam.cpp
@@ -3025,7 +3025,7 @@ namespace euf {
                     m_compiler.insert(tree, qa, mp, first_idx, false);
             }
             DEBUG_CODE(if (first_idx == 0) {
-                m_trees[lbl_id]->get_patterns().push_back(std::move(std::make_pair(qa, mp)));
+                m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
                 ctx.get_trail().push(push_back_trail<std::pair<quantifier*, app*>, false>(m_trees[lbl_id]->get_patterns()));
             });
             TRACE(trigger_bug, tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
diff --git a/src/ast/pp.cpp b/src/ast/pp.cpp
index 7b3dddb2d..9c4c10c69 100644
--- a/src/ast/pp.cpp
+++ b/src/ast/pp.cpp
@@ -71,7 +71,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
     unsigned i;
     int space_left;
     svector<std::pair<format *, unsigned> > todo;
-    todo.push_back(std::move(std::make_pair(f, 0)));
+    todo.push_back(std::make_pair(f, 0));
     app_ref  space(mk_string(m, " "), fm(m));
     while (!todo.empty()) {
         if (line >= max_num_lines)
@@ -94,28 +94,28 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
             out << f->get_decl()->get_parameter(0).get_symbol();
             break;
         case OP_INDENT:
-            todo.push_back(std::move(std::make_pair(to_app(f->get_arg(0)), 
+            todo.push_back(std::make_pair(to_app(f->get_arg(0)), 
                                           std::min(indent + f->get_decl()->get_parameter(0).get_int(),
-                                                   max_indent))));
+                                                   max_indent)));
             break;
         case OP_COMPOSE:
             i = f->get_num_args();
             while (i > 0) {
                 --i;
-                todo.push_back(std::move(std::make_pair(to_app(f->get_arg(i)), indent)));
+                todo.push_back(std::make_pair(to_app(f->get_arg(i)), indent));
             }
             break;
         case OP_CHOICE:
             space_left = std::min(max_width - pos, max_ribbon - pos);
             if (space_left > 0 && fits(m, to_app(f->get_arg(0)), space_left)) 
-                todo.push_back(std::move(std::make_pair(to_app(f->get_arg(0)), indent)));
+                todo.push_back(std::make_pair(to_app(f->get_arg(0)), indent));
             else
-                todo.push_back(std::move(std::make_pair(to_app(f->get_arg(1)), indent)));
+                todo.push_back(std::make_pair(to_app(f->get_arg(1)), indent));
             break;
         case OP_LINE_BREAK:
         case OP_LINE_BREAK_EXT:
             if (single_line) {
-                todo.push_back(std::move(std::make_pair(space, indent)));
+                todo.push_back(std::make_pair(space, indent));
                 break;
             }
             pos = indent;
diff --git a/src/ast/rewriter/factor_rewriter.cpp b/src/ast/rewriter/factor_rewriter.cpp
index 33333ce9f..89354b236 100644
--- a/src/ast/rewriter/factor_rewriter.cpp
+++ b/src/ast/rewriter/factor_rewriter.cpp
@@ -156,8 +156,8 @@ void factor_rewriter::mk_is_negative(expr_ref& result, expr_ref_vector& eqs) {
 // m_muls: list of products
 void factor_rewriter::mk_adds(expr* arg1, expr* arg2) {
     m_adds.reset();
-    m_adds.push_back(std::move(std::make_pair(arg1, true)));
-    m_adds.push_back(std::move(std::make_pair(arg2, false)));
+    m_adds.push_back(std::make_pair(arg1, true));
+    m_adds.push_back(std::make_pair(arg2, false));
     rational k;
     for (unsigned i = 0; i < m_adds.size();) {
         bool sign = m_adds[i].second;
@@ -173,13 +173,13 @@ void factor_rewriter::mk_adds(expr* arg1, expr* arg2) {
         if (a().is_add(e) && e->get_num_args() > 0) {
             m_adds[i].first = e->get_arg(0);
             for (unsigned j = 1; j < e->get_num_args(); ++j) {
-                m_adds.push_back(std::move(std::make_pair(e->get_arg(j),sign)));
+                m_adds.push_back(std::make_pair(e->get_arg(j),sign));
             }            
         }
         else if (a().is_sub(e) && e->get_num_args() > 0) {
             m_adds[i].first = e->get_arg(0);
             for (unsigned j = 1; j < e->get_num_args(); ++j) {
-                m_adds.push_back(std::move(std::make_pair(e->get_arg(j),!sign)));
+                m_adds.push_back(std::make_pair(e->get_arg(j),!sign));
             }
         }
         else if (a().is_uminus(e)) {
diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index e8ff1a15e..95d06f3a2 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -93,7 +93,7 @@ struct pb2bv_rewriter::imp {
         void sort_args() {
             vector<ca> cas;
             for (unsigned i = 0; i < m_args.size(); ++i) {
-                cas.push_back(std::move(std::make_pair(m_coeffs[i], expr_ref(m_args.get(i), m))));
+                cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args.get(i), m)));
             }
             std::sort(cas.begin(), cas.end(), compare_coeffs());
             m_coeffs.reset();
diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp
index 1d4baf526..4f7de21b0 100644
--- a/src/ast/rewriter/pb_rewriter.cpp
+++ b/src/ast/rewriter/pb_rewriter.cpp
@@ -209,7 +209,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
 
     vector<std::pair<expr*,rational> > vec;
     for (unsigned i = 0; i < num_args; ++i) {
-        vec.push_back(std::move(std::make_pair(args[i], m_util.get_coeff(f, i))));
+        vec.push_back(std::make_pair(args[i], m_util.get_coeff(f, i)));
     }
     
     switch(f->get_decl_kind()) {
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index e48ea7f21..86bb297e9 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4984,7 +4984,7 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
         all_ranges = true;
         unsigned ch = 0, ch2 = 0;
         svector<std::pair<unsigned, unsigned>> ranges, ranges1;
-        ranges.push_back(std::move(std::make_pair(0, u().max_char())));
+        ranges.push_back(std::make_pair(0, u().max_char()));
         auto exclude_range = [&](unsigned lower, unsigned upper) {
             SASSERT(lower <= upper);
             if (lower == 0) {
diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index e058392f2..3c0eb9173 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1985,7 +1985,7 @@ namespace dd {
                     continue;
                 }
                 while (!m.is_val(n)) {
-                    m_nodes.push_back(std::move(std::make_pair(true, n)));
+                    m_nodes.push_back(std::make_pair(true, n));
                     m_mono.vars.push_back(m.var(n));
                     n = m.hi(n);
                 }
@@ -2002,14 +2002,14 @@ namespace dd {
         unsigned n = m_pdd.root;
         auto& m = m_pdd.manager();
         while (!m.is_val(n)) {
-            m_nodes.push_back(std::move(std::make_pair(true, n)));
+            m_nodes.push_back(std::make_pair(true, n));
             m_mono.vars.push_back(m.var(n));
             n = m.hi(n);
         }
         m_mono.coeff = m.val(n);
         // if m_pdd is constant and non-zero, the iterator should return a single monomial
         if (m_nodes.empty() && !m_mono.coeff.is_zero())
-            m_nodes.push_back(std::move(std::make_pair(false, n)));
+            m_nodes.push_back(std::make_pair(false, n));
     }
 
     pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); }
diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index e5d414c99..714eabc3a 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -285,7 +285,7 @@ namespace lp {
         std::ostream& print_lar_term_L(const std_vector<iv>& t, std::ostream& out) const {
             vector<std::pair<mpq, unsigned>> tp;
             for (const auto& p : t) {
-                tp.push_back(std::move(std::make_pair(p.coeff(), p.var())));
+                tp.push_back(std::make_pair(p.coeff(), p.var()));
             }
             return print_linear_combination_customized(
                 tp, [](int j) -> std::string { return "x" + std::to_string(j); }, out);
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 620731615..5c93b12db 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -957,7 +957,7 @@ namespace lp {
 
         for (auto& [v, c] : coeffs)
             if (!is_zero(c))
-                left_side.push_back(std::move(std::make_pair(c, v)));        
+                left_side.push_back(std::make_pair(c, v));        
     }
 
     void lar_solver::add_touched_row(unsigned rid) {
@@ -2731,8 +2731,8 @@ namespace lp {
 
     bool lar_solver::are_equal(lpvar j, lpvar k) {
         vector<std::pair<mpq, lpvar>> coeffs;        
-        coeffs.push_back(std::move(std::make_pair(mpq(1), j)));
-        coeffs.push_back(std::move(std::make_pair(mpq(-1), k)));
+        coeffs.push_back(std::make_pair(mpq(1), j));
+        coeffs.push_back(std::make_pair(mpq(-1), k));
         lar_term t(coeffs);
         subst_known_terms(&t);
         return t.is_empty();
@@ -2741,8 +2741,8 @@ namespace lp {
     std::pair<constraint_index, constraint_index> lar_solver::add_equality(lpvar j, lpvar k) {
         vector<std::pair<mpq, lpvar>> coeffs;
         
-        coeffs.push_back(std::move(std::make_pair(mpq(1), j)));
-        coeffs.push_back(std::move(std::make_pair(mpq(-1), k)));
+        coeffs.push_back(std::make_pair(mpq(1), j));
+        coeffs.push_back(std::make_pair(mpq(-1), k));
         unsigned ej = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var
             
 
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index c1d5e77a1..34f2f0a1b 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -774,7 +774,7 @@ std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
         unsigned arity = mon.vars().size();
         auto it = m.find(arity);
         if (it == m.end()) {
-            it = m.insert(it, std::move(std::make_pair(arity, unsigned_vector())));
+            it = m.insert(it, std::make_pair(arity, unsigned_vector()));
         }
         it->second.push_back(mon.var());
     }
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index cd783c6f8..f6c15bd8b 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -112,7 +112,7 @@ void intervals::add_mul_of_degree_one_to_vector(const nex_mul* e, vector<std::pa
     SASSERT((*e)[0].pow() == 1);
     const nex *ev = (*e)[0].e();
     lpvar j = to_var(ev)->var();
-    v.push_back(std::move(std::make_pair(e->coeff(), j)));
+    v.push_back(std::make_pair(e->coeff(), j));
 }
 
 void intervals::add_linear_to_vector(const nex* e, vector<std::pair<rational, lpvar>> &v) {
@@ -122,7 +122,7 @@ void intervals::add_linear_to_vector(const nex* e, vector<std::pair<rational, lp
         add_mul_of_degree_one_to_vector(to_mul(e), v);
         break; 
     case expr_type::VAR:
-        v.push_back(std::move(std::make_pair(rational(1), to_var(e)->var())));
+        v.push_back(std::make_pair(rational(1), to_var(e)->var()));
         break;
     default:
         SASSERT(!e->is_sum());
diff --git a/src/model/model_macro_solver.cpp b/src/model/model_macro_solver.cpp
index 992e55180..64881482e 100644
--- a/src/model/model_macro_solver.cpp
+++ b/src/model/model_macro_solver.cpp
@@ -513,7 +513,7 @@ void non_auf_macro_solver::collect_candidates(ptr_vector<quantifier> const& qs,
                 TRACE(model_finder, tout << "considering macro for: " << f->get_name() << "\n";
                 m->display(tout); tout << "\n";);
                 if (m->is_unconditional() && (!qi->is_auf() || m->get_weight() >= m_mbqi_force_template)) {
-                    full_macros.insert(f, std::move(std::make_pair(m, q)));
+                    full_macros.insert(f, std::make_pair(m, q));
                     cond_macros.erase(f);
                 }
                 else if (!full_macros.contains(f) && !qi->is_auf())
diff --git a/src/muz/base/dl_boogie_proof.cpp b/src/muz/base/dl_boogie_proof.cpp
index d7cf39707..889ec8a32 100644
--- a/src/muz/base/dl_boogie_proof.cpp
+++ b/src/muz/base/dl_boogie_proof.cpp
@@ -107,7 +107,7 @@ namespace datalog {
                     for (unsigned k = 1; k < premises1.size(); ++k) {
                         if (m.get_fact(premises1[k].get()) == lit) {
                             premises2.push_back(premises1[k].get());
-                            positions2.push_back(std::move(std::make_pair(j+1,0)));
+                            positions2.push_back(std::make_pair(j+1,0));
                             substs2.push_back(expr_ref_vector(m));
                             break;
                         }
@@ -220,7 +220,7 @@ namespace datalog {
                     unsigned sz = sub.size();
                     SASSERT(sz == q->get_num_decls());
                     for (unsigned i = 0; i < sz; ++i) {
-                        s.push_back(std::move(std::make_pair(q->get_decl_name(sz-1-i), sub[i])));
+                        s.push_back(std::make_pair(q->get_decl_name(sz-1-i), sub[i]));
                     }
                     return;
                 }
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index 012e96ee8..975d4e721 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -334,7 +334,7 @@ namespace datalog {
         proof_ref_vector premises(m);
         premises.push_back(m.mk_asserted(fml1));
         premises.push_back(m.mk_asserted(fml2));
-        positions.push_back(std::move(std::make_pair(idx+1, 0)));
+        positions.push_back(std::make_pair(idx+1, 0));
 
         TRACE(dl, 
               tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
@@ -372,7 +372,7 @@ namespace datalog {
         proof_ref_vector premises(m);
         premises.push_back(r1.get_proof());
         premises.push_back(r2.get_proof());
-        positions.push_back(std::move(std::make_pair(idx+1, 0)));
+        positions.push_back(std::make_pair(idx+1, 0));
 
         TRACE(dl, 
               tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 3abc8739a..b2feb4b92 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -319,7 +319,7 @@ namespace datalog {
                     }
                     proof* premises[2] = { pr, p };
 
-                    positions.push_back(std::move(std::make_pair(0, 1)));
+                    positions.push_back(std::make_pair(0, 1));
 
                     substs.push_back(sub1);
                     substs.push_back(sub);
@@ -547,7 +547,7 @@ namespace datalog {
                 app* body_j = r->get_tail(j);
                 prop_body = vs(body_j, sub.size(), sub.data());
                 prs.push_back(get_proof(md, head_j, to_app(prop_body), level-1));
-                positions.push_back(std::move(std::make_pair(j+1,0)));
+                positions.push_back(std::make_pair(j+1,0));
                 substs.push_back(expr_ref_vector(m));
             }
             pr = m.mk_hyper_resolve(sz+1, prs.data(), prop, positions, substs);
@@ -1082,7 +1082,7 @@ namespace datalog {
                         }
 
                         prs.push_back(get_proof(md, to_app(trace->get_arg(j)), path1));
-                        positions.push_back(std::move(std::make_pair(j+1,0)));
+                        positions.push_back(std::make_pair(j+1,0));
                         substs.push_back(expr_ref_vector(m));
                     }
                     head = rl->get_head();
@@ -1256,7 +1256,7 @@ namespace datalog {
                     scoped_proof _sp(m);
                     proof* premises[2] = { pr, p };
 
-                    positions.push_back(std::move(std::make_pair(0, 1)));
+                    positions.push_back(std::make_pair(0, 1));
 
                     substs.push_back(sub1);
                     substs.push_back(sub);
diff --git a/src/muz/rel/dl_bound_relation.cpp b/src/muz/rel/dl_bound_relation.cpp
index f36e37ab7..2a078d8f7 100644
--- a/src/muz/rel/dl_bound_relation.cpp
+++ b/src/muz/rel/dl_bound_relation.cpp
@@ -534,10 +534,10 @@ namespace datalog {
             }
             uint_set2& src = (*m_elems)[j];
             for (unsigned idx : src.lt) {
-                m_todo.push_back(std::move(std::make_pair(idx, true)));
+                m_todo.push_back(std::make_pair(idx, true));
             }
             for (unsigned idx : src.le) {
-                m_todo.push_back(std::move(std::make_pair(idx, strict)));
+                m_todo.push_back(std::make_pair(idx, strict));
             }
             if (strict) {
                 dst.lt.insert(j);
@@ -551,14 +551,14 @@ namespace datalog {
     void bound_relation::mk_lt(unsigned i, unsigned j) {
         m_todo.reset();
         i = find(i);
-        m_todo.push_back(std::move(std::make_pair(find(j), true)));
+        m_todo.push_back(std::make_pair(find(j), true));
         mk_lt(i);
     }
 
     void bound_relation::mk_le(unsigned i, unsigned j) {
         m_todo.reset();
         i = find(i);
-        m_todo.push_back(std::move(std::make_pair(find(j), false)));
+        m_todo.push_back(std::make_pair(find(j), false));
         mk_lt(i);
     }
 
diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index 01d94ee6b..ef486a2f6 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -76,7 +76,7 @@ namespace datalog {
         for(unsigned i = 0; i < n; ++i) {
             unsigned sz = reg(i) ? reg(i)->get_size_estimate_bytes() : 0;
             total_bytes += sz;
-            sizes.push_back(std::move(std::make_pair(i, sz)));
+            sizes.push_back(std::make_pair(i, sz));
         }
         std::sort(sizes.begin(), sizes.end(), compare_size_proc());        
 
diff --git a/src/muz/rel/dl_product_relation.cpp b/src/muz/rel/dl_product_relation.cpp
index 3bf69f443..7dd9056f6 100644
--- a/src/muz/rel/dl_product_relation.cpp
+++ b/src/muz/rel/dl_product_relation.cpp
@@ -896,10 +896,10 @@ namespace datalog {
                 for (unsigned j = i + 1; j < r.size(); ++j) {
                     relation_mutator_fn& m2 = *(m_mutators[j]);  
                     if (m1.supports_attachment(r[j])) {
-                        m_attach.push_back(std::move(std::make_pair(i,j)));
+                        m_attach.push_back(std::make_pair(i,j));
                     }
                     if (m2.supports_attachment(r[i])) {
-                        m_attach.push_back(std::move(std::make_pair(j,i)));
+                        m_attach.push_back(std::make_pair(j,i));
                     }
                 }
             }
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index cd074cf10..20735cfcc 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -547,7 +547,7 @@ namespace datalog {
         get_rmanager().reset_saturated_marks();
         get_relation(pred).add_fact(fact);
         if (!m_context.print_aig().is_null()) {
-            m_table_facts.push_back(std::move(std::make_pair(pred, fact)));
+            m_table_facts.push_back(std::make_pair(pred, fact));
         }
     }
 
diff --git a/src/muz/spacer/spacer_sat_answer.cpp b/src/muz/spacer/spacer_sat_answer.cpp
index 175e01722..70f8d76f3 100644
--- a/src/muz/spacer/spacer_sat_answer.cpp
+++ b/src/muz/spacer/spacer_sat_answer.cpp
@@ -187,7 +187,7 @@ proof *ground_sat_answer_op::mk_proof_step(frame &fr) {
     for (auto &k : fr.m_kids) {premises.push_back(m_cache.find(k));}
 
     for (unsigned i = 0; i < premises.size(); ++i) {
-        positions.push_back(std::move(std::make_pair(0,i)));
+        positions.push_back(std::make_pair(0,i));
     }
     for (unsigned i = 0; i <= premises.size(); ++i) {
         substs.push_back(expr_ref_vector(m));
diff --git a/src/muz/spacer/spacer_sym_mux.cpp b/src/muz/spacer/spacer_sym_mux.cpp
index b177efe40..11b5097f2 100644
--- a/src/muz/spacer/spacer_sym_mux.cpp
+++ b/src/muz/spacer/spacer_sym_mux.cpp
@@ -54,14 +54,14 @@ void sym_mux::register_decl(func_decl *fdecl) {
     entry->m_variants.push_back(mk_variant(fdecl, 1));
 
     m_entries.insert(fdecl, entry);
-    m_muxes.insert(entry->m_variants.get(0), std::move(std::make_pair(entry, 0)));
-    m_muxes.insert(entry->m_variants.get(1), std::move(std::make_pair(entry, 1)));
+    m_muxes.insert(entry->m_variants.get(0), std::make_pair(entry, 0));
+    m_muxes.insert(entry->m_variants.get(1), std::make_pair(entry, 1));
 }
 void sym_mux::ensure_capacity(sym_mux_entry &entry, unsigned sz) const {
     while (entry.m_variants.size() < sz) {
         unsigned idx = entry.m_variants.size();
         entry.m_variants.push_back (mk_variant(entry.m_main, idx));
-        m_muxes.insert(entry.m_variants.back(), std::move(std::make_pair(&entry, idx)));
+        m_muxes.insert(entry.m_variants.back(), std::make_pair(&entry, idx));
     }
 }
 
diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp
index 126025456..40060629d 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.cpp
+++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp
@@ -154,7 +154,7 @@ namespace spacer {
                     if (m_ctx.is_b_pure (premise)) {
                         if (!m_use_constant_from_a) {
                             rational coefficient = params[i].get_rational();
-                            coeff_lits.push_back(std::move(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))));
+                            coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
                         }
                     }
                     else {
@@ -163,14 +163,14 @@ namespace spacer {
 
                         if (m_use_constant_from_a) {
                             rational coefficient = params[i].get_rational();
-                            coeff_lits.push_back(std::move(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))));
+                            coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
                         }
                     }
                 }
                 else {
                     if (m_use_constant_from_a) {
                         rational coefficient = params[i].get_rational();
-                        coeff_lits.push_back(std::move(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))));
+                        coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
                     }
                 }
             }
@@ -199,7 +199,7 @@ namespace spacer {
                         brw.mk_not(premise, negatedPremise);
                         pinned.push_back(negatedPremise);
                         rational coefficient = params[i].get_rational();
-                        coeff_lits.push_back(std::move(std::make_pair(abs(coefficient), to_app(negatedPremise))));
+                        coeff_lits.push_back(std::make_pair(abs(coefficient), to_app(negatedPremise)));
                     }
                 }
             }
@@ -341,7 +341,7 @@ namespace spacer {
             coeff_lits_t coeff_lits;
             for (unsigned l = 0; l < matrix.num_cols(); ++l) {
                 if (!matrix.get(k,l).is_zero()) {
-                    coeff_lits.push_back(std::move(std::make_pair(matrix.get(k, l), ordered_basis[l])));
+                    coeff_lits.push_back(std::make_pair(matrix.get(k, l), ordered_basis[l]));
                 }
             }
             SASSERT(!coeff_lits.empty());
@@ -472,7 +472,7 @@ namespace spacer {
 
                         evaluation = (*model)(bounded_vectors[j][k].get());
                         if (!util.is_zero(evaluation)) {
-                            coeff_lits.push_back(std::move(std::make_pair(rational(1), ordered_basis[j])));
+                            coeff_lits.push_back(std::make_pair(rational(1), ordered_basis[j]));
                         }
                     }
                     SASSERT(!coeff_lits.empty()); // since then previous outer loop would have found solution already
diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp
index f17f4b320..a775a7033 100644
--- a/src/muz/tab/tab_context.cpp
+++ b/src/muz/tab/tab_context.cpp
@@ -1623,7 +1623,7 @@ namespace datalog {
             proof_ref_vector premises(m);
             premises.push_back(m.mk_asserted(r1.to_formula()));
             premises.push_back(m.mk_asserted(r2.to_formula()));
-            positions.push_back(std::move(std::make_pair(idx+1, 0)));
+            positions.push_back(std::make_pair(idx+1, 0));
             pr = m.mk_hyper_resolve(2, premises.data(), fml, positions, substs);
             pc.insert(pr);
         }
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index ac366eff7..9e567c902 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
@@ -119,7 +119,7 @@ namespace datalog {
                     if (a1->get_decl() == a2->get_decl() &&
                         a1->get_num_args() == a2->get_num_args()) {
                         for (unsigned k = 0; k < a1->get_num_args(); ++k) {
-                            todo.push_back(std::move(std::make_pair(a1->get_arg(k), a2->get_arg(k))));
+                            todo.push_back(std::make_pair(a1->get_arg(k), a2->get_arg(k)));
                         }
                         match(i, pat, j + 1, todo, q, conjs);
                         todo.resize(sz);
@@ -140,7 +140,7 @@ namespace datalog {
     
         if (m_funs.find(to_app(arg)->get_decl(), terms)) {
             for (unsigned k = 0; k < terms->size(); ++k) {
-                todo.push_back(std::move(std::make_pair(arg, (*terms)[k])));
+                todo.push_back(std::make_pair(arg, (*terms)[k]));
                 match(i + 1, pat, j, todo, q, conjs);
                 todo.pop_back();
             }
diff --git a/src/opt/totalizer.cpp b/src/opt/totalizer.cpp
index 33995ce28..41d730560 100644
--- a/src/opt/totalizer.cpp
+++ b/src/opt/totalizer.cpp
@@ -75,7 +75,7 @@ namespace opt {
                 m_clauses.push_back(mk_or(clause));
             }
             def = mk_not(m, mk_and(ors));
-            m_defs.push_back(std::move(std::make_pair(c, def)));            
+            m_defs.push_back(std::make_pair(c, def));            
         }
     }
 
diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index bafb26811..49736e4c3 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -578,7 +578,7 @@ namespace arith {
         TRACE(artih, tout << mk_bounded_pp(e.eq()->get_expr(), m) << "\n");
         ensure_column(e.v1());
         ensure_column(e.v2());
-        m_delayed_eqs.push_back(std::move(std::make_pair(e, false)));
+        m_delayed_eqs.push_back(std::make_pair(e, false));
         ctx.push(push_back_vector<svector<std::pair<euf::th_eq, bool>>>(m_delayed_eqs));
     }
 
diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index ce4ab1c06..6076cdfca 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -557,7 +557,7 @@ namespace arith {
             rational const& r = m_columns[var];
             if (!r.is_zero()) {
                 auto vi = register_theory_var_in_lar_solver(var);
-                m_left_side.push_back(std::move(std::make_pair(r, vi)));
+                m_left_side.push_back(std::make_pair(r, vi));
                 m_columns[var].reset();
             }
         }
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 040a0cd89..8228c7118 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1083,7 +1083,7 @@ namespace arith {
             m_nla->am().set(r, m_nla->am_value(t));
         }
         else {
-            m_todo_terms.push_back(std::move(std::make_pair(t, rational::one())));
+            m_todo_terms.push_back(std::make_pair(t, rational::one()));
             TRACE(nl_value, tout << "v" << v << " " << t << "\n";);
             TRACE(nl_value, tout << "v" << v << " := w" << t << "\n";
             lp().print_term(lp().get_term(t), tout) << "\n";);
@@ -1103,7 +1103,7 @@ namespace arith {
                     auto wi = arg.j();
                     c1 = arg.coeff() * wcoeff;
                     if (lp().column_has_term(wi)) {
-                        m_todo_terms.push_back(std::move(std::make_pair(wi, c1)));
+                        m_todo_terms.push_back(std::make_pair(wi, c1));
                     }
                     else {
                         m_nla->am().set(r1, c1.to_mpq());
diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index 8777a320b..c4e75979e 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -237,7 +237,7 @@ namespace array {
                 if (i < num_args) {
                     SASSERT(!parent_sel_set->contains(sel) || (*(parent_sel_set->find(sel)))->get_root() == sel->get_root());
                     parent_sel_set->insert(sel);
-                    todo.push_back(std::move(std::make_pair(parent_root, sel)));
+                    todo.push_back(std::make_pair(parent_root, sel));
                 }
             }
         }
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index be98839d7..3ac6da303 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -631,7 +631,7 @@ namespace bv {
         bool ok = true;
         svector<std::pair<expr*, internalize_mode>> delay;
         for (auto kv : m_delay_internalize)
-            delay.push_back(std::move(std::make_pair(kv.m_key, kv.m_value)));
+            delay.push_back(std::make_pair(kv.m_key, kv.m_value));
         flet<bool> _cheap1(m_cheap_axioms, true);
         for (auto [e, mode] : delay) 
             if (!check_delay_internalized(e))
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index dbc1479c2..65746231d 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -93,8 +93,8 @@ namespace dt {
     }
 
     void solver::oc_push_stack(enode* n) {
-        m_dfs.push_back(std::move(std::make_pair(EXIT, n)));
-        m_dfs.push_back(std::move(std::make_pair(ENTER, n)));
+        m_dfs.push_back(std::make_pair(EXIT, n));
+        m_dfs.push_back(std::make_pair(ENTER, n));
     }
 
     /**
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index 22632aa51..dec0d11f4 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -91,7 +91,7 @@ namespace euf {
         unsigned sz = m_clauses.size();
         m_clauses.push_back(cl);
         m_roots.push_back(true);
-        m_trail.push_back(std::move(std::make_pair(update::add_clause, 0)));
+        m_trail.push_back(std::make_pair(update::add_clause, 0));
         for (sat::literal lit : *cl) {
             ctx.s().set_external(lit.var());
             occurs(lit).push_back(sz);
@@ -113,7 +113,7 @@ namespace euf {
         unsigned sz = m_clauses.size();
         m_clauses.push_back(cl);
         m_roots.push_back(false);
-        m_trail.push_back(std::move(std::make_pair(update::add_clause, 0)));
+        m_trail.push_back(std::make_pair(update::add_clause, 0));
         for (sat::literal lit : *cl) {
             ctx.s().set_external(lit.var());
             occurs(lit).push_back(sz);
@@ -121,8 +121,8 @@ namespace euf {
     }
 
     void relevancy::add_to_propagation_queue(sat::literal lit) {
-        m_trail.push_back(std::move(std::make_pair(update::add_queue, lit.var())));
-        m_queue.push_back(std::move(std::make_pair(lit, nullptr)));
+        m_trail.push_back(std::make_pair(update::add_queue, lit.var()));
+        m_queue.push_back(std::make_pair(lit, nullptr));
     }
 
     void relevancy::set_relevant(sat::literal lit) {
@@ -130,7 +130,7 @@ namespace euf {
         if (n)
             mark_relevant(n);        
         m_relevant_var_ids.setx(lit.var(), true, false);
-        m_trail.push_back(std::move(std::make_pair(update::relevant_var, lit.var())));
+        m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
     }
 
     void relevancy::set_asserted(sat::literal lit) {
@@ -197,7 +197,7 @@ namespace euf {
         flush();
         if (m_qhead == m_queue.size())
             return;
-        m_trail.push_back(std::move(std::make_pair(update::set_qhead, m_qhead)));
+        m_trail.push_back(std::make_pair(update::set_qhead, m_qhead));
         while (m_qhead < m_queue.size() && !ctx.s().inconsistent() && ctx.get_manager().inc()) {
             auto const& [lit, n] = m_queue[m_qhead++];
             SASSERT(n || lit != sat::null_literal);
@@ -224,8 +224,8 @@ namespace euf {
         if (is_relevant(n))
             return;
         TRACE(relevancy, tout << "mark #" << ctx.bpp(n) << "\n");
-        m_trail.push_back(std::move(std::make_pair(update::add_queue, 0)));
-        m_queue.push_back(std::move(std::make_pair(sat::null_literal, n)));
+        m_trail.push_back(std::make_pair(update::add_queue, 0));
+        m_queue.push_back(std::make_pair(sat::null_literal, n));
     }
 
     void relevancy::mark_relevant(sat::literal lit) {
@@ -272,7 +272,7 @@ namespace euf {
             if (true_lit != sat::null_literal) 
                 set_asserted(true_lit);            
             else {
-                m_trail.push_back(std::move(std::make_pair(update::set_root, idx)));
+                m_trail.push_back(std::make_pair(update::set_root, idx));
                 m_roots[idx] = true;
             }
         next:
diff --git a/src/sat/smt/pb_internalize.cpp b/src/sat/smt/pb_internalize.cpp
index a7584b0ce..b7873f7ba 100644
--- a/src/sat/smt/pb_internalize.cpp
+++ b/src/sat/smt/pb_internalize.cpp
@@ -82,7 +82,7 @@ namespace pb {
         for (unsigned i = 0; i < lits.size(); ++i) {
             rational c = m_pb.get_coeff(t, i);
             check_unsigned(c);
-            wlits.push_back(std::move(std::make_pair(c.get_unsigned(), lits[i])));
+            wlits.push_back(std::make_pair(c.get_unsigned(), lits[i]));
         }
     }
 
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 39208cc09..a6eb4910d 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -521,7 +521,7 @@ namespace q {
                 unsigned i = 0;
                 for (expr* arg : *to_app(s)) {
                     if (!is_ground(arg) && !is_uninterp(arg) && !qb.is_free(arg))
-                        qb.var_args.push_back(std::move(std::make_pair(to_app(s), i)));
+                        qb.var_args.push_back(std::make_pair(to_app(s), i));
                     ++i;
                 }
             }
diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp
index 5451eee14..852da2f11 100644
--- a/src/smt/expr_context_simplifier.cpp
+++ b/src/smt/expr_context_simplifier.cpp
@@ -428,7 +428,7 @@ void expr_strong_context_simplifier::simplify_basic(expr* fml, expr_ref& result)
 
     done:
         if (r) {
-            cache.insert(e, std::move(std::make_pair(pos, r)));
+            cache.insert(e, std::make_pair(pos, r));
         }
 
         TRACE(expr_context_simplifier, 
@@ -704,7 +704,7 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r
 
     done:
         if (r) {
-            cache.insert(e, std::move(std::make_pair(pos, r)));
+            cache.insert(e, std::make_pair(pos, r));
         }
 
         TRACE(expr_context_simplifier, 
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 9a4505b4a..e368e137b 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -1157,7 +1157,7 @@ bool theory_seq::solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const&
             return false;
         m.inc_ref(rhs);
         m.inc_ref(ls[0]);
-        m_nth_eq2_cache.insert(std::move(std::make_pair(rhs, ls[0])));
+        m_nth_eq2_cache.insert(std::make_pair(rhs, ls[0]));
         get_trail_stack().push(remove_obj_pair_map(m, m_nth_eq2_cache, rhs, ls[0]));
         ls1.push_back(s);        
         if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx)); 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 7cff92666..ff4f5b964 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3238,14 +3238,14 @@ namespace smt {
     void context::internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy) {
         for (expr* e : asms) {
             if (is_valid_assumption(m, e)) {
-                asm2proxy.push_back(std::move(std::make_pair(e, expr_ref(e, m))));
+                asm2proxy.push_back(std::make_pair(e, expr_ref(e, m)));
             }
             else {
                 expr_ref proxy(m), fml(m);
                 proxy = m.mk_fresh_const(symbol(), m.mk_bool_sort());
                 fml = m.mk_implies(proxy, e);
                 m_asserted_formulas.assert_expr(fml);
-                asm2proxy.push_back(std::move(std::make_pair(e, proxy)));
+                asm2proxy.push_back(std::make_pair(e, proxy));
             }
         }
         // The new assertions are of the form 'proxy => assumption'
@@ -3332,7 +3332,7 @@ namespace smt {
             }
             clausep = clause::mk(m, lits.size(), lits.data(), CLS_AUX, js);
         }
-        m_tmp_clauses.push_back(std::move(std::make_pair(clausep, lits)));
+        m_tmp_clauses.push_back(std::make_pair(clausep, lits));
     }
 
     void context::reset_tmp_clauses() {
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index ad516b0ee..979c55de6 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -228,7 +228,7 @@ namespace smt {
             return false;
         if (ctx.add_fingerprint(store, store->get_owner_id(), select->get_num_args() - 1, select->get_args() + 1)) {
             TRACE(array, tout << "adding axiom2 to todo queue\n";);
-            m_axiom2_todo.push_back(std::move(std::make_pair(store, select))); 
+            m_axiom2_todo.push_back(std::make_pair(store, select)); 
             return true;
         }
         TRACE(array, tout << "axiom already instantiated: #" << store->get_owner_id() << " #" << select->get_owner_id() << "\n";);
@@ -315,7 +315,7 @@ namespace smt {
             return false; // axiom was already instantiated
         if (already_diseq(n1, n2))
             return false;
-        m_extensionality_todo.push_back(std::move(std::make_pair(n1, n2)));         
+        m_extensionality_todo.push_back(std::make_pair(n1, n2));         
         return true;
     }
 
@@ -328,7 +328,7 @@ namespace smt {
         enode * nodes[2] = { a1, a2 };
         if (!ctx.add_fingerprint(this, 1, 2, nodes))
             return; // axiom was already instantiated
-        m_congruent_todo.push_back(std::move(std::make_pair(a1, a2)));         
+        m_congruent_todo.push_back(std::make_pair(a1, a2));         
     }
 
    
@@ -838,7 +838,7 @@ namespace smt {
                 if (i < num_args) {
                     SASSERT(!parent_sel_set->contains(sel) || (*(parent_sel_set->find(sel)))->get_root() == sel->get_root());
                     parent_sel_set->insert(sel);
-                    todo.push_back(std::move(std::make_pair(parent_root, sel)));
+                    todo.push_back(std::make_pair(parent_root, sel));
                 }
             }
         }
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index c79e85a9e..14cfc943f 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1210,7 +1210,7 @@ namespace smt {
                 }
                 
                 m_diseq_watch.reserve(watch_var+1);
-                m_diseq_watch[watch_var].push_back(std::move(std::make_pair(v1, v2)));
+                m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
                 m_diseq_watch_trail.push_back(watch_var);
                 return;
             }
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index aa5169df2..c7be4804c 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -71,8 +71,8 @@ namespace smt {
     }
 
     void theory_datatype::oc_push_stack(enode * n) {
-        m_stack.push_back(std::move(std::make_pair(EXIT, n)));
-        m_stack.push_back(std::move(std::make_pair(ENTER, n)));
+        m_stack.push_back(std::make_pair(EXIT, n));
+        m_stack.push_back(std::make_pair(ENTER, n));
     }
 
 
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index a36e27933..862440e43 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -531,7 +531,7 @@ namespace smt {
             case l_false:
                 break;
             default:
-                args.push_back(std::move(std::make_pair(l, c)));
+                args.push_back(std::make_pair(l, c));
                 break;
             }
         }
diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
index adc3a6f77..aec069a02 100644
--- a/src/smt/theory_special_relations.cpp
+++ b/src/smt/theory_special_relations.cpp
@@ -1166,7 +1166,7 @@ namespace smt {
             relation& r = *kv.m_value;
             if (r.m_property != sr_po) continue;
             for (atom* ap : r.m_asserted_atoms) {
-                atoms.push_back(std::move(std::make_pair(ap->var(), ap->phase())));
+                atoms.push_back(std::make_pair(ap->var(), ap->phase()));
             }
         }
     }
diff --git a/src/smt/theory_utvpi.cpp b/src/smt/theory_utvpi.cpp
index e13be88b5..2072474b0 100644
--- a/src/smt/theory_utvpi.cpp
+++ b/src/smt/theory_utvpi.cpp
@@ -85,14 +85,14 @@ namespace smt {
 
     bool utvpi_tester::linearize(expr* e) {
         m_terms.reset();
-        m_terms.push_back(std::move(std::make_pair(e, rational(1))));
+        m_terms.push_back(std::make_pair(e, rational(1)));
         return linearize();
     }
 
     bool utvpi_tester::linearize(expr* e1, expr* e2) {
         m_terms.reset();
-        m_terms.push_back(std::move(std::make_pair(e1, rational(1))));
-        m_terms.push_back(std::move(std::make_pair(e2, rational(-1))));
+        m_terms.push_back(std::make_pair(e1, rational(1)));
+        m_terms.push_back(std::make_pair(e2, rational(-1)));
         return linearize();
     }
 
@@ -109,21 +109,21 @@ namespace smt {
             m_terms.pop_back();
             if (a.is_add(e)) {
                 for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
-                    m_terms.push_back(std::move(std::make_pair(to_app(e)->get_arg(i), mul)));
+                    m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul));
                 }
             }
             else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) {
-                m_terms.push_back(std::move(std::make_pair(e2, mul*num)));
+                m_terms.push_back(std::make_pair(e2, mul*num));
             }
             else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) {
-                m_terms.push_back(std::move(std::make_pair(e2, mul*num)));
+                m_terms.push_back(std::make_pair(e2, mul*num));
             }
             else if (a.is_sub(e, e1, e2)) {
-                m_terms.push_back(std::move(std::make_pair(e1, mul)));
-                m_terms.push_back(std::move(std::make_pair(e2, -mul)));                
+                m_terms.push_back(std::make_pair(e1, mul));
+                m_terms.push_back(std::make_pair(e2, -mul));                
             }
             else if (a.is_uminus(e, e1)) {
-                m_terms.push_back(std::move(std::make_pair(e1, -mul)));
+                m_terms.push_back(std::make_pair(e1, -mul));
             }
             else if (a.is_numeral(e, num)) {
                 m_weight += num*mul;
@@ -140,7 +140,7 @@ namespace smt {
             if (r.is_zero()) {
                 continue;
             }
-            m_terms.push_back(std::move(std::make_pair(kv.m_key, r)));
+            m_terms.push_back(std::make_pair(kv.m_key, r));
             if (m_terms.size() > 2) {
                 return false;
             }