diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index b1e81a9c57..a788224ad2 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -27,14 +27,11 @@ namespace smt {
     theory_array::theory_array(context& ctx):
         theory_array_base(ctx), 
         m_params(ctx.get_fparams()),
-        m_find(*this),
-        m_trail_stack(),
-        m_final_check_idx(0) {
+        m_find(*this) {
     }
 
     theory_array::~theory_array() {
         std::for_each(m_var_data.begin(), m_var_data.end(), delete_proc<var_data>());
-        m_var_data.reset();
     }
 
     void theory_array::init_search_eh() {
diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h
index 1337a86aed..b170b88e92 100644
--- a/src/smt/theory_array.h
+++ b/src/smt/theory_array.h
@@ -42,17 +42,16 @@ namespace smt {
             ptr_vector<enode>  m_stores;
             ptr_vector<enode>  m_parent_selects;
             ptr_vector<enode>  m_parent_stores;
-            bool               m_prop_upward;
-            bool               m_is_array;
-            bool               m_is_select;
-            var_data():m_prop_upward(false), m_is_array(false), m_is_select(false) {}
+            bool               m_prop_upward = false;
+            bool               m_is_array = false;
+            bool               m_is_select = false;
         };
         ptr_vector<var_data>            m_var_data;
         theory_array_params&            m_params;
         theory_array_stats              m_stats;
         th_union_find                   m_find;
         trail_stack                     m_trail_stack;
-        unsigned                        m_final_check_idx;
+        unsigned                        m_final_check_idx = 0;
 
         theory_var mk_var(enode * n) override;
         bool internalize_atom(app * atom, bool gate_ctx) override;
diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp
index 988f3fdad9..226c2abb41 100644
--- a/src/smt/theory_array_bapa.cpp
+++ b/src/smt/theory_array_bapa.cpp
@@ -98,10 +98,9 @@ namespace smt {
     
     class theory_array_bapa::imp {
         struct sz_info {
-            bool                  m_is_leaf;   // has it been split into disjoint subsets already?
-            rational              m_size;      // set to >= integer if fixed in final check, otherwise -1
+            bool                  m_is_leaf = true;               // has it been split into disjoint subsets already?
+            rational              m_size = rational::minus_one(); // set to >= integer if fixed in final check, otherwise -1
             obj_map<enode, expr*> m_selects;
-            sz_info(): m_is_leaf(true), m_size(rational::minus_one()) {}
         };
 
         typedef std::pair<func_decl*, func_decl*> func_decls;
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 345663b6bf..b92c0e560d 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -34,7 +34,6 @@ namespace smt {
 
     theory_array_full::~theory_array_full() {
         std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc<var_data_full>());
-        m_var_data_full.reset();
     }
 
     theory* theory_array_full::mk_fresh(context* new_ctx) { 
diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h
index 98e53627c9..5142e022da 100644
--- a/src/smt/theory_array_full.h
+++ b/src/smt/theory_array_full.h
@@ -23,7 +23,7 @@ Revision History:
 
 namespace smt {
 
-    class theory_array_full : public theory_array {
+    class theory_array_full final : public theory_array {
         struct var_data_full {
             ptr_vector<enode>  m_maps;
             ptr_vector<enode>  m_consts;