From 6bad27a56bb3343bb2582cfbc3d3fc191e13f28a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 11 Feb 2026 21:41:34 +0000 Subject: [PATCH] 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 | 2 +- src/ast/ast_pp_util.cpp | 2 +- src/model/model_macro_solver.cpp | 2 +- src/opt/totalizer.cpp | 2 +- src/smt/expr_context_simplifier.cpp | 4 ++-- src/smt/seq_eq_solver.cpp | 2 +- src/smt/theory_bv.cpp | 2 +- src/smt/theory_datatype.cpp | 4 ++-- 8 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 4aeda7a5c..341e26c36 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(params[i].get_int()); unsigned y = static_cast(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; } diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index 2b7e72a91..5553a6e9b 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::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); diff --git a/src/model/model_macro_solver.cpp b/src/model/model_macro_solver.cpp index 64881482e..992e55180 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 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()) diff --git a/src/opt/totalizer.cpp b/src/opt/totalizer.cpp index 41d730560..33995ce28 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::make_pair(c, def)); + m_defs.push_back(std::move(std::make_pair(c, def))); } } diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp index 852da2f11..5451eee14 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::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, diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index e368e137b..9a4505b4a 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::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)); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 14cfc943f..c79e85a9e 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::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; } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index c7be4804c..aa5169df2 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::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))); }