diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h
index d9a6fc629..2e49051e3 100644
--- a/src/ast/justified_expr.h
+++ b/src/ast/justified_expr.h
@@ -1,6 +1,5 @@
 
-#ifndef JUSTIFIED_EXPR_H_
-#define JUSTIFIED_EXPR_H_
+#pragma once
 
 #include "ast/ast.h"
 
@@ -40,6 +39,15 @@ public:
         m.inc_ref(m_proof);
     }
 
+    justified_expr(justified_expr && other):
+        m(other.m),
+        m_fml(nullptr),
+        m_proof(nullptr)
+    {
+        std::swap(m_fml, other.m_fml);
+        std::swap(m_proof, other.m_proof);
+    }
+
     ~justified_expr() {
         m.dec_ref(m_fml);
         m.dec_ref(m_proof);
@@ -50,5 +58,3 @@ public:
     expr* get_fml() const { return m_fml; }
     proof* get_proof() const { return m_proof; }        
 };
-
-#endif
diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index db9f5eb66..7bf9de2e0 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/src/ast/normal_forms/nnf.cpp
@@ -221,16 +221,6 @@ struct nnf::imp {
             m_cache_result(cache_res),
             m_spos(spos) {
         }
-        frame(frame && other):
-            m_curr(std::move(other.m_curr)),
-            m_i(other.m_i),
-            m_pol(other.m_pol),
-            m_in_q(other.m_in_q),
-            m_new_child(other.m_new_child),
-            m_cache_result(other.m_cache_result),
-            m_spos(other.m_spos) {            
-        }
-            
     };
 
     // There are four caches:
diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h
index 4903b2067..3d42f13a0 100644
--- a/src/math/automata/automaton.h
+++ b/src/math/automata/automaton.h
@@ -54,6 +54,10 @@ public:
             if (m_t) m.inc_ref(m_t);
         }
 
+        move(move &&other) noexcept : m(other.m), m_t(nullptr), m_src(other.m_src), m_dst(other.m_dst) {
+            std::swap(m_t, other.m_t);
+        }
+
         move& operator=(move const& other) {
             SASSERT(&m == &other.m);
             T* t = other.m_t;
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 0abb38eae..062b6904d 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -208,7 +208,7 @@ namespace sat {
     }
 
     void model_converter::add_elim_stack(entry & e) {
-        e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, stackv()));
+        e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, std::move(m_elim_stack)));
         // VERIFY(for (auto const& s : stackv()) VERIFY(legal_to_flip(s.second.var())););
         stackv().reset();
     }
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index 93a078818..e453bcaa1 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef SAT_MODEL_CONVERTER_H_
-#define SAT_MODEL_CONVERTER_H_
+#pragma once
 
 #include "sat/sat_types.h"
 #include "util/ref_vector.h"
@@ -51,12 +50,12 @@ namespace sat {
             unsigned        m_counter;
             unsigned        m_refcount;
             elim_stackv     m_stack;
-            elim_stack(elim_stack const& );
         public:
-            elim_stack(elim_stackv const& stack): 
+            elim_stack(elim_stack const&) = delete;
+            elim_stack(elim_stackv && stack):
                 m_counter(0),
                 m_refcount(0), 
-                m_stack(stack) {
+                m_stack(std::move(stack)) {
                 m_counter = ++counter;
             }
             ~elim_stack() { }
@@ -76,14 +75,6 @@ namespace sat {
             sref_vector<elim_stack> m_elim_stack;
             entry(kind k, bool_var v): m_var(v), m_kind(k) {}
         public:
-            entry(entry const & src):
-                m_var(src.m_var),
-                m_kind(src.m_kind),
-                m_clauses(src.m_clauses),
-                m_clause(src.m_clause)
-            {
-                m_elim_stack.append(src.m_elim_stack);
-            }
             bool_var var() const { return m_var; }
             kind get_kind() const { return m_kind; }
         };
@@ -166,5 +157,3 @@ namespace sat {
     }
 
 };
-
-#endif
diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp
index a5ea1a14c..efdb78754 100644
--- a/src/smt/old_interval.cpp
+++ b/src/smt/old_interval.cpp
@@ -228,7 +228,7 @@ interval::interval(v_dependency_manager & m, rational const & val, bool open, bo
 }
 
 interval & interval::operator=(interval const & other) {
-    SASSERT(&m == &other.m);
+    SASSERT(&m_manager == &other.m_manager);
     m_lower = other.m_lower;
     m_upper = other.m_upper;
     m_lower_open = other.m_lower_open;
@@ -239,7 +239,7 @@ interval & interval::operator=(interval const & other) {
 }
 
 interval & interval::operator=(interval && other) {
-    SASSERT(&m == &other.m);
+    SASSERT(&m_manager == &other.m_manager);
     m_lower = std::move(other.m_lower);
     m_upper = std::move(other.m_upper);
     m_lower_open = other.m_lower_open;
diff --git a/src/util/buffer.h b/src/util/buffer.h
index a261788ee..22cf17ada 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -39,7 +39,7 @@ protected:
     }
 
     void expand() {
-        static_assert(std::is_nothrow_move_constructible<T>::value);
+        static_assert(std::is_nothrow_move_constructible<T>::value, "");
         unsigned new_capacity = m_capacity << 1;
         T * new_buffer        = reinterpret_cast<T*>(memory::allocate(sizeof(T) * new_capacity));
         for (unsigned i = 0; i < m_pos; ++i) {
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index 55866065e..78abd3c87 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#ifndef HASHTABLE_H_
-#define HASHTABLE_H_
+#pragma once
+
 #include "util/debug.h"
 #include <ostream>
 #include "util/util.h"
@@ -269,6 +269,19 @@ public:
             m_st_collision = 0;
         });
     }
+
+    core_hashtable(core_hashtable && source) noexcept :
+        HashProc(source),
+        EqProc(source),
+        m_table(nullptr) {
+        m_capacity    = source.m_capacity;
+        std::swap(m_table, source.m_table);
+        m_size        = source.m_size;
+        m_num_deleted = 0;
+        HS_CODE({
+            m_st_collision = 0;
+        });
+    }
     
     ~core_hashtable() {
         delete_table();
@@ -736,6 +749,3 @@ public:
                   EqProc const & e = EqProc()):
         core_hashtable<int_hash_entry<INT_MIN, INT_MIN + 1>, HashProc, EqProc>(initial_capacity, h, e) {}
 };
