diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake
index ebabc71dba..3b9ae912ef 100644
--- a/cmake/compiler_warnings.cmake
+++ b/cmake/compiler_warnings.cmake
@@ -28,6 +28,8 @@ set(CLANG_ONLY_WARNINGS
   "-Wimplicit-fallthrough"
   "-Wextra-semi"
   "-Wignored-qualifiers"
+  "-Wnoctad-maybe-unsupported"
+  "-Wdeprecated-copy-with-user-provided-copy"
 )
 
 set(MSVC_WARNINGS "/W3")
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index bfe400c57e..8566173f2b 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -458,6 +458,7 @@ public:
               Default constructor of invalid info.
             */
             info() = default;
+            info(const info&) = default;
 
             /*
               Used for constructing either an invalid info that is only used to indicate uninitialized entry, or valid but unknown info value.
diff --git a/src/math/lp/dense_matrix.h b/src/math/lp/dense_matrix.h
index 2d9d6c2358..40bba66f97 100644
--- a/src/math/lp/dense_matrix.h
+++ b/src/math/lp/dense_matrix.h
@@ -45,6 +45,7 @@ public:
     unsigned m_n; // number of const
     vector<T> m_values;
     dense_matrix(unsigned m, unsigned n);
+    dense_matrix(const dense_matrix &) = default;
 
     dense_matrix operator*=(matrix<T, X> const & a) {
         SASSERT(column_count() == a.row_count());
diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h
index 3a6081f409..abc96df676 100644
--- a/src/math/subpaving/subpaving_t.h
+++ b/src/math/subpaving/subpaving_t.h
@@ -120,7 +120,9 @@ public:
         justification(justification const & source) { m_data = source.m_data; }
         explicit justification(clause * c) { m_data = TAG(void*, c, CLAUSE); }
         explicit justification(var x) { m_data = BOXTAGINT(void*, x, VAR_DEF);  }
-        
+
+        justification &operator=(justification const &) = default;
+
         kind get_kind() const { return static_cast<kind>(GET_TAG(m_data)); }
         bool is_clause() const { return get_kind() == CLAUSE; }
         bool is_axiom() const { return get_kind() == AXIOM; }
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index a0b7d05382..fe72073410 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -32,6 +32,7 @@ class aig_lit {
 public:
     aig_lit(aig * n = nullptr):m_ref(n) {}
     aig_lit(aig_ref const & r):m_ref(static_cast<aig*>(r.m_ref)) {}
+    aig_lit(const aig_lit &) = default;
     bool is_inverted() const { return (reinterpret_cast<size_t>(m_ref) & static_cast<size_t>(1)) == static_cast<size_t>(1); }
     void invert() { m_ref = reinterpret_cast<aig*>(reinterpret_cast<size_t>(m_ref) ^ static_cast<size_t>(1)); }
     aig * ptr() const { return reinterpret_cast<aig*>(reinterpret_cast<size_t>(m_ref) & ~static_cast<size_t>(1)); }
diff --git a/src/util/inf_s_integer.h b/src/util/inf_s_integer.h
index 873ad2bdec..12b2c08d0c 100644
--- a/src/util/inf_s_integer.h
+++ b/src/util/inf_s_integer.h
@@ -45,6 +45,7 @@ class inf_s_integer {
     std::string to_string() const;
 
     inf_s_integer() = default;
+    inf_s_integer(const inf_s_integer&) = default;
 
     explicit inf_s_integer(int n):m_first(n), m_second(0) {}
     explicit inf_s_integer(int n, int d): m_first(n), m_second(0) { SASSERT(d == 1); }
diff --git a/src/util/params.cpp b/src/util/params.cpp
index 751789c34f..4a997b11a4 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -361,7 +361,8 @@ class params {
             rational *    m_rat_value;
         };
         value() : m_kind(CPK_BOOL), m_bool_value(false) {}
-        value& operator=(value const& other) {
+        value(const value &) = default;
+        value &operator=(value const &other) {
             m_kind = other.m_kind;
             switch (m_kind) {
             case CPK_BOOL: m_bool_value = other.m_bool_value; break;
diff --git a/src/util/ref_buffer.h b/src/util/ref_buffer.h
index d82b0bd538..269d10ea62 100644
--- a/src/util/ref_buffer.h
+++ b/src/util/ref_buffer.h
@@ -174,7 +174,9 @@ public:
         super(ref_manager_wrapper<T, TManager>(other.m_manager)) {
         SASSERT(this->m_buffer.size() == 0);
         append(other);
-    }        
+    }
+
+    ref_buffer &operator=(const ref_buffer &) = default;
 };
 
 /**