diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp
index 81c01d7fc..4f3951bc8 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(dst_vector);
+            result.push_back(std::move(dst_vector));
         }
-        return result;
+        return std::move(result);
     }
 
     void mk_synchronize::add_rec_tail(vector< ptr_vector<app> > & recursive_calls,
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index ba8f5faa3..95f70d635 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 defs;
+        return std::move(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 7f39cd5ed..7724e6398 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 conds;
+        return std::move(conds);
     }
 
     sat::check_result solver::check() {
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index c7be4804c..5dcff8873 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 result;
+        return std::move(result);
     }
 
     void theory_datatype::relevant_eh(app * n) {
diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp
index c98a2b57a..2a27f911f 100644
--- a/src/solver/solver_pool.cpp
+++ b/src/solver/solver_pool.cpp
@@ -351,7 +351,7 @@ ptr_vector<solver> solver_pool::get_base_solvers() const {
             solvers.push_back(s->base_solver());
         }
     }
-    return solvers;
+    return std::move(solvers);
 }
 
 void solver_pool::updt_params(const params_ref &p) {