-
-
-#endif /* HASHTABLE_H_ */
diff --git a/src/util/hwf.h b/src/util/hwf.h
index 3230cdb7e..f2afbee63 100644
--- a/src/util/hwf.h
+++ b/src/util/hwf.h
@@ -36,9 +36,6 @@ class hwf {
     }
 
 public:    
-    hwf() {}
-    hwf(hwf const & other) { this->value = other.value; }
-    ~hwf() {}   
     void swap(hwf & other) { double t = value; value = other.value; other.value = t; }
 };
 
diff --git a/src/util/mpf.h b/src/util/mpf.h
index 107ada0bd..fb5f2a022 100644
--- a/src/util/mpf.h
+++ b/src/util/mpf.h
@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef MPF_H_
-#define MPF_H_
+#pragma once
 
 #include<string>
 #include "util/mpz.h"
@@ -45,18 +44,13 @@ class mpf {
     unsigned sign:1; // counts as one sbit.
     mpz significand;
     mpf_exp_t exponent;
-    mpf & operator=(mpf const & other) { UNREACHABLE(); return *this; }
     void set(unsigned _ebits, unsigned _sbits);
 public:
     mpf();
     mpf(unsigned ebits, unsigned sbits);
-    mpf(mpf && other) :
-        ebits(other.ebits),
-        sbits(other.sbits),
-        sign(other.sign),
-        significand(std::move(other.significand)),
-        exponent(other.exponent) {}
+    mpf(mpf &&) = default;
     ~mpf();
+    mpf & operator=(mpf const & other) = delete;
     unsigned get_ebits() const { return ebits; }
     unsigned get_sbits() const { return sbits; }
     void swap(mpf & other);
@@ -325,5 +319,3 @@ public:
 };
 
 typedef _scoped_numeral_vector<mpf_manager> scoped_mpf_vector;
-
-#endif
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 4cc15229f..a9e6063a3 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef MPQ_H_
-#define MPQ_H_
+#pragma once
 
 #include "util/mpz.h"
 #include "util/trace.h"
@@ -27,11 +26,11 @@ class mpq {
     mpz m_den;
     friend class mpq_manager<true>;
     friend class mpq_manager<false>;
-    mpq & operator=(mpq const & other) { UNREACHABLE(); return *this; }
 public:
     mpq(int v):m_num(v), m_den(1) {}
     mpq():m_den(1) {}
-    mpq(mpq && other) : m_num(std::move(other.m_num)), m_den(std::move(other.m_den)) {}
+    mpq(mpq &&) = default;
+    mpq & operator=(mpq const &) = delete;
     void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); }
     mpz const & numerator() const { return m_num; }
     mpz const & denominator() const { return m_den; }
@@ -862,6 +861,3 @@ typedef mpq_manager<false> unsynch_mpq_manager;
 typedef _scoped_numeral<unsynch_mpq_manager> scoped_mpq;
 typedef _scoped_numeral<synch_mpq_manager> scoped_synch_mpq;
 typedef _scoped_numeral_vector<unsynch_mpq_manager> scoped_mpq_vector;
