diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index c1a1a3d94..95d06f3a2 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -324,20 +324,20 @@ struct pb2bv_rewriter::imp {
                 unsigned c = m_coeffs[i].get_unsigned();
                 v.push_back(c >= k ? k : c);
                 e.push_back(args[i]);   
-                es.push_back(e);
-                coeffs.push_back(v);
+                es.push_back(std::move(e));
+                coeffs.push_back(std::move(v));
             }
             while (es.size() > 1) {
                 for (unsigned i = 0; i + 1 < es.size(); i += 2) {
                     expr_ref_vector o(m);
                     unsigned_vector oc;
                     tot_adder(es[i], coeffs[i], es[i + 1], coeffs[i + 1], k, o, oc);
-                    es[i / 2].set(o);
-                    coeffs[i / 2] = oc;
+                    es[i / 2] = std::move(o);
+                    coeffs[i / 2] = std::move(oc);
                 }
                 if ((es.size() % 2) == 1) {
-                    es[es.size() / 2].set(es.back());
-                    coeffs[es.size() / 2] = coeffs.back();
+                    es[es.size() / 2] = std::move(es.back());
+                    coeffs[es.size() / 2] = std::move(coeffs.back());
                 }
                 es.shrink((1 + es.size())/2);
                 coeffs.shrink((1 + coeffs.size())/2);
diff --git a/src/ast/substitution/expr_offset.h b/src/ast/substitution/expr_offset.h
index d52182117..7a9e08899 100644
--- a/src/ast/substitution/expr_offset.h
+++ b/src/ast/substitution/expr_offset.h
@@ -31,6 +31,11 @@ class expr_offset {
 public:
     expr_offset() = default;
     expr_offset(expr * e, unsigned o):m_expr(e), m_offset(o) {}
+    expr_offset(const expr_offset&) = default;
+    expr_offset(expr_offset&&) noexcept = default;
+
+    expr_offset& operator=(expr_offset const & other) = default;
+    expr_offset& operator=(expr_offset&&) noexcept = default;
     
     expr * get_expr() const { return m_expr; }
     unsigned get_offset() const { return m_offset; }
diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index 111b255f8..f4cfa1fbd 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -2129,8 +2129,7 @@ namespace polynomial {
                 for (unsigned i = 0; i < sz; ++i) {
                     monomial * m = m_tmp_ms[i];
                     unsigned pos = m_m2pos.get(m);
-                    new_as.push_back(numeral());
-                    swap(new_as.back(), m_tmp_as[pos]);
+                    new_as.push_back(std::move(m_tmp_as[pos]));
                     m_m2pos.reset(m);
                     m_m2pos.set(m, i);
                 }
diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp
index 60ff87537..7e68f33fb 100644
--- a/src/qe/nlarith_util.cpp
+++ b/src/qe/nlarith_util.cpp
@@ -1953,8 +1953,8 @@ namespace nlarith {
             for (; i + 1 < mat.size(); i += 2) {
                 if (mat[i+1].contains(Zero)) {
                     if (i != j) {
-                        mat[j] = mat[i];
-                        mat[j+1] = mat[i+1];
+                        mat[j] = std::move(mat[i]);
+                        mat[j+1] = std::move(mat[i+1]);
                     }
                     j += 2;
                 }
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 6cc6a33c2..263dad43c 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -385,7 +385,6 @@ namespace qe {
             // They are sorted by size, so we project the largest variables first to avoid 
             // renaming variables. 
             for (unsigned i = vars.size(); i-- > 0;) {
-                new_result.reset();
                 ex.project(vars[i], result.size(), result.data(), new_result);
                 TRACE(qe, display_project(tout, vars[i], result, new_result););
                 result = std::move(new_result);
diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp
index c6ca56405..8e4751ff7 100644
--- a/src/sat/sat_mus.cpp
+++ b/src/sat/sat_mus.cpp
@@ -208,7 +208,7 @@ namespace sat {
                 lits2.insert(*it);
             }
         }
-        lits1 = lits3;
+        lits1 = std::move(lits3);
     }
 
     literal_vector& mus::get_core() {
diff --git a/src/sat/sat_xor_finder.cpp b/src/sat/sat_xor_finder.cpp
index 532e16fa3..372aade4c 100644
--- a/src/sat/sat_xor_finder.cpp
+++ b/src/sat/sat_xor_finder.cpp
@@ -210,7 +210,7 @@ namespace sat {
                 }
                 bv.push_back(parity);
             }
-            m_parity.push_back(bv);
+            m_parity.push_back(std::move(bv));
         }
     }
 
diff --git a/src/util/vector.h b/src/util/vector.h
index b0c1a0b6b..74783308e 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -650,6 +650,17 @@ public:
     svector(SZ s):vector<T, false, SZ>(s) {}
     svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
     svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
+    svector(const svector&) = default;
+    svector(svector&&) noexcept = default;
+
+    svector & operator=(const svector & source) {
+        vector<T, false, SZ>::operator=(source);
+        return *this;
+    }
+    svector & operator=(svector && source) noexcept {
+        vector<T, false, SZ>::operator=(std::move(source));
+        return *this;
+    }
 };