Add std::move for std::make_pair in 8 more files (insert and push_back)

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

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::make_pair(x, y));
+            positions.push_back(std::move(std::make_pair(x, y)));
             substs.push_back(expr_ref_vector(*this));
             ++i;
         }

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::make_pair(f, u.get_def(f).get_rhs()));
+        recfuns.push_back(std::move(std::make_pair(f, u.get_def(f).get_rhs())));
     }
     if (!recfuns.empty())
         ast_smt2_pp_recdefs(out, recfuns, m_env);

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::make_pair(m, q));
+                    full_macros.insert(f, std::move(std::make_pair(m, q)));
                     cond_macros.erase(f);
                 }
                 else if (!full_macros.contains(f) && !qi->is_auf())

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::make_pair(c, def));            
+            m_defs.push_back(std::move(std::make_pair(c, def)));            
         }
     }
 

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::make_pair(pos, r));
+            cache.insert(e, std::move(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::make_pair(pos, r));
+            cache.insert(e, std::move(std::make_pair(pos, r)));
         }
 
         TRACE(expr_context_simplifier, 

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::make_pair(rhs, ls[0]));
+        m_nth_eq2_cache.insert(std::move(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)); 

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::make_pair(v1, v2));
+                m_diseq_watch[watch_var].push_back(std::move(std::make_pair(v1, v2)));
                 m_diseq_watch_trail.push_back(watch_var);
                 return;
             }

src/smt/theory_datatype.cpp

@@ -71,8 +71,8 @@ namespace smt {
     }
 
     void theory_datatype::oc_push_stack(enode * n) {
-        m_stack.push_back(std::make_pair(EXIT, n));
-        m_stack.push_back(std::make_pair(ENTER, n));
+        m_stack.push_back(std::move(std::make_pair(EXIT, n)));
+        m_stack.push_back(std::move(std::make_pair(ENTER, n)));
     }