diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp
index 76c1803f2..ec4727152 100644
--- a/src/ackermannization/lackr_model_constructor.cpp
+++ b/src/ackermannization/lackr_model_constructor.cpp
@@ -41,8 +41,6 @@ public:
         , m_ackr_helper(m)
     {}
     
-    ~imp() { }
-    
     //
     // Returns true iff model was successfully constructed.
     // Conflicts are saved as a side effect.
diff --git a/src/ast/ast_pp_dot.cpp b/src/ast/ast_pp_dot.cpp
index 47da4d4f4..1298239a2 100644
--- a/src/ast/ast_pp_dot.cpp
+++ b/src/ast/ast_pp_dot.cpp
@@ -45,8 +45,6 @@ struct ast_pp_dot_st {
         m_printed(),
         m_to_print(),
         m_first(true) {}
-
-    ~ast_pp_dot_st() {};
     
     void push_term(const expr * a) { m_to_print.push_back(a); }        
 
diff --git a/src/ast/euf/euf_ac_plugin.h b/src/ast/euf/euf_ac_plugin.h
index 7da346dba..2963c1f8b 100644
--- a/src/ast/euf/euf_ac_plugin.h
+++ b/src/ast/euf/euf_ac_plugin.h
@@ -47,7 +47,6 @@ namespace euf {
             unsigned_vector eqs;       // equality occurrences
             
             unsigned root_id() const { return root->n->get_id(); }
-            ~node() {}
             static node* mk(region& r, enode* n);
         };
 
@@ -270,8 +269,6 @@ namespace euf {
         ac_plugin(egraph& g, unsigned fid, unsigned op);
 
         ac_plugin(egraph& g, func_decl* f);
-
-        ~ac_plugin() override {}
         
         theory_id get_id() const override { return m_fid; }
 
diff --git a/src/ast/euf/euf_arith_plugin.h b/src/ast/euf/euf_arith_plugin.h
index 4c2a88d36..0cc122d99 100644
--- a/src/ast/euf/euf_arith_plugin.h
+++ b/src/ast/euf/euf_arith_plugin.h
@@ -33,8 +33,6 @@ namespace euf {
     public:
         arith_plugin(egraph& g);
 
-        ~arith_plugin() override {}
-
         theory_id get_id() const override { return a.get_family_id(); }
 
         void register_node(enode* n) override;
diff --git a/src/ast/euf/euf_bv_plugin.h b/src/ast/euf/euf_bv_plugin.h
index ec2c0b448..6bf48df2a 100644
--- a/src/ast/euf/euf_bv_plugin.h
+++ b/src/ast/euf/euf_bv_plugin.h
@@ -95,8 +95,6 @@ namespace euf {
     public:
         bv_plugin(egraph& g);
 
-        ~bv_plugin() override {}
-
         theory_id get_id() const override { return bv.get_family_id(); }
 
         void register_node(enode* n) override;
diff --git a/src/ast/euf/euf_specrel_plugin.h b/src/ast/euf/euf_specrel_plugin.h
index ae93bd2a5..5e3578ccf 100644
--- a/src/ast/euf/euf_specrel_plugin.h
+++ b/src/ast/euf/euf_specrel_plugin.h
@@ -34,8 +34,6 @@ namespace euf {
     public:
 
         specrel_plugin(egraph& g);
-
-        ~specrel_plugin() override {}
         
         theory_id get_id() const override { return sp.get_family_id(); }
 
diff --git a/src/ast/rewriter/label_rewriter.cpp b/src/ast/rewriter/label_rewriter.cpp
index 8adefb896..548d4fa82 100644
--- a/src/ast/rewriter/label_rewriter.cpp
+++ b/src/ast/rewriter/label_rewriter.cpp
@@ -26,8 +26,6 @@ label_rewriter::label_rewriter(ast_manager & m) :
     m_label_fid(m.get_label_family_id()),
     m_rwr(m, false, *this) {}
 
-label_rewriter::~label_rewriter() {}
-
 br_status label_rewriter::reduce_app(
     func_decl * f, unsigned num, expr * const * args, expr_ref & result, 
     proof_ref & result_pr) {
diff --git a/src/ast/rewriter/label_rewriter.h b/src/ast/rewriter/label_rewriter.h
index 8bec62ed6..a4720853c 100644
--- a/src/ast/rewriter/label_rewriter.h
+++ b/src/ast/rewriter/label_rewriter.h
@@ -27,7 +27,6 @@ class label_rewriter : public default_rewriter_cfg {
     rewriter_tpl<label_rewriter> m_rwr;
 public:    
     label_rewriter(ast_manager & m);
-    ~label_rewriter();
 
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, 
                          proof_ref & result_pr);
diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h
index cd89bb2f9..1afa19f84 100644
--- a/src/ast/rewriter/rewriter.h
+++ b/src/ast/rewriter/rewriter.h
@@ -346,8 +346,6 @@ public:
     ast_manager & m() const { return this->m_manager; }
     Config & cfg() { return m_cfg; }
     Config const & cfg() const { return m_cfg; }
-
-    ~rewriter_tpl() override {};
     
     void reset();
     void cleanup();
diff --git a/src/ast/simplifiers/reduce_args_simplifier.cpp b/src/ast/simplifiers/reduce_args_simplifier.cpp
index f9c788792..96607734b 100644
--- a/src/ast/simplifiers/reduce_args_simplifier.cpp
+++ b/src/ast/simplifiers/reduce_args_simplifier.cpp
@@ -375,8 +375,6 @@ public:
         m_bv(m)
     {}
 
-    ~reduce_args_simplifier() override {}
-
     char const* name() const override { return "reduce-args"; }
 
     void collect_statistics(statistics& st) const override {
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index 239fa73b6..abd79c515 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -31,8 +31,6 @@ rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx
     m_dt(m), m_dl(m), m_a(m), m_bv(m), m_ar(m), m_rec(m), 
     m_generate_proof(false), m_collected(false), m_is_monotone(true) {}
 
-rule_properties::~rule_properties() {}
-
 void rule_properties::collect(rule_set const& rules) {
     reset();
     m_collected = true;
diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h
index a7ef9a0de..3159c28a6 100644
--- a/src/muz/base/rule_properties.h
+++ b/src/muz/base/rule_properties.h
@@ -58,7 +58,6 @@ namespace datalog {
         bool check_accessor(app* n);
     public:
         rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& is_predicate);
-        ~rule_properties();    
         void set_generate_proof(bool generate_proof) { m_generate_proof = generate_proof; } 
         void collect(rule_set const& r);
         void check_quantifier_free();
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 913e35f36..e83569e0e 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -1443,8 +1443,6 @@ namespace datalog {
         m_rule_trace(ctx.get_rule_manager()) {
     }
 
-    bmc::~bmc() {}
-
     lbool bmc::query(expr* query) {
         m_solver = nullptr;
         m_answer = nullptr;
diff --git a/src/muz/bmc/dl_bmc_engine.h b/src/muz/bmc/dl_bmc_engine.h
index 90c4ab862..05d5707a6 100644
--- a/src/muz/bmc/dl_bmc_engine.h
+++ b/src/muz/bmc/dl_bmc_engine.h
@@ -51,8 +51,6 @@ namespace datalog {
     public:
         bmc(context& ctx);
 
-        ~bmc() override;
-
         lbool query(expr* query) override;
 
         void display_certificate(std::ostream& out) const override;
diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp
index 89ae71e36..9d4baa4ae 100644
--- a/src/muz/clp/clp_context.cpp
+++ b/src/muz/clp/clp_context.cpp
@@ -59,8 +59,6 @@ namespace datalog {
             m_fparams.m_mbqi = false;
         }
 
-        ~imp() {}        
-
         lbool query(expr* query) {
             m_ctx.ensure_opened();
             m_solver.reset();
diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
index cf759c76e..f4f946d09 100644
--- a/src/muz/ddnf/ddnf.cpp
+++ b/src/muz/ddnf/ddnf.cpp
@@ -78,8 +78,6 @@ namespace datalog {
             m_descendants(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq) {
         }
 
-        ~ddnf_node() {}
-
         unsigned inc_ref() {
             return ++m_refs;
         }
@@ -429,8 +427,6 @@ namespace datalog {
     class ddnfs {
         u_map<ddnf_mgr*> m_mgrs;
     public:
-        ddnfs() {}
-
         ~ddnfs() {
             u_map<ddnf_mgr*>::iterator it = m_mgrs.begin(), end = m_mgrs.end();
             for (; it != end; ++it) {
@@ -503,8 +499,6 @@ namespace datalog {
             m_inner_ctx.updt_params(params);
         }
 
-        ~imp() {}        
-
         lbool query(expr* query) {
             m_ctx.ensure_opened();
             rule_set& old_rules = m_ctx.get_rules();
diff --git a/src/muz/spacer/spacer_expand_bnd_generalizer.h b/src/muz/spacer/spacer_expand_bnd_generalizer.h
index 91ba3b417..6d4e68d17 100644
--- a/src/muz/spacer/spacer_expand_bnd_generalizer.h
+++ b/src/muz/spacer/spacer_expand_bnd_generalizer.h
@@ -43,7 +43,6 @@ class lemma_expand_bnd_generalizer : public lemma_generalizer {
 
   public:
     lemma_expand_bnd_generalizer(context &ctx);
-    ~lemma_expand_bnd_generalizer() override {}
 
     void operator()(lemma_ref &lemma) override;
 
diff --git a/src/muz/spacer/spacer_global_generalizer.h b/src/muz/spacer/spacer_global_generalizer.h
index 00b85ecd5..b7ee05757 100644
--- a/src/muz/spacer/spacer_global_generalizer.h
+++ b/src/muz/spacer/spacer_global_generalizer.h
@@ -161,7 +161,6 @@ class lemma_global_generalizer : public lemma_generalizer {
 
   public:
     lemma_global_generalizer(context &ctx);
-    ~lemma_global_generalizer() override {}
 
     void operator()(lemma_ref &lemma) override;
 
diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp
index f65661e9e..175c8aeb8 100644
--- a/src/muz/tab/tab_context.cpp
+++ b/src/muz/tab/tab_context.cpp
@@ -1354,8 +1354,6 @@ namespace datalog {
             m_fparams.m_mbqi = false;
         }
 
-        ~imp() {}
-
         lbool query(expr* query) {
             m_ctx.ensure_opened();
             m_index.reset();
diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.h b/src/muz/transforms/dl_mk_array_eq_rewrite.h
index 7f6a29bf3..eabef4792 100644
--- a/src/muz/transforms/dl_mk_array_eq_rewrite.h
+++ b/src/muz/transforms/dl_mk_array_eq_rewrite.h
@@ -40,7 +40,6 @@ namespace datalog {
      public:
         mk_array_eq_rewrite(context & ctx, unsigned priority);
         rule_set * operator()(rule_set const & source) override;
-        ~mk_array_eq_rewrite() override{}
     };
 
 
diff --git a/src/muz/transforms/dl_mk_array_instantiation.h b/src/muz/transforms/dl_mk_array_instantiation.h
index 0002f4ecd..71924288f 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.h
+++ b/src/muz/transforms/dl_mk_array_instantiation.h
@@ -112,7 +112,6 @@ namespace datalog {
      public:
         mk_array_instantiation(context & ctx, unsigned priority);
         rule_set * operator()(rule_set const & source) override;
-        ~mk_array_instantiation() override{}
     };
 
 
diff --git a/src/muz/transforms/dl_mk_backwards.cpp b/src/muz/transforms/dl_mk_backwards.cpp
index 5d124336b..5024d4631 100644
--- a/src/muz/transforms/dl_mk_backwards.cpp
+++ b/src/muz/transforms/dl_mk_backwards.cpp
@@ -27,8 +27,6 @@ namespace datalog {
         m(ctx.get_manager()),
         m_ctx(ctx) {        
     }
-
-    mk_backwards::~mk_backwards() { }
         
     rule_set * mk_backwards::operator()(rule_set const & source) {
         context& ctx = source.get_context();
diff --git a/src/muz/transforms/dl_mk_backwards.h b/src/muz/transforms/dl_mk_backwards.h
index 78a9d2fd0..4d1522e02 100644
--- a/src/muz/transforms/dl_mk_backwards.h
+++ b/src/muz/transforms/dl_mk_backwards.h
@@ -27,7 +27,6 @@ namespace datalog {
         context&     m_ctx;
     public:
         mk_backwards(context & ctx, unsigned priority = 33000);
-        ~mk_backwards() override;
         rule_set * operator()(rule_set const & source) override;
     };
 
diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp
index 439cb4540..0072f0078 100644
--- a/src/muz/transforms/dl_mk_bit_blast.cpp
+++ b/src/muz/transforms/dl_mk_bit_blast.cpp
@@ -146,8 +146,6 @@ namespace datalog {
             m_dst(nullptr)
         {}
 
-        ~expand_mkbv_cfg() {}
-
         void set_src(rule_set const* src) { m_src = src; }
         void set_dst(rule_set* dst) { m_dst = dst; }
         func_decl_ref_vector const& old_funcs() const { return m_old_funcs; }
diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp
index 753b82cea..98bd3c41a 100644
--- a/src/muz/transforms/dl_mk_elim_term_ite.cpp
+++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp
@@ -80,8 +80,6 @@ namespace datalog {
         rm(ctx.get_rule_manager()),
         m_ground(m) {}
 
-    mk_elim_term_ite::~mk_elim_term_ite() {}
-
     /**
        \brief map free variables in e to ground, fresh, constants
        m_ground is reset on every new rule so it is safe to assume
diff --git a/src/muz/transforms/dl_mk_elim_term_ite.h b/src/muz/transforms/dl_mk_elim_term_ite.h
index 98acd12f1..d42a7d773 100644
--- a/src/muz/transforms/dl_mk_elim_term_ite.h
+++ b/src/muz/transforms/dl_mk_elim_term_ite.h
@@ -35,7 +35,6 @@ namespace datalog {
         expr_ref ground(expr* e);
     public:
         mk_elim_term_ite(context &ctx, unsigned priority);
-        ~mk_elim_term_ite() override;
         rule_set * operator()(const rule_set &source) override;
     };
 }
diff --git a/src/muz/transforms/dl_mk_karr_invariants.cpp b/src/muz/transforms/dl_mk_karr_invariants.cpp
index 18d67f549..955c3ca92 100644
--- a/src/muz/transforms/dl_mk_karr_invariants.cpp
+++ b/src/muz/transforms/dl_mk_karr_invariants.cpp
@@ -58,8 +58,6 @@ namespace datalog {
             m_inner_ctx.updt_params(params);
     }
 
-    mk_karr_invariants::~mk_karr_invariants() { }
-
     void matrix::display_row(
         std::ostream& out, vector<rational> const& row, rational const& b, bool is_eq) {
         for (unsigned j = 0; j < row.size(); ++j) {
diff --git a/src/muz/transforms/dl_mk_karr_invariants.h b/src/muz/transforms/dl_mk_karr_invariants.h
index ac1015d14..9ba579a60 100644
--- a/src/muz/transforms/dl_mk_karr_invariants.h
+++ b/src/muz/transforms/dl_mk_karr_invariants.h
@@ -62,8 +62,6 @@ namespace datalog {
         rule_set* update_rules(rule_set const& src);
     public:
         mk_karr_invariants(context & ctx, unsigned priority);
-
-        ~mk_karr_invariants() override;
         
         rule_set * operator()(rule_set const & source) override;
 
diff --git a/src/muz/transforms/dl_mk_loop_counter.cpp b/src/muz/transforms/dl_mk_loop_counter.cpp
index 91aaa8d8b..a20224eb2 100644
--- a/src/muz/transforms/dl_mk_loop_counter.cpp
+++ b/src/muz/transforms/dl_mk_loop_counter.cpp
@@ -30,8 +30,6 @@ namespace datalog {
         m_refs(m) {        
     }
 
-    mk_loop_counter::~mk_loop_counter() { }
-
     app_ref mk_loop_counter::add_arg(rule_set const& src, rule_set& dst, app* fn, unsigned idx) {
         expr_ref_vector args(m);
         func_decl* new_fn, *old_fn = fn->get_decl();
diff --git a/src/muz/transforms/dl_mk_loop_counter.h b/src/muz/transforms/dl_mk_loop_counter.h
index 067945caf..b2758df67 100644
--- a/src/muz/transforms/dl_mk_loop_counter.h
+++ b/src/muz/transforms/dl_mk_loop_counter.h
@@ -35,7 +35,6 @@ namespace datalog {
         app_ref del_arg(app* fn);        
     public:
         mk_loop_counter(context & ctx, unsigned priority = 33000);
-        ~mk_loop_counter() override;
         
         rule_set * operator()(rule_set const & source) override;
 
diff --git a/src/muz/transforms/dl_mk_magic_symbolic.cpp b/src/muz/transforms/dl_mk_magic_symbolic.cpp
index 59529e630..afadfd6c3 100644
--- a/src/muz/transforms/dl_mk_magic_symbolic.cpp
+++ b/src/muz/transforms/dl_mk_magic_symbolic.cpp
@@ -63,8 +63,6 @@ namespace datalog {
         m(ctx.get_manager()),
         m_ctx(ctx) {        
     }
-
-    mk_magic_symbolic::~mk_magic_symbolic() { }
         
     rule_set * mk_magic_symbolic::operator()(rule_set const & source) {
         if (!m_ctx.magic()) {
diff --git a/src/muz/transforms/dl_mk_magic_symbolic.h b/src/muz/transforms/dl_mk_magic_symbolic.h
index 208f79f45..ac29194bc 100644
--- a/src/muz/transforms/dl_mk_magic_symbolic.h
+++ b/src/muz/transforms/dl_mk_magic_symbolic.h
@@ -29,7 +29,6 @@ namespace datalog {
         app_ref      mk_query(app* q);
     public:
         mk_magic_symbolic(context & ctx, unsigned priority = 33037);
-        ~mk_magic_symbolic() override;
         rule_set * operator()(rule_set const & source) override;
     };
 
diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 255c4f814..ef4428fa7 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -43,8 +43,6 @@ namespace mbp {
         imp(ast_manager& m) :
             m(m), a(m) {}
 
-        ~imp() {}
-
         void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
             rational w;
             if (ts.find(x, w))
diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp
index bf3ad08ed..fa7ec8cb5 100644
--- a/src/qe/mbp/mbp_arrays.cpp
+++ b/src/qe/mbp/mbp_arrays.cpp
@@ -1058,7 +1058,6 @@ namespace mbp {
         scoped_ptr<contains_app> m_var;
 
         imp(ast_manager& m): m(m), a(m), m_stores(m) {}
-        ~imp() {}
 
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
             return false;
diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp
index e5e5309f3..6ecaa5de2 100644
--- a/src/qe/mbp/mbp_term_graph.cpp
+++ b/src/qe/mbp/mbp_term_graph.cpp
@@ -187,8 +187,6 @@ class term {
         m_is_peq = is_partial_eq(to_app(m_expr));
     }
 
-    ~term() {}
-
     class parents {
         term const &t;
 
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 8a6f910bc..37cf62c61 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -558,7 +558,6 @@ namespace qe {
             vector<div>   m_divs;
         public:
             div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m), m_zero(a.mk_real(0), m) {}
-            ~div_rewriter_cfg() {}
             br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) {
                 rational r1, r(1);
                 if (a.is_div(f) && sz == 2 && a.is_numeral(args[0], r1) && a.is_numeral(args[1], r) && !r.is_zero()) {
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index a331bef8e..7393dc1bb 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -58,7 +58,6 @@ namespace sat {
                 m_stack(std::move(stack)) {
                 m_counter = ++counter;
             }
-            ~elim_stack() { }
             void inc_ref() { ++m_refcount; }
             void dec_ref() { if (0 == --m_refcount) { dealloc(this); } }
             elim_stackv const& stack() const { return m_stack; }
diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp
index cbbf01b20..5b7542cb2 100644
--- a/src/sat/sat_mus.cpp
+++ b/src/sat/sat_mus.cpp
@@ -24,8 +24,6 @@ Notes:
 namespace sat {
 
     mus::mus(solver& s):s(s), m_is_active(false), m_max_num_restarts(UINT_MAX) {}
-
-    mus::~mus() {}
    
     void mus::reset() {
         m_core.reset();
diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h
index 5f67f6acd..672e90185 100644
--- a/src/sat/sat_mus.h
+++ b/src/sat/sat_mus.h
@@ -30,7 +30,6 @@ namespace sat {
 
     public:
         mus(solver& s);
-        ~mus();        
         lbool operator()();
         bool is_active() const { return m_is_active; }
         model const& get_model() const { return m_model; }
diff --git a/src/sat/smt/arith_sls.h b/src/sat/smt/arith_sls.h
index 55d39b252..a65ca686d 100644
--- a/src/sat/smt/arith_sls.h
+++ b/src/sat/smt/arith_sls.h
@@ -153,7 +153,6 @@ namespace arith {
 
     public:
         sls(solver& s);
-        ~sls() override {}
         void set(sat::ddfw* d);
         void init_search() override;
         void finish_search() override;
diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp
index 7a8f31f1e..1343577d9 100644
--- a/src/sat/smt/array_solver.cpp
+++ b/src/sat/smt/array_solver.cpp
@@ -88,8 +88,6 @@ namespace array {
         m_constraint->initialize(m_constraint.get(), this);
     }
 
-    solver::~solver() {}
-
     sat::check_result solver::check() {
         force_push();
         // flet<bool> _is_redundant(m_is_redundant, true);
diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index 8dc6e4e84..0a7c854fd 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -268,7 +268,6 @@ namespace array {
         void validate_extensionality(euf::enode* s, euf::enode* t) const;
     public:
         solver(euf::solver& ctx, theory_id id);
-        ~solver() override;
         bool is_external(bool_var v) override { return false; }
         void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override {}
         void asserted(literal l) override {}
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index 34f876be6..ee8d6fb19 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -103,8 +103,6 @@ namespace intblast {
 
     public:
         solver(euf::solver& ctx);
-        
-        ~solver() override {}
 
         lbool check_axiom(sat::literal_vector const& lits);
         lbool check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp
index f251d01ae..b77a38927 100644
--- a/src/smt/arith_eq_adapter.cpp
+++ b/src/smt/arith_eq_adapter.cpp
@@ -67,8 +67,6 @@ namespace smt {
             m_ge(ge) {
         }
 
-        ~arith_eq_relevancy_eh() override {}
-
         void operator()(relevancy_propagator & rp) override {
             if (!rp.is_relevant(m_n1))
                 return;
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 4139b3109..7a567d5a9 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -223,8 +223,6 @@ namespace smt {
                 m_sort(s) {
             }
 
-            ~node() {}
-
             unsigned get_id() const { return m_id; }
 
             sort* get_sort() const { return m_sort; }
diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h
index f6e3c4659..8dea2842f 100644
--- a/src/smt/smt_relevancy.h
+++ b/src/smt/smt_relevancy.h
@@ -48,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;
     };
     
@@ -61,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_seq.h b/src/smt/theory_seq.h
index 6ed4fc41f..d469097d8 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -134,7 +134,6 @@ namespace smt {
             unsigned_vector                   m_limit;
         public:
             exclusion_table(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {}
-            ~exclusion_table() { }
             bool empty() const { return m_table.empty(); }
             void update(expr* e, expr* r);
             bool contains(expr* e, expr* r) const;
diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp
index ed645dae0..8995049f0 100644
--- a/src/solver/simplifier_solver.cpp
+++ b/src/solver/simplifier_solver.cpp
@@ -38,7 +38,6 @@ class simplifier_solver : public solver {
         model_reconstruction_trail m_reconstruction_trail;
         bool m_updated = false;
         dep_expr_state(simplifier_solver& s) :dependent_expr_state(s.m), s(s), m_reconstruction_trail(s.m, m_trail) {}
-        ~dep_expr_state() override {}
         unsigned qtail() const override { return s.m_fmls.size(); }
         dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; }
         void update(unsigned i, dependent_expr const& j) override { 
diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index 605a32ae1..31c4ad9f3 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -28,8 +28,6 @@ solver_na2as::solver_na2as(ast_manager & m):
     m_assumptions(m) {
 }
 
-solver_na2as::~solver_na2as() {}
-
 void solver_na2as::assert_expr_core2(expr * t, expr * a) {
     if (a == nullptr) {
         assert_expr_core(t);
diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h
index 81a58fb39..fd0a7dc5e 100644
--- a/src/solver/solver_na2as.h
+++ b/src/solver/solver_na2as.h
@@ -30,7 +30,6 @@ class solver_na2as : public solver {
     void restore_assumptions(unsigned old_sz);
 public:
     solver_na2as(ast_manager & m);
-    ~solver_na2as() override;
 
     void assert_expr_core2(expr * t, expr * a) override;
 
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index c791841ec..31ca836ac 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -79,8 +79,6 @@ class nla2bv_tactic : public tactic {
             m_default_bv_size = m_num_bits = p.get_uint("nla2bv_bv_size", 4);
         }
 
-        ~imp() {}
-
         void updt_params(params_ref const& p)  {} 
         
         void operator()(goal & g, model_converter_ref & mc) {
diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp
index f6db3c30e..93491f7b2 100644
--- a/src/tactic/bv/bv_bound_chk_tactic.cpp
+++ b/src/tactic/bv/bv_bound_chk_tactic.cpp
@@ -41,8 +41,6 @@ struct bv_bound_chk_rewriter_cfg : public default_rewriter_cfg {
     bv_bound_chk_rewriter_cfg(ast_manager & m, bv_bound_chk_stats& stats)
         : m_m(m), m_b_rw(m), m_stats(stats) {}
 
-    ~bv_bound_chk_rewriter_cfg() {}
-
     void updt_params(params_ref const & _p) {
         rewriter_params p(_p);
         m_bv_ineq_consistency_test_max = p.bv_ineq_consistency_test_max();        
@@ -146,8 +144,6 @@ public:
     imp(ast_manager & m, params_ref const & p, bv_bound_chk_stats& stats)
         : m_rw(m, p, stats) {    }
 
-    virtual ~imp() = default;
-
     ast_manager& m() { return m_rw.m(); }
 
     void operator()(goal_ref const & g) {
@@ -164,7 +160,7 @@ public:
         m_rw.m_cfg.cleanup();
     }
 
-    virtual void updt_params(params_ref const & p) {
+    void updt_params(params_ref const & p) {
         m_rw.updt_params(p);
     }
 
diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index 5f856800e..6ddc49c7f 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -48,8 +48,6 @@ namespace {
             r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false");
         }
 
-        ~bv_bounds_simplifier() override {}
-
         bool assert_expr(expr * t, bool sign) override {
             return assert_expr_core(t, sign);
         }
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index aa4358e9c..e3cd7893a 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -144,9 +144,8 @@ struct ctx_simplify_tactic::imp {
     };
 
     struct cache_cell {
-        expr *          m_from;
-        cached_result * m_result;
-        cache_cell():m_from(nullptr), m_result(nullptr) {}
+        expr *          m_from = nullptr;
+        cached_result * m_result = nullptr;
     };
 
     ast_manager &               m;
diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index 9ad12d504..c5cba0b9a 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -117,8 +117,6 @@ public:
         m_replace = mk_default_expr_replacer(m, false);
     }
 
-    ~imp() {}
-
     void operator()(goal & g) {
         if (g.inconsistent())
             return;        
@@ -202,10 +200,10 @@ private:
     // a |-> c1, b |-> c2 <c1,c2> |-> c
     // 
     struct u_pair {
-        unsigned m_first;
-        unsigned m_second;
+        unsigned m_first = 0;
+        unsigned m_second = 0;
         u_pair(unsigned f, unsigned s) : m_first(f), m_second(s) {}
-        u_pair(): m_first(0), m_second(0) {}
+        u_pair() = default;
 
         struct hash {
             unsigned operator()(u_pair const& p) const {
@@ -324,8 +322,6 @@ private:
     class parents {
         app_parents m_use_funs;        
     public:
-        parents() {}
-
         app_parents const& get_parents() { return m_use_funs; }
 
         void operator()(app* n) {
diff --git a/src/tactic/probe.h b/src/tactic/probe.h
index 4d1af66a8..452f2cb70 100644
--- a/src/tactic/probe.h
+++ b/src/tactic/probe.h
@@ -40,10 +40,9 @@ public:
     };
 
 private:
-    unsigned m_ref_count;
+    unsigned m_ref_count = 0;
 
 public:
-    probe():m_ref_count(0) {}
     virtual ~probe() = default;
 
     void inc_ref() { ++m_ref_count; }
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 179a42ab8..f7dcfb3ea 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -146,8 +146,6 @@ tactic * mk_trace_tactic(char const * tag) {
 
 class fail_if_undecided_tactic : public skip_tactic {
 public:
-    fail_if_undecided_tactic() {}
-
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         if (!in->is_decided()) 
             throw tactic_exception("undecided");
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 652bf8130..e62f93ecf 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -32,10 +32,8 @@ class progress_callback;
 typedef ptr_buffer<goal> goal_buffer;
 
 class tactic : public user_propagator::core {
-    unsigned m_ref_count;
+    unsigned m_ref_count = 0;
 public:
-    tactic():m_ref_count(0) {}
-
     void inc_ref() { m_ref_count++; }
     void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
 
diff --git a/src/util/chashtable.h b/src/util/chashtable.h
index 394e5998c..da7cb5b31 100644
--- a/src/util/chashtable.h
+++ b/src/util/chashtable.h
@@ -609,7 +609,7 @@ public:
     struct key_value {
         Key    m_key;
         Value  m_value;
-        key_value() {}
+        key_value() = default;
         key_value(Key const & k):m_key(k) {}
         key_value(Key const & k, Value const & v):m_key(k), m_value(v) {}
     };
diff --git a/src/util/optional.h b/src/util/optional.h
index 8e515f4be..c2a0fd3ef 100644
--- a/src/util/optional.h
+++ b/src/util/optional.h
@@ -30,7 +30,7 @@ class optional {
     }
 
 public:
-    optional() {}
+    optional() = default;
 
     explicit optional(const T & val) {
         m_obj = alloc(T, val);
@@ -116,13 +116,13 @@ public:
  */
 template<typename T>
 class optional<T*> {
-    T * m_ptr;
+    T * m_ptr = nullptr;
 
     static optional m_undef;
 
 public:
     
-    optional():m_ptr(nullptr) {}
+    optional() = default;
 
     explicit optional(T * val):m_ptr(val) {}
 
diff --git a/src/util/params.cpp b/src/util/params.cpp
index 700a53109..3440673b7 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -366,12 +366,11 @@ class params {
     };
     typedef std::pair<symbol, value> entry;
     svector<entry>        m_entries;
-    std::atomic<unsigned> m_ref_count;
+    std::atomic<unsigned> m_ref_count = 0;
     void del_value(entry & e);
     void del_values();
 
 public:
-    params():m_ref_count(0) {}
     ~params() {
         reset();
     }
diff --git a/src/util/queue.h b/src/util/queue.h
index 059dea573..771ebbcd4 100644
--- a/src/util/queue.h
+++ b/src/util/queue.h
@@ -23,13 +23,10 @@ Notes:
 template<class T>
 class queue {
     vector<T> m_elems;
-    unsigned  m_head;
-    unsigned  m_capacity;
+    unsigned  m_head = 0;
+    unsigned  m_capacity = 0;
     
 public:
-    
-    queue(): m_head(0), m_capacity(0) {}
-
     void push(T const& t) { m_elems.push_back(t); }
 
     bool empty() const { 
diff --git a/src/util/rational.h b/src/util/rational.h
index e9924bca7..61569f40c 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -41,8 +41,8 @@ public:
       ADD_INITIALIZER('rational::initialize();')
       ADD_FINALIZER('rational::finalize();')
     */
-    rational() {}
-    
+    rational() = default;
+
     rational(rational const & r) { m().set(m_val, r.m_val); }
     rational(rational&&) = default;
 
diff --git a/src/util/s_integer.h b/src/util/s_integer.h
index 6ddd2bf67..b102d6d4b 100644
--- a/src/util/s_integer.h
+++ b/src/util/s_integer.h
@@ -21,7 +21,7 @@ Revision History:
 #include "util/rational.h"
 
 class s_integer {
-    int m_val;
+    int m_val = 0;
     static s_integer m_zero;
     static s_integer m_one;
     static s_integer m_minus_one;
@@ -41,7 +41,7 @@ public:
     std::string to_string() const;
 
 public:
-    s_integer(): m_val(0) {}
+    s_integer() = default;
     explicit s_integer(int n):m_val(n) {}
     struct i64 {};
     explicit s_integer(int64_t i, i64):m_val(static_cast<int>(i)) {}
diff --git a/src/util/small_object_allocator.h b/src/util/small_object_allocator.h
index 05fe32ef0..646a203c1 100644
--- a/src/util/small_object_allocator.h
+++ b/src/util/small_object_allocator.h
@@ -29,9 +29,8 @@ class small_object_allocator {
     static const unsigned NUM_SLOTS      = (SMALL_OBJ_SIZE >> PTR_ALIGNMENT);
     struct chunk {
         chunk* m_next{ nullptr };
-        char* m_curr{ nullptr };
+        char* m_curr = m_data;
         char    m_data[CHUNK_SIZE];
-        chunk():m_curr(m_data) {}
     };
     chunk *     m_chunks[NUM_SLOTS];
     void  *     m_free_list[NUM_SLOTS];
diff --git a/src/util/vector.h b/src/util/vector.h
index 31ced7f4b..79e51d545 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -1170,7 +1170,7 @@ public:
 template<typename T>
 class ptr_vector : public vector<T *, false> {
 public:
-    ptr_vector():vector<T *, false>() {}
+    ptr_vector() = default;
     ptr_vector(unsigned s):vector<T *, false>(s) {}
     ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
     ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
@@ -1190,7 +1190,7 @@ public:
 template<typename T, typename SZ = unsigned>
 class svector : public vector<T, false, SZ> {
 public:
-    svector():vector<T, false, SZ>() {}
+    svector() = default;
     svector(SZ s):vector<T, false, SZ>(s) {}
     svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
     svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}