-
-#endif /* MPQ_H_ */
-
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 266b9aa34..248048888 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -105,8 +105,8 @@ public:
     mpz(mpz_type* ptr): m_val(0), m_kind(mpz_small), m_owner(mpz_ext), m_ptr(ptr) { SASSERT(ptr);}
     mpz(mpz && other) noexcept : m_val(other.m_val), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {
         std::swap(m_ptr, other.m_ptr);
-        unsigned o = m_owner; m_owner = other.m_owner; other.m_owner = o;
-        unsigned k = m_kind; m_kind = other.m_kind; other.m_kind = k;
+        m_owner = other.m_owner;
+        m_kind = other.m_kind;
     }
     void swap(mpz & other) { 
         std::swap(m_val, other.m_val);
diff --git a/src/util/optional.h b/src/util/optional.h
index d496fd322..b9687df8c 100644
--- a/src/util/optional.h
+++ b/src/util/optional.h
@@ -18,8 +18,7 @@ Revision History:
 
 --*/
 
-#ifndef OPTIONAL_H_
-#define OPTIONAL_H_
+#pragma once
 
 template<class T>
 class optional {
@@ -47,6 +46,11 @@ public:
         construct(val);
     }
 
+    optional(T && val) noexcept : m_obj(nullptr), m_initialized(0) {
+        std::swap(m_obj, val.m_obj);
+        std::swap(m_initialized, val.m_initialized);
+    }
+
     optional(const optional<T> & val):
         m_initialized(0) {
         if (val.m_initialized == 1) {
@@ -160,7 +164,3 @@ public:
     
     T * & operator*() { return m_ptr; }
 };
-
-
-#endif /* OPTIONAL_H_ */
-
diff --git a/src/util/rational.h b/src/util/rational.h
index eec5c50ec..0f2a2a1b7 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -40,7 +40,7 @@ public:
     rational() {}
     
     rational(rational const & r) { m().set(m_val, r.m_val); }
-    rational(rational && r) noexcept : m_val(std::move(r.m_val)) {}
+    rational(rational&&) = default;
 
     explicit rational(int n) { m().set(m_val, n); }
 
diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index 5b5d9ac34..ce8060cd3 100644
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef REF_VECTOR_H_
-#define REF_VECTOR_H_
+#pragma once
 
 #include "util/vector.h"
 #include "util/obj_ref.h"
@@ -49,11 +48,14 @@ protected:
 public:
     typedef T * data;
 
-    ref_vector_core(Ref const & r = Ref()):Ref(r) {}
+    ref_vector_core() = default;
+    ref_vector_core(Ref const & r) : Ref(r) {}
 
-    ref_vector_core(ref_vector_core && other) :
-        Ref(std::move(other)),
-        m_nodes(std::move(other.m_nodes)) {}
+    ref_vector_core(const ref_vector_core & other) {
+        append(other);
+    }
+
+    ref_vector_core(ref_vector_core &&) = default;
     
     ~ref_vector_core() {
         dec_range_ref(m_nodes.begin(), m_nodes.end());
@@ -400,9 +402,8 @@ public:
 /**
    \brief Vector of unmanaged references.
 */
-template<typename T> 
-class sref_vector : public ref_vector_core<T, ref_unmanaged_wrapper<T> > {
-};
+template<typename T>
+using sref_vector = ref_vector_core<T, ref_unmanaged_wrapper<T>>;
 
 /**
    \brief Hash utilities on ref_vector pointers.
@@ -440,6 +441,3 @@ struct ref_vector_ptr_eq {
         return true;
     }
 };
-
-
-#endif /* REF_VECTOR_H_ */
diff --git a/src/util/vector.h b/src/util/vector.h
index 9de2b2a86..588be7ae8 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -69,6 +69,7 @@ class vector {
             m_data            = reinterpret_cast<T *>(mem);
         }
         else {
+            //static_assert(std::is_nothrow_move_constructible<T>::value, "");
             SASSERT(capacity() > 0);
             SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
             SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
@@ -163,7 +164,7 @@ public:
         SASSERT(size() == source.size());
     }
 
-    vector(vector&& other) : m_data(nullptr) {
+    vector(vector&& other) noexcept : m_data(nullptr) {
         std::swap(m_data, other.m_data);
     }
 
@@ -587,7 +588,7 @@ public:
     ptr_vector(unsigned s):vector<T *, false>(s) {}
     ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
     ptr_vector(ptr_vector const & source):vector<T *, false>(source) {}
-    ptr_vector(ptr_vector && other) : vector<T*, false>(std::move(other)) {}
+    ptr_vector(ptr_vector && other) noexcept : vector<T*, false>(std::move(other)) {}
     ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
     ptr_vector & operator=(ptr_vector const & source) {
         vector<T *, false>::operator=(source);
@@ -602,7 +603,7 @@ public:
     svector(SZ s):vector<T, false, SZ>(s) {}
     svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
     svector(svector const & source):vector<T, false, SZ>(source) {}
-    svector(svector && other) : vector<T, false, SZ>(std::move(other)) {}
+    svector(svector && other) noexcept : vector<T, false, SZ>(std::move(other)) {}
     svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
     svector & operator=(svector const & source) {
         vector<T, false, SZ>::operator=(source);