diff --git a/src/ast/ast.h b/src/ast/ast.h
index 0410a4edd..611c07eec 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -130,7 +130,7 @@ public:
     explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
     parameter(parameter const&);
 
-    parameter(parameter && other) : m_kind(other.m_kind) {
+    parameter(parameter && other) noexcept : m_kind(other.m_kind) {
         switch (other.m_kind) {
         case PARAM_INT: m_int = other.get_int(); break;
         case PARAM_AST: m_ast = other.get_ast(); break;
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index b8fc04b0a..cceb34b0b 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/src/math/grobner/pdd_solver.h
@@ -25,6 +25,7 @@
 #include "util/rlimit.h"
 #include "util/statistics.h"
 #include "math/dd/dd_pdd.h"
+#include <cstring>
 
 namespace dd {
 
diff --git a/src/math/hilbert/hilbert_basis.h b/src/math/hilbert/hilbert_basis.h
index cb4dd146e..46563195c 100644
--- a/src/math/hilbert/hilbert_basis.h
+++ b/src/math/hilbert/hilbert_basis.h
@@ -25,14 +25,14 @@ Revision History:
 
 --*/
 
-#ifndef HILBERT_BASIS_H_
-#define HILBERT_BASIS_H_
+#pragma once
 
 #include "util/rational.h"
 #include "util/lbool.h"
 #include "util/statistics.h"
 #include "util/checked_int64.h"
 #include "util/rlimit.h"
+#include <cstring>
 
 typedef vector<rational> rational_vector;
 
@@ -198,6 +198,3 @@ public:
     void reset_statistics();     
 
 };
-
-
-#endif 
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index a7d7e9b86..0cd0305fc 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -24,6 +24,7 @@ Revision History:
 #include <algorithm>
 #include <limits>
 #include <iomanip>
+#include <cstring>
 #include "math/lp/lp_utils.h"
 #include "util/stopwatch.h"
 #include "math/lp/lp_types.h"
diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h
index 96b2dd03c..f18bb6f87 100644
--- a/src/math/simplex/sparse_matrix.h
+++ b/src/math/simplex/sparse_matrix.h
@@ -16,11 +16,11 @@ Notes:
 
 --*/
 
-#ifndef SPARSE_MATRIX_H_
-#define SPARSE_MATRIX_H_
+#pragma once
 
 #include "util/mpq_inf.h"
 #include "util/statistics.h"
+#include <cstring>
 
 namespace simplex {
 
@@ -271,6 +271,3 @@ namespace simplex {
     };
 
 };
-
-
-#endif
diff --git a/src/math/subpaving/subpaving_types.h b/src/math/subpaving/subpaving_types.h
index e81b86e09..28150cc04 100644
--- a/src/math/subpaving/subpaving_types.h
+++ b/src/math/subpaving/subpaving_types.h
@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef SUBPAVING_TYPES_H_
-#define SUBPAVING_TYPES_H_
+#pragma once
 
 namespace subpaving {
 
@@ -34,7 +33,6 @@ class power : public std::pair<var, unsigned> {
 public:
     power():std::pair<var, unsigned>() {}
     power(var v, unsigned d):std::pair<var, unsigned>(v, d) {}
-    power(power const & p):std::pair<var, unsigned>(p) {}
     var x() const { return first; }
     var get_var() const { return first; }
     unsigned degree() const { return second; }
@@ -47,6 +45,4 @@ struct display_var_proc {
     virtual void operator()(std::ostream & out, var x) const { out << "x" << x; }
 };
 
-};
-
-#endif
+}
diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp
index c0e52c17b..a5ea1a14c 100644
--- a/src/smt/old_interval.cpp
+++ b/src/smt/old_interval.cpp
@@ -228,6 +228,7 @@ interval::interval(v_dependency_manager & m, rational const & val, bool open, bo
 }
 
 interval & interval::operator=(interval const & other) {
+    SASSERT(&m == &other.m);
     m_lower = other.m_lower;
     m_upper = other.m_upper;
     m_lower_open = other.m_lower_open;
@@ -237,6 +238,17 @@ interval & interval::operator=(interval const & other) {
     return *this;
 }
 
+interval & interval::operator=(interval && other) {
+    SASSERT(&m == &other.m);
+    m_lower = std::move(other.m_lower);
+    m_upper = std::move(other.m_upper);
+    m_lower_open = other.m_lower_open;
+    m_upper_open = other.m_upper_open;
+    m_lower_dep  = other.m_lower_dep;
+    m_upper_dep  = other.m_upper_dep;
+    return *this;
+}
+
 interval & interval::operator+=(interval const & other) {
     m_lower      += other.m_lower;
     m_upper      += other.m_upper;
diff --git a/src/smt/old_interval.h b/src/smt/old_interval.h
index 8919d9ca0..7a6f41e26 100644
--- a/src/smt/old_interval.h
+++ b/src/smt/old_interval.h
@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef OLD_INTERVAL_H_
-#define OLD_INTERVAL_H_
+#pragma once
 
 #include "util/rational.h"
 #include "util/dependency.h"
@@ -81,6 +80,8 @@ public:
     explicit old_interval(v_dependency_manager & m, rational const & val, v_dependency * l_dep = nullptr, v_dependency * u_dep = nullptr);
     explicit old_interval(v_dependency_manager & m, rational const & val, bool open, bool lower, v_dependency * d);
     explicit old_interval(v_dependency_manager & m, ext_numeral const& lower, bool l_open, v_dependency * l_dep, ext_numeral const & upper, bool u_open, v_dependency * u_dep);
+    old_interval(const old_interval&) = default;
+    old_interval(old_interval&&) = default;
 
     bool minus_infinity() const { return m_lower.is_infinite(); }
     bool plus_infinity() const { return m_upper.is_infinite(); }
@@ -91,6 +92,7 @@ public:
     rational const & get_lower_value() const { SASSERT(!minus_infinity()); return m_lower.to_rational(); }
     rational const & get_upper_value() const { SASSERT(!plus_infinity()); return m_upper.to_rational(); }
     old_interval & operator=(old_interval const & other);
+    old_interval & operator=(old_interval && other);
     old_interval & operator+=(old_interval const & other);
     old_interval & operator-=(old_interval const & other);
     old_interval & operator*=(old_interval const & other);
@@ -125,12 +127,5 @@ inline old_interval operator/(old_interval const & i1, old_interval const & i2)
 inline old_interval expt(old_interval const & i, unsigned n) { old_interval tmp(i); tmp.expt(n); return tmp; }
 inline std::ostream & operator<<(std::ostream & out, old_interval const & i) { i.display(out); return out; }
 
-struct interval_detail{};
-inline std::pair<old_interval, interval_detail> wd(old_interval const & i) { interval_detail d; return std::make_pair(i, d); }
-inline std::ostream & operator<<(std::ostream & out, std::pair<old_interval, interval_detail> const & p) { p.first.display_with_dependencies(out); return out; }
-
 // allow "customers" of this file to keep using interval
 #define interval old_interval
-
-#endif /* OLD_INTERVAL_H_ */
-
diff --git a/src/util/buffer.h b/src/util/buffer.h
index 57150a124..a261788ee 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -21,7 +21,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<string.h>
+#include <type_traits>
 #include "util/memory_manager.h"
 
 template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
@@ -39,6 +39,7 @@ protected:
     }
 
     void expand() {
+        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/checked_int64.h b/src/util/checked_int64.h
index 507564a2e..06b957fcf 100644
--- a/src/util/checked_int64.h
+++ b/src/util/checked_int64.h
@@ -21,8 +21,7 @@ Revision History:
 
 --*/
 
-#ifndef CHECKED_INT64_H_
-#define CHECKED_INT64_H_
+#pragma once
 
 #include "util/z3_exception.h"
 #include "util/rational.h"
@@ -38,7 +37,6 @@ public:
 
     checked_int64(): m_value(0) {}
     checked_int64(int64_t v): m_value(v) {}
-    checked_int64(checked_int64 const& other) { m_value = other.m_value; }
 
     class overflow_exception : public z3_exception {
         char const * msg() const override { return "checked_int64 overflow/underflow";}
@@ -217,5 +215,3 @@ inline checked_int64<CHECK> operator*(checked_int64<CHECK> const& a, checked_int
     result *= b;
     return result;
 }
-
-#endif
diff --git a/src/util/hwf.h b/src/util/hwf.h
index 21e7655ea..3230cdb7e 100644
--- a/src/util/hwf.h
+++ b/src/util/hwf.h
@@ -16,10 +16,10 @@ Author:
 Revision History:
 
 --*/
-#ifndef HWF_H_
-#define HWF_H_
+#pragma once
 
-#include<string>
+#include <cstring>
+#include <string>
 #include "util/mpz.h"
 #include "util/mpq.h"
 #include "util/mpf.h"
@@ -172,5 +172,3 @@ protected:
 
 typedef _scoped_numeral<hwf_manager> scoped_hwf;
 typedef _scoped_numeral_vector<hwf_manager> scoped_hwf_vector;
-
-#endif
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index cdd8f5f3e..1e93d0d3d 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -16,6 +16,7 @@ Author:
 Revision History:
 
 --*/
+#include <cstring>
 #include<sstream>
 #include<iomanip>
 #include "util/mpf.h"
diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp
index 4769ab24a..8595e0185 100644
--- a/src/util/mpfx.cpp
+++ b/src/util/mpfx.cpp
@@ -16,6 +16,7 @@ Author:
 Revision History:
 
 --*/
+#include <cstring>
 #include<sstream>
 #include<iomanip>
 #include "util/mpfx.h"
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index eb6754654..3a7922e13 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -16,6 +16,7 @@ Author:
 Revision History:
 
 --*/
+#include <cstring>
 #include <sstream>
 #include <iomanip>
 #include "util/mpz.h"
diff --git a/src/util/mpz.h b/src/util/mpz.h
index dee54b1c8..266b9aa34 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef MPZ_H_
-#define MPZ_H_
+#pragma once
 
 #include<string>
 #include "util/mutex.h"
@@ -104,7 +103,7 @@ public:
     mpz(int v):m_val(v), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {}
     mpz():m_val(0), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {}
     mpz(mpz_type* ptr): m_val(0), m_kind(mpz_small), m_owner(mpz_ext), m_ptr(ptr) { SASSERT(ptr);}
-    mpz(mpz && other) : m_val(other.m_val), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {
+    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;
@@ -734,6 +733,3 @@ typedef mpz_manager<false> unsynch_mpz_manager;
 typedef _scoped_numeral<unsynch_mpz_manager> scoped_mpz;
 typedef _scoped_numeral<synch_mpz_manager> scoped_synch_mpz;
 typedef _scoped_numeral_vector<unsynch_mpz_manager> scoped_mpz_vector;
-
-#endif /* MPZ_H_ */
-
diff --git a/src/util/rational.h b/src/util/rational.h
index c7f0358dd..eec5c50ec 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef RATIONAL_H_
-#define RATIONAL_H_
+#pragma once
 
 #include "util/mpq.h"
 
@@ -41,7 +40,7 @@ public:
     rational() {}
     
     rational(rational const & r) { m().set(m_val, r.m_val); }
-    rational(rational && r) : m_val(std::move(r.m_val)) {}
+    rational(rational && r) noexcept : m_val(std::move(r.m_val)) {}
 
     explicit rational(int n) { m().set(m_val, n); }
 
@@ -576,7 +575,3 @@ inline rational gcd(rational const & r1, rational const & r2, rational & a, rati
   rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val);
   return result;
 }
-
-
-#endif /* RATIONAL_H_ */
-