Apply std::move to all remaining push_back/insert with std::make_pair (~100+ files)

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

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::make_pair(lvl, name));
+        m_aliased_lvls_names.push_back(std::move(std::make_pair(lvl, name)));
     }
 
     void push_frame(expr * n, bool use_alias) {

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::make_pair(qa, mp));
+                m_trees[lbl_id]->get_patterns().push_back(std::move(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););

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::make_pair(0, u().max_char()));
+        ranges.push_back(std::move(std::make_pair(0, u().max_char())));
         auto exclude_range = [&](unsigned lower, unsigned upper) {
             SASSERT(lower <= upper);
             if (lower == 0) {

src/math/dd/dd_pdd.cpp

@@ -1985,7 +1985,7 @@ namespace dd {
                     continue;
                 }
                 while (!m.is_val(n)) {
-                    m_nodes.push_back(std::make_pair(true, n));
+                    m_nodes.push_back(std::move(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::make_pair(true, n));
+            m_nodes.push_back(std::move(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::make_pair(false, n));
+            m_nodes.push_back(std::move(std::make_pair(false, n)));
     }
 
     pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); }

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::make_pair(p.coeff(), p.var()));
+                tp.push_back(std::move(std::make_pair(p.coeff(), p.var())));
             }
             return print_linear_combination_customized(
                 tp, [](int j) -> std::string { return "x" + std::to_string(j); }, out);

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::make_pair(c, v));        
+                left_side.push_back(std::move(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::make_pair(mpq(1), j));
+        coeffs.push_back(std::move(std::make_pair(mpq(1), j)));
-        coeffs.push_back(std::make_pair(mpq(-1), k));
+        coeffs.push_back(std::move(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::make_pair(mpq(1), j));
+        coeffs.push_back(std::move(std::make_pair(mpq(1), j)));
-        coeffs.push_back(std::make_pair(mpq(-1), k));
+        coeffs.push_back(std::move(std::make_pair(mpq(-1), k)));
         unsigned ej = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var
             
 

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::make_pair(arity, unsigned_vector()));
+            it = m.insert(it, std::move(std::make_pair(arity, unsigned_vector())));
         }
         it->second.push_back(mon.var());
     }

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::make_pair(e->coeff(), j));
+    v.push_back(std::move(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::make_pair(rational(1), to_var(e)->var()));
+        v.push_back(std::move(std::make_pair(rational(1), to_var(e)->var())));
         break;
     default:
         SASSERT(!e->is_sum());

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::make_pair(j+1,0));
+                            positions2.push_back(std::move(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::make_pair(q->get_decl_name(sz-1-i), sub[i]));
+                        s.push_back(std::move(std::make_pair(q->get_decl_name(sz-1-i), sub[i])));
                     }
                     return;
                 }

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::make_pair(idx+1, 0));
+        positions.push_back(std::move(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::make_pair(idx+1, 0));
+        positions.push_back(std::move(std::make_pair(idx+1, 0)));
 
         TRACE(dl, 
               tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";

src/muz/bmc/dl_bmc_engine.cpp

@@ -319,7 +319,7 @@ namespace datalog {
                     }
                     proof* premises[2] = { pr, p };
 
-                    positions.push_back(std::make_pair(0, 1));
+                    positions.push_back(std::move(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::make_pair(j+1,0));
+                positions.push_back(std::move(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::make_pair(j+1,0));
+                        positions.push_back(std::move(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::make_pair(0, 1));
+                    positions.push_back(std::move(std::make_pair(0, 1)));
 
                     substs.push_back(sub1);
                     substs.push_back(sub);

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::make_pair(idx, true));
+                m_todo.push_back(std::move(std::make_pair(idx, true)));
             }
             for (unsigned idx : src.le) {
-                m_todo.push_back(std::make_pair(idx, strict));
+                m_todo.push_back(std::move(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::make_pair(find(j), true));
+        m_todo.push_back(std::move(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::make_pair(find(j), false));
+        m_todo.push_back(std::move(std::make_pair(find(j), false)));
         mk_lt(i);
     }
 

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::make_pair(i, sz));
+            sizes.push_back(std::move(std::make_pair(i, sz)));
         }
         std::sort(sizes.begin(), sizes.end(), compare_size_proc());        
 

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::make_pair(i,j));
+                        m_attach.push_back(std::move(std::make_pair(i,j)));
                     }
                     if (m2.supports_attachment(r[i])) {
-                        m_attach.push_back(std::make_pair(j,i));
+                        m_attach.push_back(std::move(std::make_pair(j,i)));
                     }
                 }
             }

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::make_pair(pred, fact));
+            m_table_facts.push_back(std::move(std::make_pair(pred, fact)));
         }
     }
 

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::make_pair(0,i));
+        positions.push_back(std::move(std::make_pair(0,i)));
     }
     for (unsigned i = 0; i <= premises.size(); ++i) {
         substs.push_back(expr_ref_vector(m));

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::make_pair(entry, 0));
+    m_muxes.insert(entry->m_variants.get(0), std::move(std::make_pair(entry, 0)));
-    m_muxes.insert(entry->m_variants.get(1), std::make_pair(entry, 1));
+    m_muxes.insert(entry->m_variants.get(1), std::move(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::make_pair(&entry, idx));
+        m_muxes.insert(entry.m_variants.back(), std::move(std::make_pair(&entry, idx)));
     }
 }
 

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::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
+                            coeff_lits.push_back(std::move(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::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
+                            coeff_lits.push_back(std::move(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::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
+                        coeff_lits.push_back(std::move(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::make_pair(abs(coefficient), to_app(negatedPremise)));
+                        coeff_lits.push_back(std::move(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::make_pair(matrix.get(k, l), ordered_basis[l]));
+                    coeff_lits.push_back(std::move(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::make_pair(rational(1), ordered_basis[j]));
+                            coeff_lits.push_back(std::move(std::make_pair(rational(1), ordered_basis[j])));
                         }
                     }
                     SASSERT(!coeff_lits.empty()); // since then previous outer loop would have found solution already

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::make_pair(idx+1, 0));
+            positions.push_back(std::move(std::make_pair(idx+1, 0)));
             pr = m.mk_hyper_resolve(2, premises.data(), fml, positions, substs);
             pc.insert(pr);
         }

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::make_pair(a1->get_arg(k), a2->get_arg(k)));
+                            todo.push_back(std::move(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::make_pair(arg, (*terms)[k]));
+                todo.push_back(std::move(std::make_pair(arg, (*terms)[k])));
                 match(i + 1, pat, j, todo, q, conjs);
                 todo.pop_back();
             }

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::make_pair(e, false));
+        m_delayed_eqs.push_back(std::move(std::make_pair(e, false)));
         ctx.push(push_back_vector<svector<std::pair<euf::th_eq, bool>>>(m_delayed_eqs));
     }
 

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::make_pair(r, vi));
+                m_left_side.push_back(std::move(std::make_pair(r, vi)));
                 m_columns[var].reset();
             }
         }

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::make_pair(t, rational::one()));
+            m_todo_terms.push_back(std::move(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::make_pair(wi, c1));
+                        m_todo_terms.push_back(std::move(std::make_pair(wi, c1)));
                     }
                     else {
                         m_nla->am().set(r1, c1.to_mpq());

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::make_pair(parent_root, sel));
+                    todo.push_back(std::move(std::make_pair(parent_root, sel)));
                 }
             }
         }

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::make_pair(kv.m_key, kv.m_value));
+            delay.push_back(std::move(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))

