diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp index 4f3951bc8..81c01d7fc 100644 --- a/src/muz/transforms/dl_mk_synchronize.cpp +++ b/src/muz/transforms/dl_mk_synchronize.cpp @@ -169,9 +169,9 @@ namespace datalog { dst_vector.push_back(new_rule.get()); } } - result.push_back(std::move(dst_vector)); + result.push_back(dst_vector); } - return std::move(result); + return result; } void mk_synchronize::add_rec_tail(vector< ptr_vector > & recursive_calls, diff --git a/src/opt/opt_preprocess.cpp b/src/opt/opt_preprocess.cpp index 5c03c640a..2e1b78070 100644 --- a/src/opt/opt_preprocess.cpp +++ b/src/opt/opt_preprocess.cpp @@ -146,7 +146,7 @@ namespace opt { for (expr* f : fmls) fmls[i++] = mk_not(m, f); - return std::move(new_soft); + return new_soft; } bool preprocess::find_mutexes(vector& softs, rational& lower) { diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 95f70d635..ba8f5faa3 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -333,7 +333,7 @@ namespace qe { (void)ok; CTRACE(qe, !ok, tout << "projection failure ignored!!!!\n"); fix_non_shared(*mdl, lits); - return std::move(defs); + return defs; } mbi_result uflia_mbi::operator()(expr_ref_vector& lits, model_ref& mdl) { diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 7724e6398..7f39cd5ed 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -78,7 +78,7 @@ namespace fpa { conds.push_back(mk_literal(t)); } m_converter.m_extra_assertions.reset(); - return std::move(conds); + return conds; } sat::check_result solver::check() { diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 5dcff8873..c7be4804c 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -695,7 +695,7 @@ namespace smt { for (enode* n : f) result.push_back(n); f.reset(); - return std::move(result); + return result; } void theory_datatype::relevant_eh(app * n) { diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 2a27f911f..c98a2b57a 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -351,7 +351,7 @@ ptr_vector solver_pool::get_base_solvers() const { solvers.push_back(s->base_solver()); } } - return std::move(solvers); + return solvers; } void solver_pool::updt_params(const params_ref &p) {