diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h
index 8d179ba33..09c4e333b 100644
--- a/src/ast/pattern/pattern_inference.h
+++ b/src/ast/pattern/pattern_inference.h
@@ -114,9 +114,9 @@ class pattern_inference_cfg :  public default_rewriter_cfg {
     //
     class collect {
         struct entry {
-            expr *    m_node;
-            unsigned  m_delta;
-            entry():m_node(nullptr), m_delta(0) {}
+            expr *    m_node = nullptr;
+            unsigned  m_delta = 0;
+            entry() = default;
             entry(expr * n, unsigned d):m_node(n), m_delta(d) {}
             unsigned hash() const { 
                 return hash_u_u(m_node->get_id(), m_delta);
diff --git a/src/util/chashtable.h b/src/util/chashtable.h
index b15d6017f..394e5998c 100644
--- a/src/util/chashtable.h
+++ b/src/util/chashtable.h
@@ -52,9 +52,8 @@ public:
 
 protected:
     struct cell {
-        cell *  m_next;
+        cell *  m_next = (cell*)1;
         T       m_data;
-        cell():m_next(reinterpret_cast<cell*>(1)) {}
         bool is_free() const { return GET_TAG(m_next) == 1; }
         void mark_free() { m_next = TAG(cell*, m_next, 1); }
         void unmark_free() { m_next = UNTAG(cell*, m_next); }
diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index af56c4507..a52e3e3bd 100644
--- a/src/util/memory_manager.h
+++ b/src/util/memory_manager.h
@@ -19,6 +19,7 @@ Revision History:
 #pragma once
 
 #include<cstdlib>
+#include<memory>
 #include<ostream>
 #include<iomanip>
 #include "util/z3_exception.h"
@@ -105,18 +106,14 @@ ALLOC_ATTR T * alloc_vect(unsigned sz);
 template<typename T>
 T * alloc_vect(unsigned sz) {
     T * r = static_cast<T*>(memory::allocate(sizeof(T) * sz));
-    T * curr = r;
-    for (unsigned i = 0; i < sz; i++, curr++) 
-        new (curr) T();
+    std::uninitialized_default_construct_n(r, sz);
     return r;
 }
 
 template<typename T>
 void dealloc_vect(T * ptr, unsigned sz) {
     if (ptr == nullptr) return;
-    T * curr = ptr;
-    for (unsigned i = 0; i < sz; i++, curr++)
-        curr->~T();
+    std::destroy_n(ptr, sz);
     memory::deallocate(ptr);
 }
 
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index 49b37ca61..dbb2b776e 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -56,10 +56,9 @@ template<typename Key, typename Value>
 class obj_map {
 public:
     struct key_data {
-        Key *  m_key;
+        Key *  m_key = nullptr;
         Value  m_value;
-        key_data():m_key(nullptr), m_value() {
-        }
+        key_data() = default;
         key_data(Key * k):
             m_key(k), m_value() {
         }
diff --git a/src/util/symbol.h b/src/util/symbol.h
index ab7d41c98..721351b7e 100644
--- a/src/util/symbol.h
+++ b/src/util/symbol.h
@@ -29,7 +29,7 @@ template<typename T>
 class symbol_table;
 
 class symbol {
-    char const * m_data;
+    char const * m_data = nullptr;
 
     template<typename T>
     friend class symbol_table;
@@ -50,9 +50,7 @@ class symbol {
     }
     static symbol m_dummy;
 public:
-    symbol():
-        m_data(nullptr) {
-    }
+    symbol() = default;
     explicit symbol(char const * d);
     explicit symbol(const std::string & str) : symbol(str.c_str()) {}
     explicit symbol(unsigned idx):
diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h
index 6a683f201..1a805ff35 100644
--- a/src/util/symbol_table.h
+++ b/src/util/symbol_table.h
@@ -31,8 +31,7 @@ class symbol_table {
         symbol   m_key;
         T        m_data;
      
-        key_data() {
-        }
+        key_data() = default;
 
         explicit key_data(symbol k):
             m_key(k) {
@@ -59,10 +58,12 @@ class symbol_table {
     struct hash_entry {
         typedef key_data data;
         key_data m_data;
-     
+
+#if 0
         hash_entry() {
             SASSERT(m_data.m_key == symbol::null);
         }
+#endif
 
         unsigned get_hash() const { 
             return m_data.m_key.hash();