diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index c6e551a3c..5d94e77a1 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -33,6 +33,7 @@ Notes:
 #include "util/scoped_numeral_buffer.h"
 #include "util/ref_buffer.h"
 #include "util/common_msgs.h"
+#include <memory>
 
 namespace polynomial {
 
@@ -528,7 +529,7 @@ namespace polynomial {
             SASSERT(new_capacity > m_capacity);
             monomial * new_ptr  = allocate(new_capacity);
             new_ptr->m_size = m_ptr->m_size;
-            memcpy(new_ptr->m_powers, m_ptr->m_powers, sizeof(power)*m_ptr->m_size);
+            std::uninitialized_copy(m_ptr->m_powers, m_ptr->m_powers + m_ptr->m_size, new_ptr->m_powers);
             deallocate(m_ptr, m_capacity);
             m_ptr      = new_ptr;
             m_capacity = new_capacity;
diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h
index 76e479535..21f7c020e 100644
--- a/src/math/subpaving/subpaving_t_def.h
+++ b/src/math/subpaving/subpaving_t_def.h
@@ -21,6 +21,7 @@ Revision History:
 #include "util/buffer.h"
 #include "util/z3_exception.h"
 #include "util/common_msgs.h"
+#include <memory>
 
 namespace subpaving {
 
@@ -363,7 +364,7 @@ template<typename C>
 context_t<C>::monomial::monomial(unsigned sz, power const * pws):
     definition(constraint::MONOMIAL),
     m_size(sz) {
-    memcpy(m_powers, pws, sz*sizeof(power));
+    std::uninitialized_copy(pws, pws + sz, m_powers);
     std::sort(m_powers, m_powers+sz, typename power::lt_proc());
     DEBUG_CODE({
             for (unsigned i = 0; i < sz; i ++) {
diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp
index d78c8131e..aae9bf1ab 100644
--- a/src/sat/sat_cutset.cpp
+++ b/src/sat/sat_cutset.cpp
@@ -12,10 +12,11 @@
   --*/
 
 
-#include <sstream>
 #include "util/hashtable.h"
 #include "sat/sat_cutset.h"
 #include "sat/sat_cutset_compute_shift.h"
+#include <memory>
+#include <sstream>
 
 
 namespace sat {
@@ -84,8 +85,8 @@ namespace sat {
         }
         if (m_size == m_max_size) {
             m_max_size *= 2;
-            cut* new_cuts = new (*m_region) cut[m_max_size]; 
-            memcpy(new_cuts, m_cuts, sizeof(cut)*m_size);
+            cut* new_cuts = new (*m_region) cut[m_max_size];
+            std::uninitialized_copy(m_cuts, m_cuts + m_size, new_cuts);
             m_cuts = new_cuts;
         }
         if (m_var != UINT_MAX && on_add) on_add(m_var, c);
diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp
index 3eef0ac5f..34fe21e77 100644
--- a/src/smt/smt_justification.cpp
+++ b/src/smt/smt_justification.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include "smt/smt_conflict_resolution.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
+#include <memory>
 
 namespace smt {
 
@@ -302,8 +303,7 @@ namespace smt {
         simple_justification(r, num_lits, lits),
         m_num_eqs(num_eqs) {
         m_eqs = new (r) enode_pair[num_eqs];
-        if (num_eqs != 0)
-            memcpy(m_eqs, eqs, sizeof(enode_pair) * num_eqs);
+        std::uninitialized_copy(eqs, eqs + num_eqs, m_eqs);
         DEBUG_CODE({
             for (unsigned i = 0; i < num_eqs; i++) {
                 SASSERT(eqs[i].first->get_root() == eqs[i].second->get_root());
diff --git a/src/util/buffer.h b/src/util/buffer.h
index cd8c1d4ac..aec826a55 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -19,8 +19,7 @@ Revision History:
 
 
 --*/
-#ifndef BUFFER_H_
-#define BUFFER_H_
+#pragma once
 
 #include<string.h>
 #include "util/memory_manager.h"
@@ -42,7 +41,9 @@ protected:
     void expand() {
         unsigned new_capacity = m_capacity << 1;
         T * new_buffer        = reinterpret_cast<T*>(memory::allocate(sizeof(T) * new_capacity));
-        memcpy(new_buffer, m_buffer, m_pos * sizeof(T));
+        for (unsigned i = 0; i < m_pos; ++i) {
+            new (&new_buffer[i]) T(std::move(m_buffer[i]));
+        }
         free_memory();
         m_buffer              = new_buffer;
         m_capacity            = new_capacity;
@@ -269,7 +270,3 @@ public:
     sbuffer(): buffer<T, false, INITIAL_SIZE>() {}
     sbuffer(unsigned sz, const T& elem) : buffer<T, false, INITIAL_SIZE>(sz,elem) {}
 };
-
-
-
-#endif /* BUFFER_H_ */
diff --git a/src/util/vector.h b/src/util/vector.h
index 5dfb199a4..b1929ed0c 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -79,11 +79,7 @@ class vector {
                 throw default_exception("Overflow encountered when expanding vector");
             }
             SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
-#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5
-            if (__has_trivial_copy(T)) {
-#else
             if (std::is_trivially_copyable<T>::value) {
-#endif
                 mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
                 m_data = reinterpret_cast<T *>(mem + 2);
             } else {