diff --git a/src/api/api_polynomial.h b/src/api/api_polynomial.h
index 033d462118f..0dbcdd4e3de 100644
--- a/src/api/api_polynomial.h
+++ b/src/api/api_polynomial.h
@@ -28,9 +28,7 @@ namespace api {
         // TODO: add support for caching expressions -> polynomial and back
     public:
         pmanager(reslimit& lim) : m_pm(lim, m_nm) {}
-        ~pmanager() {}
         polynomial::manager & pm() { return m_pm; }
     };
 
-};
-
+}
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 07c3d102705..fb5072bc897 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -214,12 +214,10 @@ void display_parameters(std::ostream & out, unsigned n, parameter const * p);
    between symbols (family names) and the unique IDs.
 */
 class family_manager {
-    family_id               m_next_id;
+    family_id               m_next_id = 0;
     symbol_table<family_id> m_families;
     svector<symbol>         m_names;
 public:
-    family_manager():m_next_id(0) {}
-
     /**
        \brief Return the family_id for s, a new id is created if !has_family(s)
 
@@ -999,8 +997,8 @@ struct builtin_name {
 */
 class decl_plugin {
 protected:
-    ast_manager * m_manager;
-    family_id     m_family_id;
+    ast_manager * m_manager = nullptr;
+    family_id     m_family_id = null_family_id;
 
     virtual void set_manager(ast_manager * m, family_id id) {
         SASSERT(m_manager == nullptr);
@@ -1024,8 +1022,6 @@ class decl_plugin {
     friend class ast_manager;
 
 public:
-    decl_plugin():m_manager(nullptr), m_family_id(null_family_id) {}
-
     virtual ~decl_plugin() {}
     virtual void finalize() {}
 
@@ -1354,8 +1350,6 @@ class user_sort_plugin : public decl_plugin {
     svector<symbol> m_sort_names;
     dictionary<int> m_name2decl_kind;
 public:
-    user_sort_plugin() {}
-
     sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
     func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                              unsigned arity, sort * const * domain, sort * range) override;
@@ -2450,7 +2444,6 @@ typedef obj_mark<expr> expr_mark;
 class expr_sparse_mark {
     obj_hashtable<expr> m_marked;
 public:
-    expr_sparse_mark() {}
     bool is_marked(expr * n) const { return m_marked.contains(n); }
     void mark(expr * n) { m_marked.insert(n); }
     void mark(expr * n, bool flag) { if (flag) m_marked.insert(n); else m_marked.erase(n); }
@@ -2461,7 +2454,6 @@ template<unsigned IDX>
 class ast_fast_mark {
     ptr_buffer<ast> m_to_unmark;
 public:
-    ast_fast_mark() {}
     ~ast_fast_mark() {
         reset();
     }
@@ -2603,7 +2595,6 @@ class scoped_mark : public ast_mark {
     unsigned_vector m_lim;
 public:
     scoped_mark(ast_manager& m): m_stack(m) {}
-    ~scoped_mark() override {}
     void mark(ast * n, bool flag) override;
     void reset() override;
     void mark(ast * n);
@@ -2644,7 +2635,3 @@ struct parameter_pp {
 inline std::ostream& operator<<(std::ostream& out, parameter_pp const& pp) {
     return pp.m.display(out, pp.p);
 }
-
-
-
-
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 6ac438f16a4..34e1b5db4ae 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -105,7 +105,6 @@ namespace datatype {
         class size {
             unsigned m_ref{ 0 };
         public:
-            size() {}
             virtual ~size() { }
             void inc_ref() { ++m_ref; }
             void dec_ref();
@@ -124,7 +123,6 @@ namespace datatype {
         struct offset : public size {
             sort_size m_offset;
             offset(sort_size const& s): m_offset(s) {}
-            ~offset() override {}
             size* subst(obj_map<sort,size*>& S) override { return this; }
             sort_size eval(obj_map<sort, sort_size> const& S) override { return m_offset; }
         };
@@ -152,7 +150,6 @@ namespace datatype {
         struct sparam : public size {
             sort_ref m_param;
             sparam(sort_ref& p): m_param(p) {}
-            ~sparam() override {}
             size* subst(obj_map<sort, size*>& S) override;
             sort_size eval(obj_map<sort, sort_size> const& S) override { return S[m_param]; }
         };
diff --git a/src/ast/rewriter/ast_counter.h b/src/ast/rewriter/ast_counter.h
index 7f796098f5b..fb997c35b8d 100644
--- a/src/ast/rewriter/ast_counter.h
+++ b/src/ast/rewriter/ast_counter.h
@@ -35,8 +35,6 @@ class counter {
 public:
     typedef map_impl::iterator iterator;
     
-    counter() {}
-    
     void reset() { m_data.reset(); }
     iterator begin() const { return m_data.begin(); }
     iterator end() const { return m_data.end(); }    
@@ -74,7 +72,6 @@ class var_counter : public counter {
     unsigned_vector  m_scopes;
     unsigned get_max_var(bool & has_var);    
 public:
-    var_counter() {}
     void count_vars(const app * t, int coef = 1);
     unsigned get_max_var(expr* e);
     unsigned get_next_var(expr* e);
@@ -86,8 +83,6 @@ class ast_counter {
  public:
     typedef map_impl::iterator iterator;
     
-    ast_counter() {}
-    
     iterator begin() const { return m_data.begin(); }
     iterator end() const { return m_data.end(); }
     
diff --git a/src/ast/rewriter/recfun_rewriter.h b/src/ast/rewriter/recfun_rewriter.h
index a08a75783b1..f1c2ae44245 100644
--- a/src/ast/rewriter/recfun_rewriter.h
+++ b/src/ast/rewriter/recfun_rewriter.h
@@ -26,7 +26,6 @@ class recfun_rewriter {
     recfun::util  m_rec;
 public:
     recfun_rewriter(ast_manager& m): m(m), m_rec(m) {}
-    ~recfun_rewriter() {}
     
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
 
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 9adb4df3213..01f88112b07 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -160,7 +160,6 @@ class seq_decl_plugin : public decl_plugin {
 public:
     seq_decl_plugin();
 
-    ~seq_decl_plugin() override {}
     void finalize() override;
 
     bool unicode() const { return get_char_plugin().unicode(); }
@@ -575,8 +574,6 @@ class seq_util {
         re(*this) {
     }
 
-    ~seq_util() {}
-
     family_id get_family_id() const { return m_fid; }
 };
 
diff --git a/src/ast/shared_occs.h b/src/ast/shared_occs.h
index 468ce1436ab..59ff99569b6 100644
--- a/src/ast/shared_occs.h
+++ b/src/ast/shared_occs.h
@@ -24,8 +24,6 @@ Revision History:
 class shared_occs_mark {
     ptr_buffer<ast> m_to_unmark;
 public:
-    shared_occs_mark() {}
- 
     ~shared_occs_mark() {
         reset();
     }
diff --git a/src/ast/substitution/matcher.h b/src/ast/substitution/matcher.h
index 2c398956fa6..6ef02f2840b 100644
--- a/src/ast/substitution/matcher.h
+++ b/src/ast/substitution/matcher.h
@@ -36,8 +36,6 @@ class matcher {
     void reset();
 
 public:
-    matcher() {}
-
     /**
        \brief Return true if e2 is an instance of e1.
        In case of success (result is true), it will store the substitution that makes e1 equals to e2 into s.
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 61595e2661f..3ceb0d0693f 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -94,9 +94,8 @@ class macro_decls {
    \brief Generic wrapper.
 */
 class object_ref {
-    unsigned m_ref_count;
+    unsigned m_ref_count = 0;
 public:
-    object_ref():m_ref_count(0) {}
     virtual ~object_ref() {}
     virtual void finalize(cmd_context & ctx) = 0;
     void inc_ref(cmd_context & ctx) {
diff --git a/src/math/dd/pdd_eval.h b/src/math/dd/pdd_eval.h
index 3a5e85cf4a7..f7682927f85 100644
--- a/src/math/dd/pdd_eval.h
+++ b/src/math/dd/pdd_eval.h
@@ -26,9 +26,6 @@ class pdd_eval {
     std::function<rational (unsigned)> m_var2val;
     
 public:
-    
-    pdd_eval() {}
-    
     std::function<rational (unsigned)>& var2val() { return m_var2val; } // setter
     const std::function<rational (unsigned)>& var2val() const { return m_var2val; } // getter
     
diff --git a/src/math/grobner/pdd_simplifier.h b/src/math/grobner/pdd_simplifier.h
index c3fdbe03613..065350cb1f5 100644
--- a/src/math/grobner/pdd_simplifier.h
+++ b/src/math/grobner/pdd_simplifier.h
@@ -27,7 +27,6 @@ class simplifier {
 public:
 
     simplifier(solver& s): s(s) {}
-    ~simplifier() {}
 
     void operator()();
 
diff --git a/src/math/lp/gomory.h b/src/math/lp/gomory.h
index 58f1288d69e..68e42feb947 100644
--- a/src/math/lp/gomory.h
+++ b/src/math/lp/gomory.h
@@ -32,7 +32,6 @@ namespace lp {
         lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row);
     public:
         gomory(int_solver& lia);
-        ~gomory() {}
         lia_move operator()();
     };
 }
diff --git a/src/math/lp/int_branch.h b/src/math/lp/int_branch.h
index a7d72383a8d..9601cb65e1d 100644
--- a/src/math/lp/int_branch.h
+++ b/src/math/lp/int_branch.h
@@ -32,7 +32,6 @@ namespace lp {
 
     public:
         int_branch(int_solver& lia);
-        ~int_branch() {}
         lia_move operator()();
     };
 }
diff --git a/src/math/lp/int_cube.h b/src/math/lp/int_cube.h
index 18af0cbc10b..4addc096b59 100644
--- a/src/math/lp/int_cube.h
+++ b/src/math/lp/int_cube.h
@@ -35,7 +35,6 @@ namespace lp {
         impq get_cube_delta_for_term(const lar_term& t) const;
     public:
         int_cube(int_solver& lia);
-        ~int_cube() {}
         lia_move operator()();
     };
 }
diff --git a/src/math/lp/int_gcd_test.h b/src/math/lp/int_gcd_test.h
index 0734dc8aff0..84fd8f7eb20 100644
--- a/src/math/lp/int_gcd_test.h
+++ b/src/math/lp/int_gcd_test.h
@@ -47,7 +47,6 @@ namespace lp {
         void add_to_explanation_from_fixed_or_boxed_column(unsigned j);
     public:
         int_gcd_test(int_solver& lia);
-        ~int_gcd_test() {}
         lia_move operator()();
         bool should_apply();
     };
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 26759cb33e9..083b935a4ca 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -54,7 +54,6 @@ class nex {
     virtual unsigned size() const { return 1; }
     virtual expr_type type() const = 0;
     virtual std::ostream& print(std::ostream&) const = 0;    
-    nex() {}
     bool is_elementary() const {
         switch(type()) {
         case expr_type::SUM:
diff --git a/src/math/simplex/bit_matrix.h b/src/math/simplex/bit_matrix.h
index 189472d6abe..c827690ec43 100644
--- a/src/math/simplex/bit_matrix.h
+++ b/src/math/simplex/bit_matrix.h
@@ -92,8 +92,6 @@ class bit_matrix {
         bool operator!=(row_iterator const& other) const { return m_index != other.m_index; }  
     };
 
-    bit_matrix() {}
-    ~bit_matrix() {}
     void reset(unsigned num_columns);
     
     row_iterator begin() { return row_iterator(*this, true); }
diff --git a/src/math/subpaving/subpaving_types.h b/src/math/subpaving/subpaving_types.h
index 28150cc04a6..b914901a8f1 100644
--- a/src/math/subpaving/subpaving_types.h
+++ b/src/math/subpaving/subpaving_types.h
@@ -31,7 +31,7 @@ class exception {
 
 class power : public std::pair<var, unsigned> {
 public:
-    power():std::pair<var, unsigned>() {}
+    power() = default;
     power(var v, unsigned d):std::pair<var, unsigned>(v, d) {}
     var x() const { return first; }
     var get_var() const { return first; }
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 1e19d05c2c7..044260f126a 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -313,7 +313,6 @@ namespace datalog {
         static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); }
 
         rule() : m_ref_cnt(0), m_name(symbol::null) {}
-        ~rule() {}
 
         void deallocate(ast_manager & m);
 
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index 147fc26f151..909539a85c1 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -178,7 +178,7 @@ namespace datalog {
 
         class base_fn {
         public:
-            base_fn() {}
+            base_fn() = default;
             virtual ~base_fn() {}
         private:
             //private and undefined copy constructor and operator= to avoid copying
@@ -219,8 +219,6 @@ namespace datalog {
         */
         class mutator_fn : public base_fn {
         public:
-            ~mutator_fn() override {}
-
             virtual void operator()(base_object & t) = 0;
 
             virtual bool supports_attachment(base_object& other) { return false; }
diff --git a/src/muz/rel/dl_bound_relation.h b/src/muz/rel/dl_bound_relation.h
index 69459e92016..8f852f0ba4b 100644
--- a/src/muz/rel/dl_bound_relation.h
+++ b/src/muz/rel/dl_bound_relation.h
@@ -94,7 +94,6 @@ namespace datalog {
     struct uint_set2 {
         uint_set lt;
         uint_set le;
-        uint_set2() {}
         bool operator==(const uint_set2& other) const {
             return other.lt == lt && other.le == le;
         }
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index e74bf22e60b..ca0c462adb3 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -235,7 +235,6 @@ class pred_transformer {
     public:
         frames (pred_transformer &pt) : m_pt (pt),
                                         m_size(0), m_sorted (true) {}
-        ~frames() {}
         void simplify_formulas ();
 
         pred_transformer& pt() const {return m_pt;}
@@ -356,7 +355,6 @@ class pred_transformer {
         rule2ptrule m_rules;
         tag2ptrule m_tags;
     public:
-        pt_rules() {}
         ~pt_rules() {for (auto &kv : m_rules) {dealloc(kv.m_value);}}
 
         bool find_by_rule(const datalog::rule &r, pt_rule* &ptr) {
@@ -439,7 +437,6 @@ class pred_transformer {
 
 public:
     pred_transformer(context& ctx, manager& pm, func_decl* head);
-    ~pred_transformer() {}
 
     inline bool use_native_mbp ();
     bool mk_mdl_rf_consistent(const datalog::rule *r, model &mdl);
@@ -825,7 +822,6 @@ class pob_queue {
 
 public:
     pob_queue(): m_root(nullptr), m_max_level(0), m_min_depth(0) {}
-    ~pob_queue() {}
 
     void reset();
     pob* top();
diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h
index 83a5e51259f..07e4ed678bd 100644
--- a/src/parsers/smt2/smt2scanner.h
+++ b/src/parsers/smt2/smt2scanner.h
@@ -75,9 +75,7 @@ namespace smt2 {
             EOF_TOKEN
         };
         
-        scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);
-        
-        ~scanner() {}    
+        scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);  
         
         int get_line() const { return m_line; }
         int get_pos() const { return m_pos; }
diff --git a/src/parsers/util/scanner.h b/src/parsers/util/scanner.h
index bd1b29c33ce..a0beaeff325 100644
--- a/src/parsers/util/scanner.h
+++ b/src/parsers/util/scanner.h
@@ -39,8 +39,6 @@ class scanner {
 
     scanner(std::istream& stream, std::ostream& err, bool smt2, bool bv_token=false);
 
-    ~scanner() {}    
-    
     int get_line() const { return m_line; }
 
     int get_pos() const { return m_pos; }
@@ -86,5 +84,3 @@ class scanner {
     token read_bv_literal();
     bool state_ok();
 };
-
-
diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h
index 58f3953a05e..eb5fea442b1 100644
--- a/src/sat/dimacs.h
+++ b/src/sat/dimacs.h
@@ -63,7 +63,6 @@ namespace dimacs {
         unsigned        m_node_id{ 0 };
         std::string     m_name;
         unsigned_vector m_args;
-        drat_record() {}
     };
 
     struct drat_pp {
@@ -111,6 +110,3 @@ namespace dimacs {
 
     };
 };
-
-
-
diff --git a/src/sat/sat_aig_finder.h b/src/sat/sat_aig_finder.h
index 83e8fcaf4f4..0928e3c0a40 100644
--- a/src/sat/sat_aig_finder.h
+++ b/src/sat/sat_aig_finder.h
@@ -52,7 +52,6 @@ namespace sat {
 
     public:
         aig_finder(solver& s);
-        ~aig_finder() {}                
         void set(std::function<void (literal head, literal_vector const& ands)> const& f) { m_on_aig = f; }
         void set(std::function<void (literal head, literal cond, literal th, literal el)> const& f) { m_on_if = f; }
         void operator()(clause_vector& clauses);
diff --git a/src/sat/sat_anf_simplifier.h b/src/sat/sat_anf_simplifier.h
index d3042831107..0f140d5ab48 100644
--- a/src/sat/sat_anf_simplifier.h
+++ b/src/sat/sat_anf_simplifier.h
@@ -111,7 +111,6 @@ namespace sat {
 
     public:
         anf_simplifier(solver& s) : s(s), m_eval_ts(0) {}
-        ~anf_simplifier() {}
         
         void operator()();
         void set(config const& cfg) { m_config = cfg; }
diff --git a/src/sat/sat_binspr.h b/src/sat/sat_binspr.h
index 82a5a128c46..f533ff48952 100644
--- a/src/sat/sat_binspr.h
+++ b/src/sat/sat_binspr.h
@@ -97,8 +97,6 @@ namespace sat {
             memset(m_false, 0, sizeof(unsigned) * max_lits);
         }
 
-        ~binspr() {}
-
         void operator()();
 
         void updt_params(params_ref const& p) {}
diff --git a/src/sat/sat_lut_finder.h b/src/sat/sat_lut_finder.h
index 62f99f7f781..d51f403888e 100644
--- a/src/sat/sat_lut_finder.h
+++ b/src/sat/sat_lut_finder.h
@@ -69,7 +69,6 @@ namespace sat {
         lut_finder(solver& s) : s(s), m_max_lut_size(5) { 
             memset(m_masks, 0, sizeof(uint64_t)*7);
         }
-        ~lut_finder() {}        
 
         void set(std::function<void (uint64_t, bool_var_vector const&, bool_var)>& f) { m_on_lut = f; }
 
diff --git a/src/sat/sat_npn3_finder.h b/src/sat/sat_npn3_finder.h
index f3285e4e910..e7364e16d83 100644
--- a/src/sat/sat_npn3_finder.h
+++ b/src/sat/sat_npn3_finder.h
@@ -115,7 +115,6 @@ namespace sat {
 
     public:
         npn3_finder(solver& s);
-        ~npn3_finder() {}
         void set_on_mux(std::function<void(literal head, literal cond, literal th, literal el)> const& f) { m_on_mux = f; }
         void set_on_maj(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_maj = f; }
         void set_on_orand(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_orand = f; }
diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h
index 3693cf323ac..68266760ba0 100644
--- a/src/sat/sat_parallel.h
+++ b/src/sat/sat_parallel.h
@@ -41,7 +41,6 @@ namespace sat {
             unsigned get_length(unsigned index) const { return m_vectors[index+1]; }
             unsigned const* get_ptr(unsigned index) const { return m_vectors.data() + index + 2; }
         public:
-            vector_pool() {}
             void reserve(unsigned num_owners, unsigned sz);
             void begin_add_vector(unsigned owner, unsigned n);
             void end_add_vector();
diff --git a/src/sat/sat_prob.h b/src/sat/sat_prob.h
index 048fc448c72..305e76b8bcc 100644
--- a/src/sat/sat_prob.h
+++ b/src/sat/sat_prob.h
@@ -31,9 +31,8 @@ namespace sat {
     class prob : public i_local_search {
 
         struct clause_info {
-            clause_info(): m_trues(0), m_num_trues(0) {}
-            unsigned m_trues;        // set of literals that are true
-            unsigned m_num_trues;    // size of true set
+            unsigned m_trues = 0;        // set of literals that are true
+            unsigned m_num_trues = 0;    // size of true set
             bool is_true() const { return m_num_trues > 0; }
             void add(literal lit) { ++m_num_trues; m_trues += lit.index(); }
             void del(literal lit) { SASSERT(m_num_trues > 0); --m_num_trues; m_trues -= lit.index(); }
@@ -129,8 +128,6 @@ namespace sat {
         void add(unsigned sz, literal const* c);
 
     public:
-        prob() {}
-
         ~prob() override;
 
         lbool check(unsigned sz, literal const* assumptions, parallel* p) override;
diff --git a/src/sat/sat_xor_finder.h b/src/sat/sat_xor_finder.h
index 3e9351af934..d0081653e21 100644
--- a/src/sat/sat_xor_finder.h
+++ b/src/sat/sat_xor_finder.h
@@ -62,7 +62,6 @@ namespace sat {
 
     public:
         xor_finder(solver& s) : s(s), m_max_xor_size(5) { init_parity(); }
-        ~xor_finder() {}        
 
         void set(std::function<void (literal_vector const& lits)>& f) { m_on_xor = f; }
 
diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index 3b87d65f3ff..6cd5274c952 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -54,7 +54,6 @@ namespace array {
             euf::enode_vector   m_lambdas;             // equivalent nodes that have beta reduction properties
             euf::enode_vector   m_parent_lambdas;      // parents that have beta reduction properties
             euf::enode_vector   m_parent_selects;      // parents that use array in select position
-            var_data() {}
         };
 
 
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index 4978797a6bc..d9a43ddeadc 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -106,7 +106,6 @@ namespace smt {
 
     class quantifier_manager_plugin {
     public:
-        quantifier_manager_plugin() {}
         virtual ~quantifier_manager_plugin() {}
 
         virtual void set_manager(quantifier_manager & qm) = 0;
diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h
index 29032e915f2..53bf4807d6c 100644
--- a/src/smt/smt_relevancy.h
+++ b/src/smt/smt_relevancy.h
@@ -29,7 +29,6 @@ namespace smt {
         void mark_as_relevant(relevancy_propagator & rp, expr * n);
         void mark_args_as_relevant(relevancy_propagator & rp, app * n);
     public:
-        relevancy_eh() {}
         virtual ~relevancy_eh() {}
         /**
            \brief This method is invoked when n is marked as relevant.
@@ -49,7 +48,6 @@ namespace smt {
         expr * m_target;
     public:
         simple_relevancy_eh(expr * t):m_target(t) {}
-        ~simple_relevancy_eh() override {}
         void operator()(relevancy_propagator & rp) override;
     };
     
@@ -62,7 +60,6 @@ namespace smt {
         expr * m_target;
     public:
         pair_relevancy_eh(expr * s1, expr * s2, expr * t):m_source1(s1), m_source2(s2), m_target(t) {}
-        ~pair_relevancy_eh() override {}
         void operator()(relevancy_propagator & rp) override;
     };
 
diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h
index e5bb2668dfe..19b0e2f6d3d 100644
--- a/src/smt/theory_array_full.h
+++ b/src/smt/theory_array_full.h
@@ -29,7 +29,6 @@ namespace smt {
             ptr_vector<enode>  m_consts;
             ptr_vector<enode>  m_as_arrays;
             ptr_vector<enode>  m_parent_maps;
-            var_data_full() {}
         };
 
         ptr_vector<var_data_full> m_var_data_full;
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 285c03b3578..99e70bd7474 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -77,7 +77,6 @@ namespace smt {
                 m_pos(pos),
                 m_neg(neg) {
             }
-            ~atom() {}
             bool_var get_bool_var() const { return m_bvar; }
             bool is_true() const { return m_true; }
             void assign_eh(bool is_true) { m_true = is_true; }
@@ -383,24 +382,21 @@ namespace smt {
         static const bool m_int_theory = true;
         typedef rational numeral;
         typedef rational fin_numeral;
-        numeral     m_epsilon;
-        idl_ext() : m_epsilon(1) {}
+        numeral     m_epsilon { 1 };
     };
 
     struct sidl_ext {
         static const bool m_int_theory = true;
         typedef s_integer numeral;
         typedef s_integer fin_numeral;
-        numeral m_epsilon;
-        sidl_ext() : m_epsilon(1) {}
+        numeral m_epsilon { 1 };
     };
 
     struct rdl_ext {
         static const bool m_int_theory = false;
         typedef inf_int_rational numeral;
         typedef rational fin_numeral;
-        numeral      m_epsilon;        
-        rdl_ext() : m_epsilon(rational(), true) {}
+        numeral      m_epsilon { rational(), true };
     };
 
     //
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 2006e013b92..99344eb3142 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -77,7 +77,6 @@ namespace smt {
             atom(bool_var bv, int pos, int neg) : 
                 m_bvar(bv), m_true(false),
                 m_pos(pos), m_neg(neg) {}
-            ~atom() {}
             bool_var get_bool_var() const { return m_bvar; }
             void assign_eh(bool is_true) { m_true = is_true; }
             int get_asserted_edge() const { return this->m_true?m_pos:m_neg; }
diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h
index 3e6dd909856..80bebabcc9b 100644
--- a/src/solver/smt_logics.h
+++ b/src/solver/smt_logics.h
@@ -20,7 +20,6 @@ Revision History:
 
 class smt_logics {
 public:
-    smt_logics() {}        
     static bool supported_logic(symbol const & s);
     static bool logic_has_reals_only(symbol const& l);       
     static bool logic_is_all(symbol const& s) { return s == "ALL"; }
@@ -36,5 +35,3 @@ class smt_logics {
     static bool logic_has_fd(symbol const& s) { return s == "QF_FD"; }
     static bool logic_has_datatype(symbol const& s);
 };
-
-
diff --git a/src/tactic/arith/linear_equation.h b/src/tactic/arith/linear_equation.h
index b3d43ab5ec0..5220a1e46fc 100644
--- a/src/tactic/arith/linear_equation.h
+++ b/src/tactic/arith/linear_equation.h
@@ -68,7 +68,6 @@ class linear_equation_manager {
 
 public:
     linear_equation_manager(numeral_manager & _m, small_object_allocator & a):m_allocator(a), m(_m), m_int_buffer(m), m_val_buffer(m) {}
-    ~linear_equation_manager() {}
 
     linear_equation * mk(unsigned sz, mpq * as, var * xs, bool normalized = false);
     linear_equation * mk(unsigned sz, mpz * as, var * xs, bool normalized = false);
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 3b5005347e2..541d50838c2 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -64,8 +64,6 @@ class expr_dominators {
 
 class dom_simplifier {
  public:
-    dom_simplifier() {}
-    
     virtual ~dom_simplifier() {}
     /**
        \brief assert_expr performs an implicit push
diff --git a/src/util/approx_set.h b/src/util/approx_set.h
index bce67f69264..7355437b971 100644
--- a/src/util/approx_set.h
+++ b/src/util/approx_set.h
@@ -164,7 +164,7 @@ typedef approx_set_tpl<unsigned, u2u> u_approx_set;
 
 class approx_set : public u_approx_set {
 public:
-    approx_set():u_approx_set() {}
+    approx_set() = default;
     approx_set(unsigned e):u_approx_set(e) {}
     
     class iterator {
diff --git a/src/util/basic_interval.h b/src/util/basic_interval.h
index 1c15317e038..ca5868b8817 100644
--- a/src/util/basic_interval.h
+++ b/src/util/basic_interval.h
@@ -33,7 +33,6 @@ class basic_interval_manager {
         bound m_lower;
         bound m_upper;
     public:
-        interval() {}
         bound const & lower() const { return m_lower; }
         bound const & upper() const { return m_upper; }
         bound & lower() { return m_lower; }
diff --git a/src/util/buffer.h b/src/util/buffer.h
index b778451a751..4c363fe9127 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -87,11 +87,13 @@ class buffer {
                 push_back(std::move(source.m_buffer[i]));
             }
         } else {
-            m_pos           = source.m_pos;
-            m_capacity      = source.m_capacity;
-            m_buffer        = source.m_buffer;
-            source.m_buffer = reinterpret_cast<T*>(source.m_initial_buffer);
-            source.m_pos    = 0;
+            m_buffer          = source.m_buffer;
+            m_pos             = source.m_pos;
+            m_capacity        = source.m_capacity;
+            m_buffer          = source.m_buffer;
+            source.m_buffer   = reinterpret_cast<T*>(source.m_initial_buffer);
+            source.m_pos      = 0;
+            source.m_capacity = INITIAL_SIZE;
         }
     }
 
diff --git a/src/util/dictionary.h b/src/util/dictionary.h
index dab52f938cc..a65144b3f9d 100644
--- a/src/util/dictionary.h
+++ b/src/util/dictionary.h
@@ -20,8 +20,4 @@ Module Name:
 #include "util/symbol.h"
 
 template<typename T>
-class dictionary : public map<symbol, T, symbol_hash_proc, symbol_eq_proc> {
-public:
-    dictionary() {}
-};
-
+using dictionary = map<symbol, T, symbol_hash_proc, symbol_eq_proc>;
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index e904abe11eb..cfe4d20cabf 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -44,11 +44,10 @@ typedef enum { HT_FREE,
 template<typename T>
 class default_hash_entry {
     unsigned         m_hash{ 0 }; //!< cached hash code
-    hash_entry_state m_state;
+    hash_entry_state m_state = HT_FREE;
     T                m_data;
 public:
     typedef T         data;
-    default_hash_entry():m_state(HT_FREE), m_data() {}
     unsigned get_hash() const  { return m_hash; }
     bool is_free() const { return m_state == HT_FREE; }
     bool is_deleted() const { return m_state == HT_DELETED; }
@@ -67,10 +66,9 @@ class default_hash_entry {
 template<int Free, int Deleted>
 class int_hash_entry {
     unsigned         m_hash; //!< cached hash code
-    int              m_data;
+    int              m_data = Free;
 public:
     typedef int data;
-    int_hash_entry():m_data(Free) {}
     unsigned get_hash() const { return m_hash; }
     bool is_free() const { return m_data == Free; }
     bool is_deleted() const { return m_data == Deleted; }
@@ -89,10 +87,9 @@ class int_hash_entry {
 template<typename T>
 class ptr_hash_entry {
     unsigned        m_hash; //!< cached hash code
-    T *             m_ptr;
+    T *             m_ptr = nullptr;
 public:
     typedef T * data;
-    ptr_hash_entry():m_ptr(nullptr) {}
     unsigned get_hash() const { return m_hash; }
     bool is_free() const { return m_ptr == nullptr; }
     bool is_deleted() const { return m_ptr == reinterpret_cast<T *>(1); }
@@ -112,10 +109,9 @@ class ptr_hash_entry {
 */
 template<typename T>
 class ptr_addr_hash_entry : public ptr_hash_entry<T> {
-    T *             m_ptr;
+    T *             m_ptr = nullptr;
 public:
     typedef T * data;
-    ptr_addr_hash_entry():m_ptr(nullptr) {}
     unsigned get_hash() const { return get_ptr_hash(m_ptr); }
     bool is_free() const { return m_ptr == nullptr; }
     bool is_deleted() const { return m_ptr == reinterpret_cast<T *>(1); }
diff --git a/src/util/lim_vector.h b/src/util/lim_vector.h
index 1249a965720..15cc286a206 100644
--- a/src/util/lim_vector.h
+++ b/src/util/lim_vector.h
@@ -22,8 +22,6 @@ template<typename T>
 class lim_svector : public svector<T, unsigned> {
     unsigned_vector  m_lim;
 public:
-    lim_svector() {}
-
     void push_scope() {
         m_lim.push_back(this->size());
     }
diff --git a/src/util/max_cliques.h b/src/util/max_cliques.h
index 0bf67592c1b..64a718bd13f 100644
--- a/src/util/max_cliques.h
+++ b/src/util/max_cliques.h
@@ -86,8 +86,6 @@ class max_cliques : public T {
     unsigned_vector const& next(unsigned vertex) const { return m_next[vertex]; }
     
 public:
-    max_cliques() {}
-
     void add_edge(unsigned src, unsigned dst) {
         m_next.reserve(std::max(src, dst) + 1);
         m_next.reserve(std::max(negate(src), negate(dst)) + 1);
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index e45bcc57b24..254f5f70d7d 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -29,10 +29,9 @@ Revision History:
 */
 template<typename T>
 class obj_hash_entry {
-    T *             m_ptr;
+    T *             m_ptr = nullptr;
 public:
     typedef T * data;
-    obj_hash_entry():m_ptr(nullptr) {}
     unsigned get_hash() const { return m_ptr->hash(); }
     bool is_free() const { return m_ptr == nullptr; }
     bool is_deleted() const { return m_ptr == reinterpret_cast<T *>(1); }
@@ -82,7 +81,6 @@ class obj_map {
         key_data m_data;
     public:
         typedef key_data data;
-        obj_map_entry() {}
         unsigned get_hash() const { return m_data.hash(); }
         bool is_free() const { return m_data.m_key == nullptr; }
         bool is_deleted() const { return m_data.m_key == reinterpret_cast<Key *>(1); }
diff --git a/src/util/obj_pair_hashtable.h b/src/util/obj_pair_hashtable.h
index 03fdcc0170c..e9d2e9bb543 100644
--- a/src/util/obj_pair_hashtable.h
+++ b/src/util/obj_pair_hashtable.h
@@ -29,11 +29,10 @@ Revision History:
 template<typename T1, typename T2>
 class obj_pair_hash_entry {
     unsigned            m_hash; // cached hash code
-    std::pair<T1*, T2*> m_data;
+    std::pair<T1*, T2*> m_data { nullptr, nullptr };
     
 public:
     typedef std::pair<T1*, T2*> data;
-    obj_pair_hash_entry():m_data(static_cast<T1*>(nullptr),static_cast<T2*>(nullptr)) {}
     unsigned get_hash() const { return m_hash; }
     bool is_free() const { return m_data.first == 0; }
     bool is_deleted() const { return m_data.first == reinterpret_cast<T1 *>(1); }
@@ -94,7 +93,6 @@ class obj_pair_map {
         key_data m_data;
     public:
         typedef key_data data;
-        entry() {}
         unsigned get_hash() const { return m_data.hash(); }
         bool is_free() const { return m_data.m_key1 == nullptr; }
         bool is_deleted() const { return m_data.m_key1 == reinterpret_cast<Key1 *>(1); }
diff --git a/src/util/obj_pair_set.h b/src/util/obj_pair_set.h
index 83cc00bd84a..8280e252115 100644
--- a/src/util/obj_pair_set.h
+++ b/src/util/obj_pair_set.h
@@ -34,7 +34,6 @@ class obj_pair_set {
     typedef chashtable<obj_pair, hash_proc, eq_proc> set;
     set m_set;
 public:
-    obj_pair_set() {}
     void insert(T1 * t1, T2 * t2) { m_set.insert(obj_pair(t1, t2)); }
     void insert(obj_pair const & p) { m_set.insert(p); }
     bool insert_if_not_there(T1 * t1, T2 * t2) { return m_set.insert_if_not_there2(obj_pair(t1, t2)); }
diff --git a/src/util/obj_triple_hashtable.h b/src/util/obj_triple_hashtable.h
index cd1f17651bf..7d75084fe98 100644
--- a/src/util/obj_triple_hashtable.h
+++ b/src/util/obj_triple_hashtable.h
@@ -30,11 +30,10 @@ Revision History:
 template<typename T1, typename T2, typename T3>
 class obj_triple_hash_entry {
     unsigned            m_hash; // cached hash code
-    triple<T1*, T2*, T3*> m_data;
+    triple<T1*, T2*, T3*> m_data { nullptr, nullptr, nullptr };
     
 public:
     typedef triple<T1*, T2*, T3*> data;
-    obj_triple_hash_entry():m_data(0,0,0) {}
     unsigned get_hash() const { return m_hash; }
     bool is_free() const { return m_data.first == 0; }
     bool is_deleted() const { return m_data.first == reinterpret_cast<T1 *>(1); }
@@ -99,7 +98,6 @@ class obj_triple_map {
         key_data m_data;
     public:
         typedef key_data data;
-        entry() {}
         unsigned get_hash() const { return m_data.hash(); }
         bool is_free() const { return m_data.m_key1 == nullptr; }
         bool is_deleted() const { return m_data.m_key1 == reinterpret_cast<Key1 *>(1); }
diff --git a/src/util/sat_literal.h b/src/util/sat_literal.h
index 1e587644e17..ccfecffbadf 100644
--- a/src/util/sat_literal.h
+++ b/src/util/sat_literal.h
@@ -87,7 +87,7 @@ namespace sat {
     };
 
     const literal null_literal;
-    struct literal_hash : obj_hash<literal> {};
+    using literal_hash = obj_hash<literal>;
 
     inline literal to_literal(unsigned x) { literal l; l.m_val = x; return l; }
     inline bool operator<(literal const & l1, literal const & l2) { return l1.m_val < l2.m_val;  }
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 664efefdaeb..c82d2585773 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -24,7 +24,6 @@ Revision History:
 class union_find_default_ctx {
 public:
     typedef trail_stack _trail_stack;
-    union_find_default_ctx() : m_stack() {}
        
     void unmerge_eh(unsigned, unsigned) {}
     void merge_eh(unsigned, unsigned, unsigned, unsigned) {}
@@ -51,7 +50,6 @@ class union_find {
         union_find & m_owner;
     public:
         mk_var_trail(union_find & o):m_owner(o) {}
-        ~mk_var_trail() override {}
         void undo() override {
             m_owner.m_find.pop_back();
             m_owner.m_size.pop_back();
@@ -69,7 +67,6 @@ class union_find {
         unsigned     m_r1;
     public:
         merge_trail(union_find & o, unsigned r1):m_owner(o), m_r1(r1) {}
-        ~merge_trail() override {}
         void undo() override { m_owner.unmerge(m_r1); }
     };