src/sat/smt/dt_solver.cpp

@@ -93,8 +93,8 @@ namespace dt {
     }
 
     void solver::oc_push_stack(enode* n) {
-        m_dfs.push_back(std::make_pair(EXIT, n));
+        m_dfs.push_back(std::move(std::make_pair(EXIT, n)));
-        m_dfs.push_back(std::make_pair(ENTER, n));
+        m_dfs.push_back(std::move(std::make_pair(ENTER, n)));
     }
 
     /**

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::make_pair(update::add_clause, 0));
+        m_trail.push_back(std::move(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::make_pair(update::add_clause, 0));
+        m_trail.push_back(std::move(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::make_pair(update::add_queue, lit.var()));
+        m_trail.push_back(std::move(std::make_pair(update::add_queue, lit.var())));
-        m_queue.push_back(std::make_pair(lit, nullptr));
+        m_queue.push_back(std::move(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::make_pair(update::relevant_var, lit.var()));
+        m_trail.push_back(std::move(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::make_pair(update::set_qhead, m_qhead));
+        m_trail.push_back(std::move(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::make_pair(update::add_queue, 0));
+        m_trail.push_back(std::move(std::make_pair(update::add_queue, 0)));
-        m_queue.push_back(std::make_pair(sat::null_literal, n));
+        m_queue.push_back(std::move(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::make_pair(update::set_root, idx));
+                m_trail.push_back(std::move(std::make_pair(update::set_root, idx)));
                 m_roots[idx] = true;
             }
         next:

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::make_pair(c.get_unsigned(), lits[i]));
+            wlits.push_back(std::move(std::make_pair(c.get_unsigned(), lits[i])));
         }
     }
 

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::make_pair(to_app(s), i));
+                        qb.var_args.push_back(std::move(std::make_pair(to_app(s), i)));
                     ++i;
                 }
             }

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::make_pair(e, expr_ref(e, m)));
+                asm2proxy.push_back(std::move(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::make_pair(e, proxy));
+                asm2proxy.push_back(std::move(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::make_pair(clausep, lits));
+        m_tmp_clauses.push_back(std::move(std::make_pair(clausep, lits)));
     }
 
     void context::reset_tmp_clauses() {

src/smt/theory_pb.cpp

@@ -531,7 +531,7 @@ namespace smt {
             case l_false:
                 break;
             default:
-                args.push_back(std::make_pair(l, c));
+                args.push_back(std::move(std::make_pair(l, c)));
                 break;
             }
         }

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::make_pair(ap->var(), ap->phase()));
+                atoms.push_back(std::move(std::make_pair(ap->var(), ap->phase())));
             }
         }
     }