diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 67a605869ca..8e2cbef827b 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -34,9 +34,6 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
         m_nums(m_amanager) {
     }
 
-    ~algebraic_numbers_wrapper() {
-    }
-
     unsigned mk_id(algebraic_numbers::anum const & val) {
         SASSERT(!m_amanager.is_rational(val));
         unsigned idx = m_id_gen.mk();
diff --git a/src/ast/ast_trail.h b/src/ast/ast_trail.h
index 5a76dd537a4..18c8961e61b 100644
--- a/src/ast/ast_trail.h
+++ b/src/ast/ast_trail.h
@@ -33,8 +33,7 @@ class ast2ast_trailmap {
 public:
     ast2ast_trailmap(ast_manager& m):
         m_domain(m),
-        m_range(m), 
-        m_map()
+        m_range(m)
     {}
 
     bool find(S* s, T*& t) {
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index cc5c6eb75e7..e5ab4a8066c 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -1040,11 +1040,6 @@ namespace datatype {
         return m_family_id;
     }
 
-
-    util::~util() {
-        
-    }
-
     ptr_vector<func_decl> const * util::get_datatype_constructors(sort * ty) {
         SASSERT(is_datatype(ty));
         ptr_vector<func_decl> * r = nullptr;
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index ca33b48c1f3..dcca7897060 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -338,7 +338,6 @@ namespace datatype {
 
     public:
         util(ast_manager & m);
-        ~util();
         ast_manager & get_manager() const { return m; }
         // sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params); 
         bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); }
diff --git a/src/ast/expr2polynomial.cpp b/src/ast/expr2polynomial.cpp
index a69d5b43680..3bcd7367a50 100644
--- a/src/ast/expr2polynomial.cpp
+++ b/src/ast/expr2polynomial.cpp
@@ -504,9 +504,6 @@ default_expr2polynomial::default_expr2polynomial(ast_manager & am, polynomial::m
     expr2polynomial(am, pm, nullptr) {
 }
 
-default_expr2polynomial::~default_expr2polynomial() {
-}
-
 bool default_expr2polynomial::is_int(polynomial::var x) const {
     return m_is_int[x];
 }
diff --git a/src/ast/expr2polynomial.h b/src/ast/expr2polynomial.h
index 1d89587c454..b3356e9e08d 100644
--- a/src/ast/expr2polynomial.h
+++ b/src/ast/expr2polynomial.h
@@ -102,7 +102,6 @@ class default_expr2polynomial : public expr2polynomial {
     bool_vector m_is_int;
 public:
     default_expr2polynomial(ast_manager & am, polynomial::manager & pm);
-    ~default_expr2polynomial() override;
     bool is_int(polynomial::var x) const override;
 protected:
     polynomial::var mk_var(bool is_int) override;
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index 42467c21929..f68de5e32d5 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -36,9 +36,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
 
     fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p);
 
-    ~fpa2bv_rewriter_cfg() {
-    }
-
     void cleanup_buffers() {
         m_out.finalize();
     }
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 76e44278db1..3bdc19d5e01 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -47,9 +47,6 @@ void fpa_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_bv_plugin = static_cast<bv_decl_plugin*>(m_manager->get_plugin(m_bv_fid));
 }
 
-fpa_decl_plugin::~fpa_decl_plugin() {
-}
-
 unsigned fpa_decl_plugin::mk_id(mpf const & v) {
     unsigned new_id = m_id_gen.mk();
     m_values.reserve(new_id+1);
@@ -961,9 +958,6 @@ fpa_util::fpa_util(ast_manager & m):
     m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m_fid));
 }
 
-fpa_util::~fpa_util() {
-}
-
 sort * fpa_util::mk_float_sort(unsigned ebits, unsigned sbits) {
     parameter ps[2] = { parameter(ebits), parameter(sbits) };
     return m().mk_sort(m_fid, FLOATING_POINT_SORT, 2, ps);
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index 0357efa4705..39b3fc33c46 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -175,7 +175,6 @@ class fpa_decl_plugin : public decl_plugin {
     bool is_float_sort(sort * s) const { return is_sort_of(s, m_family_id, FLOATING_POINT_SORT); }
     bool is_rm_sort(sort * s) const { return is_sort_of(s, m_family_id, ROUNDING_MODE_SORT); }
 
-    ~fpa_decl_plugin() override;
     void finalize() override;
 
     decl_plugin * mk_fresh() override;
@@ -216,7 +215,6 @@ class fpa_util {
 
 public:
     fpa_util(ast_manager & m);
-    ~fpa_util();
 
     ast_manager & m() const { return m_manager; }
     mpf_manager & fm() const { return m_plugin->fm(); }
diff --git a/src/ast/macros/cond_macro.h b/src/ast/macros/cond_macro.h
index 7e8064ac675..0dc3c1e0b9d 100644
--- a/src/ast/macros/cond_macro.h
+++ b/src/ast/macros/cond_macro.h
@@ -39,10 +39,7 @@ class cond_macro {
         m_weight(weight) {
         SASSERT(!m_hint || !m_cond);
     }
-    
-    ~cond_macro() {
-    }
-    
+
     func_decl * get_f() const { return m_f; }
     
     expr * get_def() const { return m_def; }
diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp
index bc63aae8e10..3006e383ca9 100644
--- a/src/ast/macros/macro_finder.cpp
+++ b/src/ast/macros/macro_finder.cpp
@@ -269,9 +269,6 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
     m_autil(m) {
 }
 
-macro_finder::~macro_finder() {
-}
-
 bool macro_finder::expand_macros(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps,  expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     TRACE("macro_finder", tout << "starting expand_macros:\n";
           m_macro_manager.display(tout););
diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h
index 91e5deeb9c4..fe27221722e 100644
--- a/src/ast/macros/macro_finder.h
+++ b/src/ast/macros/macro_finder.h
@@ -43,7 +43,6 @@ class macro_finder {
 
 public:
     macro_finder(ast_manager & m, macro_manager & mm);
-    ~macro_finder();
     void operator()(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
     void operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
 };
diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index b7c94b1b5f7..824573d46be 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -41,9 +41,6 @@ macro_manager::macro_manager(ast_manager & m):
     m_util.set_forbidden_set(&m_forbidden_set);
 }
 
-macro_manager::~macro_manager() {
-}
-
 void macro_manager::push_scope() {
     m_scopes.push_back(scope());
     scope & s              = m_scopes.back();
diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h
index 758e3c1a7ee..9d8831c309f 100644
--- a/src/ast/macros/macro_manager.h
+++ b/src/ast/macros/macro_manager.h
@@ -64,7 +64,6 @@ class macro_manager {
 
 public:
     macro_manager(ast_manager & m);
-    ~macro_manager();
     void copy_to(macro_manager& dst);
     ast_manager & get_manager() const { return m; }
     macro_util & get_util() { return m_util; }
diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index dff36278d74..b65daf06310 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -31,9 +31,6 @@ quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) :
   m_new_qsorts(m) {
 }
 
-quasi_macros::~quasi_macros() {
-}
-
 void quasi_macros::find_occurrences(expr * e) {
     unsigned j;
     m_todo.reset();
diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index 4441f432eb3..2b5350cf0b7 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -60,7 +60,6 @@ class quasi_macros {
 
 public:
     quasi_macros(ast_manager & m, macro_manager & mm);
-    ~quasi_macros();
 
     /**
        \brief Find pure function macros and apply them.
diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp
index c931c6fad51..4e9ee626305 100644
--- a/src/ast/normal_forms/defined_names.cpp
+++ b/src/ast/normal_forms/defined_names.cpp
@@ -57,7 +57,7 @@ struct defined_names::impl {
     unsigned_vector m_lims;          //!< Backtracking support.
 
     impl(ast_manager & m, char const * prefix);
-    virtual ~impl();
+    virtual ~impl() = default;
 
     app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
     void cache_new_name(expr * e, app * name);
@@ -90,9 +90,6 @@ defined_names::impl::impl(ast_manager & m, char const * prefix):
         m_z3name = prefix;
 }
 
-defined_names::impl::~impl() {
-}
-
 /**
    \brief Given an expression \c e that may contain free variables, return an application (sk x_1 ... x_n),
    where sk is a fresh variable name, and x_i's are the free variables of \c e.
diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp
index 8ae0dcbf267..2fbd99bdf61 100644
--- a/src/ast/pattern/expr_pattern_match.cpp
+++ b/src/ast/pattern/expr_pattern_match.cpp
@@ -41,9 +41,6 @@ expr_pattern_match::expr_pattern_match(ast_manager & manager):
     m_manager(manager), m_precompiled(manager) {        
 }
 
-expr_pattern_match::~expr_pattern_match() {
-}
-
 bool 
 expr_pattern_match::match_quantifier(quantifier* qf, app_ref_vector& patterns, unsigned& weight) {
     if (m_regs.empty()) {
diff --git a/src/ast/pattern/expr_pattern_match.h b/src/ast/pattern/expr_pattern_match.h
index 2fd0b4b73c9..11939e1de44 100644
--- a/src/ast/pattern/expr_pattern_match.h
+++ b/src/ast/pattern/expr_pattern_match.h
@@ -116,7 +116,6 @@ class expr_pattern_match {
 
  public:
     expr_pattern_match(ast_manager & manager);
-    ~expr_pattern_match();
     bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight);
     bool match_quantifier_index(quantifier* qf, app_ref_vector & patterns, unsigned& index);
     unsigned initialize(quantifier* qf);
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index 5f2534a5107..cba1932be77 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -366,9 +366,6 @@ namespace recfun {
           m_plugin(dynamic_cast<decl::plugin*>(m.get_plugin(m_fid))) {
     }
 
-    util::~util() {
-    }
-
     def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range, bool is_generated) {
         return alloc(def, m(), m_fid, name, n, domain, range, is_generated);
     }
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 73e2b5244f8..d9fe07dcf32 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -237,7 +237,6 @@ namespace recfun {
 
     public:
         util(ast_manager &m);
-        ~util();
 
         ast_manager & m() { return m_manager; }
         family_id get_family_id() const { return m_fid; }
diff --git a/src/ast/sls/bvsls_opt_engine.cpp b/src/ast/sls/bvsls_opt_engine.cpp
index 7dc71cd8cdf..2f006dc9f9a 100644
--- a/src/ast/sls/bvsls_opt_engine.cpp
+++ b/src/ast/sls/bvsls_opt_engine.cpp
@@ -28,10 +28,6 @@ bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) :
     m_best_model = alloc(model, m);
 }
 
-bvsls_opt_engine::~bvsls_opt_engine()
-{    
-}
-
 bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
     expr_ref const & objective, 
     model_ref initial_model, 
diff --git a/src/ast/sls/bvsls_opt_engine.h b/src/ast/sls/bvsls_opt_engine.h
index 435fa3af483..25182c15624 100644
--- a/src/ast/sls/bvsls_opt_engine.h
+++ b/src/ast/sls/bvsls_opt_engine.h
@@ -31,7 +31,6 @@ class bvsls_opt_engine : public sls_engine {
 
 public:
     bvsls_opt_engine(ast_manager & m, params_ref const & p);
-    ~bvsls_opt_engine();
 
     class optimization_result {
     public:
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index e9ca5595fb7..5f5195bb9da 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -2464,9 +2464,6 @@ cmd_context::dt_eh::dt_eh(cmd_context & owner):
     m_dt_util(owner.m()) {
 }
 
-cmd_context::dt_eh::~dt_eh() {
-}
-
 void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
     TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";);
     for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 6dc60c9dd96..cd43203a7fc 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -305,7 +305,6 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     public:
         void reset() { m_dt_util.reset(); }
         dt_eh(cmd_context & owner);
-        ~dt_eh() override;
         void operator()(sort * dt, pdecl* pd) override;
     };
 
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index a0805110bf4..b2b858b07ea 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -27,7 +27,6 @@ Module Name:
 #include "ast/ast_smt2_pp.h"
 #include "tactic/tactic.h"
 #include "tactic/tactical.h"
-#include "tactic/probe.h"
 #include "solver/check_sat_result.h"
 #include "cmd_context/cmd_context_to_goal.h"
 #include "cmd_context/echo_tactic.h"
@@ -38,9 +37,6 @@ probe_info::probe_info(symbol const & n, char const * d, probe * p):
     m_probe(p) {
 }
 
-probe_info::~probe_info() {
-}
-
 class declare_tactic_cmd : public cmd {
     symbol           m_name;
     sexpr *          m_decl;
diff --git a/src/cmd_context/tactic_cmds.h b/src/cmd_context/tactic_cmds.h
index 5096ae9629b..de5fda0a867 100644
--- a/src/cmd_context/tactic_cmds.h
+++ b/src/cmd_context/tactic_cmds.h
@@ -18,12 +18,12 @@ Module Name:
 #pragma once
 
 #include "ast/ast.h"
+#include "tactic/probe.h"
 #include "util/params.h"
 #include "util/cmd_context_types.h"
 #include "util/ref.h"
 
 class tactic;
-class probe;
 
 typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&);
 
@@ -52,7 +52,6 @@ class probe_info {
     ref<probe>       m_probe;
 public:
     probe_info(symbol const & n, char const * d, probe * p);
-    ~probe_info();
 
     symbol get_name() const { return m_name; }
     char const * get_descr() const { return m_descr; }
diff --git a/src/math/lp/core_solver_pretty_printer.cpp b/src/math/lp/core_solver_pretty_printer.cpp
index 18bef83030f..65a9aef974f 100644
--- a/src/math/lp/core_solver_pretty_printer.cpp
+++ b/src/math/lp/core_solver_pretty_printer.cpp
@@ -21,7 +21,5 @@ Revision History:
 #include "math/lp/core_solver_pretty_printer_def.h"
 template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out);
 template void lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::print();
-template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::~core_solver_pretty_printer();
 template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> > &, std::ostream & out);
-template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::~core_solver_pretty_printer();
 template void lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::print();
diff --git a/src/math/lp/core_solver_pretty_printer.h b/src/math/lp/core_solver_pretty_printer.h
index 5bf29d511db..c9ab997606c 100644
--- a/src/math/lp/core_solver_pretty_printer.h
+++ b/src/math/lp/core_solver_pretty_printer.h
@@ -66,7 +66,6 @@ class core_solver_pretty_printer {
 
     void init_costs();
 
-    ~core_solver_pretty_printer();
     void init_rs_width();
 
     T current_column_norm();
diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h
index cbe67ea36a1..6d35273af7f 100644
--- a/src/math/lp/core_solver_pretty_printer_def.h
+++ b/src/math/lp/core_solver_pretty_printer_def.h
@@ -67,8 +67,6 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_co
     
 }
 
-template <typename T, typename X> core_solver_pretty_printer<T, X>::~core_solver_pretty_printer() {
-}
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_rs_width() {
     m_rs_width = static_cast<unsigned>(T_to_string(m_core_solver.get_cost()).size());
     for (unsigned i = 0; i < nrows(); i++) {
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index b546df706ac..6cdd735a15d 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -121,9 +121,6 @@ namespace algebraic_numbers {
             m_y = pm().mk_var();
         }
 
-        ~imp() {
-        }
-
         bool acell_inv(algebraic_cell const& c) {
             auto s = upm().eval_sign_at(c.m_p_sz, c.m_p, lower(&c));
             return s == sign_zero || c.m_sign_lower == (s == sign_neg);
diff --git a/src/math/realclosure/mpz_matrix.cpp b/src/math/realclosure/mpz_matrix.cpp
index 3bbd387c675..701b3b26dae 100644
--- a/src/math/realclosure/mpz_matrix.cpp
+++ b/src/math/realclosure/mpz_matrix.cpp
@@ -36,9 +36,6 @@ mpz_matrix_manager::mpz_matrix_manager(unsynch_mpz_manager & nm, small_object_al
     m_allocator(a) {
 }
 
-mpz_matrix_manager::~mpz_matrix_manager() {
-}
-
 void mpz_matrix_manager::mk(unsigned m, unsigned n, mpz_matrix & A) {
     SASSERT(m > 0 && n > 0);
     del(A);
diff --git a/src/math/realclosure/mpz_matrix.h b/src/math/realclosure/mpz_matrix.h
index 91fe226816b..9eb051ed220 100644
--- a/src/math/realclosure/mpz_matrix.h
+++ b/src/math/realclosure/mpz_matrix.h
@@ -63,7 +63,6 @@ class mpz_matrix_manager {
     bool solve_core(mpz_matrix const & A, mpz * b, bool int_solver);
 public:
     mpz_matrix_manager(unsynch_mpz_manager & nm, small_object_allocator & a);
-    ~mpz_matrix_manager();
     unsynch_mpz_manager & nm() const { return m_nm; }
     void mk(unsigned m, unsigned n, mpz_matrix & A);
     void del(mpz_matrix & r);
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index ecea560a515..561d6a6d7c2 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -410,8 +410,6 @@ namespace realclosure {
             sbuffer<unsigned>  m_szs;        // size of each polynomial in the sequence
         public:
             scoped_polynomial_seq(imp & m):m_seq_coeffs(m) {}
-            ~scoped_polynomial_seq() {
-            }
 
             /**
                \brief Add a new polynomial to the sequence.
diff --git a/src/model/numeral_factory.cpp b/src/model/numeral_factory.cpp
index ba19ec94176..6f7aeeb2cd3 100644
--- a/src/model/numeral_factory.cpp
+++ b/src/model/numeral_factory.cpp
@@ -28,9 +28,6 @@ arith_factory::arith_factory(ast_manager & m):
     m_util(m) {
 }
 
-arith_factory::~arith_factory() {
-}
-
 app * arith_factory::mk_num_value(rational const & val, bool is_int) {
     return numeral_factory::mk_value(val, is_int ? m_util.mk_int() : m_util.mk_real());
 }
@@ -40,9 +37,6 @@ bv_factory::bv_factory(ast_manager & m):
     m_util(m) {
 }
 
-bv_factory::~bv_factory() {
-}
-
 app * bv_factory::mk_value_core(rational const & val, sort * s) {
     return m_util.mk_numeral(val, s);
 }
diff --git a/src/model/numeral_factory.h b/src/model/numeral_factory.h
index 174ea8757c0..ca917d9273d 100644
--- a/src/model/numeral_factory.h
+++ b/src/model/numeral_factory.h
@@ -34,7 +34,6 @@ class arith_factory : public numeral_factory {
 
 public:
     arith_factory(ast_manager & m);
-    ~arith_factory() override;
 
     app * mk_num_value(rational const & val, bool is_int);
 };
@@ -46,7 +45,6 @@ class bv_factory : public numeral_factory {
 
 public:
     bv_factory(ast_manager & m);
-    ~bv_factory() override;
 
     app * mk_num_value(rational const & val, unsigned bv_size);
 };
diff --git a/src/model/value_factory.cpp b/src/model/value_factory.cpp
index 30fa82caf57..c799191992b 100644
--- a/src/model/value_factory.cpp
+++ b/src/model/value_factory.cpp
@@ -25,9 +25,6 @@ value_factory::value_factory(ast_manager & m, family_id fid):
     m_fid(fid) {
 }
 
-value_factory::~value_factory() {
-}
-
 basic_factory::basic_factory(ast_manager & m, unsigned seed):
     value_factory(m, m.get_basic_family_id()), m_rand(seed) {
 }
diff --git a/src/model/value_factory.h b/src/model/value_factory.h
index 20c383efec6..85515495b8f 100644
--- a/src/model/value_factory.h
+++ b/src/model/value_factory.h
@@ -31,7 +31,7 @@ class value_factory {
 public:
     value_factory(ast_manager & m, family_id fid);
 
-    virtual ~value_factory();
+    virtual ~value_factory() = default;
 
     /**
        \brief Return some value of the given sort. The result is always different from zero.
diff --git a/src/muz/base/bind_variables.cpp b/src/muz/base/bind_variables.cpp
index 5ac41e0bf45..d96a49f6799 100644
--- a/src/muz/base/bind_variables.cpp
+++ b/src/muz/base/bind_variables.cpp
@@ -25,9 +25,6 @@ bind_variables::bind_variables(ast_manager & m):
     m_vars(m),
     m_pinned(m)
 {}
-
-bind_variables::~bind_variables() {
-}
     
 expr_ref bind_variables::operator()(expr* fml, bool is_forall) {
     if (m_vars.empty()) {
diff --git a/src/muz/base/bind_variables.h b/src/muz/base/bind_variables.h
index e231b70396c..4c183b50771 100644
--- a/src/muz/base/bind_variables.h
+++ b/src/muz/base/bind_variables.h
@@ -40,7 +40,6 @@ class bind_variables {
     expr_ref abstract(expr* fml, cache_t& cache, unsigned scope);
 public:
     bind_variables(ast_manager & m);
-    ~bind_variables();
     
     expr_ref operator()(expr* fml, bool is_forall);
 
diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index a15c8060907..c6df500d8b9 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -267,9 +267,6 @@ class dlexer {
         next();
     }
 
-    dlexer() {
-    }
-
     void set_stream(std::istream* s, char_reader* r) { 
         m_input = s; 
         m_reader = r;
diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp
index 24b109f35d1..454f6d8bc59 100644
--- a/src/muz/rel/check_relation.cpp
+++ b/src/muz/rel/check_relation.cpp
@@ -150,8 +150,6 @@ namespace datalog {
         m(rm.get_context().get_manager()),
         m_base(nullptr) {
     }
-    check_relation_plugin::~check_relation_plugin() {
-    }
     check_relation& check_relation_plugin::get(relation_base& r) {
         return dynamic_cast<check_relation&>(r);
     }
diff --git a/src/muz/rel/check_relation.h b/src/muz/rel/check_relation.h
index b0b4a8acc4a..773b45813fc 100644
--- a/src/muz/rel/check_relation.h
+++ b/src/muz/rel/check_relation.h
@@ -89,7 +89,6 @@ namespace datalog {
             unsigned_vector const& cols1, unsigned_vector const& cols2);
     public:
         check_relation_plugin(relation_manager& rm);
-        ~check_relation_plugin() override;
         void set_plugin(relation_plugin* p) { m_base = p; }
 
         bool can_handle_signature(const relation_signature & s) override;
diff --git a/src/muz/rel/dl_external_relation.cpp b/src/muz/rel/dl_external_relation.cpp
index a47b0719f83..a2e42f64024 100644
--- a/src/muz/rel/dl_external_relation.cpp
+++ b/src/muz/rel/dl_external_relation.cpp
@@ -34,9 +34,6 @@ namespace datalog {
     {
     }
 
-    external_relation::~external_relation() {
-    }
-
     void external_relation::mk_accessor(decl_kind k, func_decl_ref& fn, const relation_fact& f, bool destructive, expr_ref& res) const {
         ast_manager& m = m_rel.get_manager();
         family_id fid = get_plugin().get_family_id();
diff --git a/src/muz/rel/dl_external_relation.h b/src/muz/rel/dl_external_relation.h
index 17e9a236462..c8887eeedbd 100644
--- a/src/muz/rel/dl_external_relation.h
+++ b/src/muz/rel/dl_external_relation.h
@@ -122,7 +122,6 @@ namespace datalog {
         void mk_accessor(decl_kind k, func_decl_ref& fn, const relation_fact& f, bool destructive, expr_ref& res) const;
 
         external_relation(external_relation_plugin & p, const relation_signature & s, expr* r);
-        ~external_relation() override;
 
     public:
         external_relation_plugin & get_plugin() const;
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index a4b7045974a..2d22e34a9fe 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -631,9 +631,6 @@ namespace datalog {
         );
     }
 
-    mk_explanations::~mk_explanations() {
-    }
-
     func_decl * mk_explanations::get_union_decl(context & ctx) {
         ast_manager & m = ctx.get_manager();
         sort_ref s(ctx.get_decl_util().mk_rule_sort(), m);
diff --git a/src/muz/rel/dl_mk_explanations.h b/src/muz/rel/dl_mk_explanations.h
index 5491918de69..33d5cc8eea0 100644
--- a/src/muz/rel/dl_mk_explanations.h
+++ b/src/muz/rel/dl_mk_explanations.h
@@ -65,8 +65,6 @@ namespace datalog {
         */
         mk_explanations(context & ctx);
 
-        ~mk_explanations() override;
-
         /**
            \brief Return explanation predicate that corresponds to \c orig_decl.
         */
diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index 30b57f2a49b..824b298b437 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -38,9 +38,6 @@ namespace datalog {
         m_rewriter.updt_params(m_params);
     }
 
-    mk_array_blast::~mk_array_blast() {
-    }
-
     bool mk_array_blast::is_store_def(expr* e, expr*& x, expr*& y) {
         if (m.is_eq(e, x, y)) {
             if (!a.is_store(y)) {
diff --git a/src/muz/transforms/dl_mk_array_blast.h b/src/muz/transforms/dl_mk_array_blast.h
index 352c8a24886..12102af73e3 100644
--- a/src/muz/transforms/dl_mk_array_blast.h
+++ b/src/muz/transforms/dl_mk_array_blast.h
@@ -64,8 +64,6 @@ namespace datalog {
            \brief Create rule transformer that removes array stores and selects by ackermannization.
         */
         mk_array_blast(context & ctx, unsigned priority);
-
-        ~mk_array_blast() override;
         
         rule_set * operator()(rule_set const & source) override;
 
diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
index b8a68a443da..6b321bc752d 100644
--- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
@@ -149,9 +149,6 @@ namespace datalog {
         m_mc(nullptr) {
     }
 
-    mk_quantifier_abstraction::~mk_quantifier_abstraction() {
-    }
-
     func_decl* mk_quantifier_abstraction::declare_pred(rule_set const& rules, rule_set& dst, func_decl* old_p) {
 
         if (rules.is_output_predicate(old_p)) {
diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.h b/src/muz/transforms/dl_mk_quantifier_abstraction.h
index 6cf546a503f..33c70c08b20 100644
--- a/src/muz/transforms/dl_mk_quantifier_abstraction.h
+++ b/src/muz/transforms/dl_mk_quantifier_abstraction.h
@@ -49,8 +49,6 @@ namespace datalog {
 
     public:
         mk_quantifier_abstraction(context & ctx, unsigned priority);
-
-        ~mk_quantifier_abstraction() override;
         
         rule_set * operator()(rule_set const & source) override;
     };
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index 61c395b4e04..d1fb6400cf7 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
@@ -41,9 +41,6 @@ namespace datalog {
         m_cnst2var(m) {        
     }
 
-    mk_quantifier_instantiation::~mk_quantifier_instantiation() {        
-    }
-
     void mk_quantifier_instantiation::extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs) {
         conjs.reset();
         qs.reset();
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.h b/src/muz/transforms/dl_mk_quantifier_instantiation.h
index 5c0c28cd4da..716de11f025 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.h
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.h
@@ -60,8 +60,6 @@ namespace datalog {
     public:
         mk_quantifier_instantiation(context & ctx, unsigned priority);
 
-        ~mk_quantifier_instantiation() override;
-        
         rule_set * operator()(rule_set const & source) override;
     };
 
diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp
index 38305a04e3b..54cf22ea85e 100644
--- a/src/muz/transforms/dl_mk_scale.cpp
+++ b/src/muz/transforms/dl_mk_scale.cpp
@@ -110,9 +110,6 @@ namespace datalog {
         m_eqs(m) {
     }
 
-    mk_scale::~mk_scale() {
-    }
-
     rule_set * mk_scale::operator()(rule_set const & source) {
         if (!m_ctx.scale()) {
             return nullptr;
diff --git a/src/muz/transforms/dl_mk_scale.h b/src/muz/transforms/dl_mk_scale.h
index a8e42f17ed7..fcbf4c2265f 100644
--- a/src/muz/transforms/dl_mk_scale.h
+++ b/src/muz/transforms/dl_mk_scale.h
@@ -42,7 +42,6 @@ namespace datalog {
         app_ref mk_constraint(unsigned num_vars, app* q);
     public:
         mk_scale(context & ctx, unsigned priority = 33039);
-        ~mk_scale() override;
         rule_set * operator()(rule_set const & source) override;
     };
 
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index a188206b430..cda44bdd436 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -156,9 +156,6 @@ namespace nlsat {
             m_minimize_cores   = false;
             m_signed_project   = false;
         }
-        
-        ~imp() {
-        }
 
         std::ostream& display(std::ostream & out, polynomial_ref const & p) const {
             m_pm.display(out, p, m_solver.display_proc());
diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp
index 76a310f00f9..872266f5fbe 100644
--- a/src/nlsat/nlsat_interval_set.cpp
+++ b/src/nlsat/nlsat_interval_set.cpp
@@ -112,9 +112,6 @@ namespace nlsat {
         m_am(m),
         m_allocator(a) {
     }
-     
-    interval_set_manager::~interval_set_manager() {
-    }
     
     void interval_set_manager::del(interval_set * s) {
         if (s == nullptr)
diff --git a/src/nlsat/nlsat_interval_set.h b/src/nlsat/nlsat_interval_set.h
index 2e74f33c623..297318912c6 100644
--- a/src/nlsat/nlsat_interval_set.h
+++ b/src/nlsat/nlsat_interval_set.h
@@ -33,7 +33,6 @@ namespace nlsat {
         void del(interval_set * s);
     public:
         interval_set_manager(anum_manager & m, small_object_allocator & a);
-        ~interval_set_manager();
         
         void set_seed(unsigned s) { m_rand.set_seed(s); }
 
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index aff1301e079..c059494399a 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -58,9 +58,6 @@ namespace opt {
     }
 
     unsigned opt_solver::m_dump_count = 0;
-    
-    opt_solver::~opt_solver() {
-    }
 
     void opt_solver::updt_params(params_ref const & _p) {
         opt_params p(_p);
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 66835df489d..e614a54fcf6 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -85,7 +85,6 @@ namespace opt {
         bool                m_was_unknown;
     public:
         opt_solver(ast_manager & m, params_ref const & p, generic_model_converter& fm);
-        ~opt_solver() override;
 
         solver* translate(ast_manager& m, params_ref const& p) override;
         void updt_params(params_ref const& p) override;
diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp
index 82802819db2..e7cdf9476b0 100644
--- a/src/opt/pb_sls.cpp
+++ b/src/opt/pb_sls.cpp
@@ -123,9 +123,6 @@ namespace smt {
             one = mpz(1);
         }
 
-        ~imp() {
-        }
-
         void reset() {
             init_max_flips();
             m_non_greedy_percent = 30;
diff --git a/src/parsers/util/simple_parser.cpp b/src/parsers/util/simple_parser.cpp
index 6c3303e5c49..c039fd9a19c 100644
--- a/src/parsers/util/simple_parser.cpp
+++ b/src/parsers/util/simple_parser.cpp
@@ -28,9 +28,6 @@ simple_parser::simple_parser(ast_manager & m):
     m_exprs(m) {
 }
 
-simple_parser::~simple_parser() {
-}
-
 void simple_parser::add_builtin_op(symbol const & s, family_id fid, decl_kind kind) {
     SASSERT(!m_builtin.contains(s));
     SASSERT(!m_vars.contains(s));
diff --git a/src/parsers/util/simple_parser.h b/src/parsers/util/simple_parser.h
index b40a0d98305..c3cc0712e0f 100644
--- a/src/parsers/util/simple_parser.h
+++ b/src/parsers/util/simple_parser.h
@@ -45,7 +45,7 @@ class simple_parser {
     expr * parse_expr(scanner & s);
 public:
     simple_parser(ast_manager & m);
-    virtual ~simple_parser();
+    virtual ~simple_parser() = default;
     void add_builtin_op(symbol const & s, family_id fid, decl_kind kind);
     void add_builtin_op(char const * str, family_id fid, decl_kind kind);
     void add_var(symbol const & s, var * v);
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 6e5d3fae392..92b4f7f5c2e 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -353,9 +353,6 @@ namespace sat {
         DEBUG_CODE(verify_unsat_stack(););
     }
 
-    local_search::local_search() {
-    }
-
     void local_search::reinit(solver& s, bool_vector const& phase) {
         import(s, true);
         for (unsigned i = phase.size(); i-- > 0; )
@@ -419,10 +416,6 @@ namespace sat {
         if (_init) 
             init();        
     }
-    
-    local_search::~local_search() {
-    }
-    
 
     lbool local_search::check() {
         return check(0, nullptr, nullptr);
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index b6223452285..e8959478e1e 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -227,10 +227,6 @@ namespace sat {
         unsigned num_vars() const { return m_vars.size() - 1; }     // var index from 1 to num_vars
 
     public:
-
-        local_search();
-
-        ~local_search() override;
         
         reslimit& rlimit() override { return m_limit; }
 
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index ddb277e9b23..fa5720ede26 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -23,13 +23,6 @@ Revision History:
 
 namespace sat {
 
-    model_converter::model_converter(): m_exposed_lim(0), m_solver(nullptr) {
-    }
-
-    model_converter::~model_converter() {
-    }
-
-
     model_converter& model_converter::operator=(model_converter const& other) {
         copy(other);
         return *this;
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index 7393dc1bb28..170886aa690 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -79,9 +79,9 @@ namespace sat {
         };
     private:
         vector<entry>          m_entries;           // entries accumulated during SAT search
-        unsigned               m_exposed_lim;       // last entry that was exposed to model converter.
+        unsigned               m_exposed_lim = 0;   // last entry that was exposed to model converter.
         bool_vector            m_mark;              // literals that are used in asserted clauses.
-        solver const*          m_solver;
+        solver const*          m_solver = nullptr;
         elim_stackv            m_elim_stack;
 
         void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const;
@@ -95,8 +95,6 @@ namespace sat {
         void add_elim_stack(entry & e);
 
     public:
-        model_converter();
-        ~model_converter();
         void set_solver(solver const* s) { m_solver = s; }
         void operator()(model & m) const;
         model_converter& operator=(model_converter const& other);
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index 42cda4bfb3c..c001ee90f94 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -296,9 +296,6 @@ namespace euf {
         add_plugin(alloc(bv::theory_checker, m));
     }
 
-    theory_checker::~theory_checker() {
-    }
-
     void theory_checker::add_plugin(theory_checker_plugin* p) {
         m_plugins.push_back(p);
         p->register_plugins(*this);
diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h
index d84e4d19fae..0da57ee9ee4 100644
--- a/src/sat/smt/euf_proof_checker.h
+++ b/src/sat/smt/euf_proof_checker.h
@@ -45,7 +45,6 @@ namespace euf {
         void add_plugin(theory_checker_plugin* p);
     public:
         theory_checker(ast_manager& m);
-        ~theory_checker();
         void register_plugin(symbol const& rule, theory_checker_plugin*);
         bool check(expr* jst);
         expr_ref_vector clause(expr* jst);
diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
index 1c356f9f22f..0fa35cfd425 100644
--- a/src/sat/smt/q_mam.cpp
+++ b/src/sat/smt/q_mam.cpp
@@ -2000,9 +2000,6 @@ namespace q {
             m_args.resize(INIT_ARGS_SIZE);
         }
 
-        ~interpreter() {
-        }
-
         void init(code_tree * t) {
             TRACE("mam_bug", tout << "preparing to match tree:\n" << *t << "\n";);
             m_registers.reserve(t->get_num_regs(), nullptr);
diff --git a/src/sat/smt/specrel_solver.cpp b/src/sat/smt/specrel_solver.cpp
index d59029e6bc3..064e1990491 100644
--- a/src/sat/smt/specrel_solver.cpp
+++ b/src/sat/smt/specrel_solver.cpp
@@ -32,9 +32,6 @@ namespace specrel {
         ctx.get_egraph().add_plugin(alloc(euf::specrel_plugin, ctx.get_egraph()));
     }
 
-    solver::~solver() {
-    }
-
     void solver::asserted(sat::literal l) {
 
     }
diff --git a/src/sat/smt/specrel_solver.h b/src/sat/smt/specrel_solver.h
index 9ebb769160c..51e383bad53 100644
--- a/src/sat/smt/specrel_solver.h
+++ b/src/sat/smt/specrel_solver.h
@@ -39,7 +39,6 @@ namespace specrel {
         
     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 {}
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index a10c243f84f..71eeb55cb56 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1995,9 +1995,6 @@ namespace {
             m_args.resize(INIT_ARGS_SIZE);
         }
 
-        ~interpreter() {
-        }
-
         void init(code_tree * t) {
             TRACE("mam_bug", tout << "preparing to match tree:\n" << *t << "\n";);
             m_registers.reserve(t->get_num_regs(), nullptr);
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index 52399abb6e1..81d41eeee29 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -43,9 +43,6 @@ namespace smt {
         m_vals.resize(15, 0.0f);
     }
 
-    qi_queue::~qi_queue() {
-    }
-
     void qi_queue::setup() {
         TRACE("qi_cost", tout << "qi_cost: " << m_params.m_qi_cost << "\n";);
         if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) {
diff --git a/src/smt/qi_queue.h b/src/smt/qi_queue.h
index bdf4bd50ecf..961dd73e010 100644
--- a/src/smt/qi_queue.h
+++ b/src/smt/qi_queue.h
@@ -80,7 +80,6 @@ namespace smt {
 
     public:
         qi_queue(quantifier_manager & qm, context & ctx, qi_params & params);
-        ~qi_queue();
         void setup();
         /**
            \brief Insert a new quantifier in the queue, f contains the quantifier and bindings.
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 7932434738f..90877a96320 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -52,9 +52,6 @@ namespace smt {
     {
     }
 
-    conflict_resolution::~conflict_resolution() {
-    }
-
     /**
        \brief Mark all enodes in a 'proof' tree branch starting at n
        n -> ... -> root
diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h
index cf707bd310f..87ad197718f 100644
--- a/src/smt/smt_conflict_resolution.h
+++ b/src/smt/smt_conflict_resolution.h
@@ -208,7 +208,7 @@ namespace smt {
                             vector<watch_list> & watches
                             );
 
-        virtual ~conflict_resolution();
+        virtual ~conflict_resolution() = default;
 
         virtual bool resolve(b_justification conflict, literal not_l);
 
diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index 0c876e8bc26..86f1c114176 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -177,9 +177,6 @@ namespace smt {
         m_lazy(true) {
     }
 
-    theory::~theory() {
-    }
-
     smt_params const& theory::get_fparams() const { 
         return ctx.get_fparams();
     }
diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index 416d626f738..74dfe8aa2c1 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -388,7 +388,7 @@ namespace smt {
 
     public:
         theory(context& ctx, family_id fid);
-        virtual ~theory();
+        virtual ~theory() = default;
         
         virtual void setup() {}
 
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index e68f0f53fd5..e2bc5e7a4f8 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -1054,7 +1054,6 @@ namespace smt {
         // -----------------------------------
     public:
         theory_arith(context& ctx);
-        ~theory_arith() override;
         
         theory * mk_fresh(context * new_ctx) override;
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 8a2d9f3c9bd..e4f788f60ef 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1737,10 +1737,6 @@ namespace smt {
         m_bound_watch(null_bool_var) {
     }
 
-    template<typename Ext>
-    theory_arith<Ext>::~theory_arith() {
-    }
-
     template<typename Ext>
     theory* theory_arith<Ext>::mk_fresh(context* new_ctx) {
         return alloc(theory_arith<Ext>, *new_ctx);
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 5740285a2ea..b1fe47b6574 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1493,9 +1493,6 @@ namespace smt {
         m_bb.set_flat_and_or(false);
     }
 
-    theory_bv::~theory_bv() {
-    }
-
     theory* theory_bv::mk_fresh(context* new_ctx) {
         return alloc(theory_bv, *new_ctx);
     }
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index 72775c1d353..0a7d4bbb25b 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -268,7 +268,6 @@ namespace smt {
         typedef std::pair<enode*, unsigned> var_enode_pos;
         
         theory_bv(context& ctx);
-        ~theory_bv() override;
         
         theory * mk_fresh(context * new_ctx) override;
 
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index b794a44b5c7..3302199a29b 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -762,8 +762,7 @@ namespace smt {
         m_util(m),
         m_autil(m),
         m_sutil(m),
-        m_find(*this),
-        m_trail_stack() {
+        m_find(*this) {
     }
 
     theory_datatype::~theory_datatype() {
diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp
index ee94ac3555b..94a5edc5913 100644
--- a/src/solver/assertions/asserted_formulas.cpp
+++ b/src/solver/assertions/asserted_formulas.cpp
@@ -89,10 +89,6 @@ void asserted_formulas::setup() {
         m_smt_params.m_relevancy_lemma = false;
 }
 
-
-asserted_formulas::~asserted_formulas() {
-}
-
 void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_expr>& result) {
     if (inconsistent()) {
         return;
diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h
index 481af58b737..643cbc04611 100644
--- a/src/solver/assertions/asserted_formulas.h
+++ b/src/solver/assertions/asserted_formulas.h
@@ -254,7 +254,6 @@ class asserted_formulas {
 
 public:
     asserted_formulas(ast_manager & m, smt_params & smtp, params_ref const& p);
-    ~asserted_formulas();
     void finalize();
 
     void updt_params(params_ref const& p);
diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp
index fd7939d9503..944f717b998 100644
--- a/src/solver/check_sat_result.cpp
+++ b/src/solver/check_sat_result.cpp
@@ -58,9 +58,6 @@ simple_check_sat_result::simple_check_sat_result(ast_manager & m):
     m_proof(m) {
     }
 
-simple_check_sat_result::~simple_check_sat_result() {
-}
-
 void simple_check_sat_result::collect_statistics(statistics & st) const { 
     st.copy(m_stats); 
 }
diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h
index 2269a14449a..b992d260da1 100644
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -98,7 +98,6 @@ struct simple_check_sat_result : public check_sat_result {
     std::string     m_unknown;
     
     simple_check_sat_result(ast_manager & m);
-    ~simple_check_sat_result() override;
     ast_manager& get_manager() const override { return m_proof.get_manager(); }
     void collect_statistics(statistics & st) const override;
     void get_unsat_core(expr_ref_vector & r) override;
diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp
index e4071628cdf..640c412773a 100644
--- a/src/tactic/core/injectivity_tactic.cpp
+++ b/src/tactic/core/injectivity_tactic.cpp
@@ -162,9 +162,6 @@ class injectivity_tactic : public tactic {
         rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) {
         }
 
-        ~rewriter_eq_cfg() {
-        }
-
         void cleanup_buffers() {
         }
 
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index ee5cd0f73c9..6e2068e26e2 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -31,9 +31,6 @@ struct simplify_tactic::imp {
         m_num_steps(0) {
     }
 
-    ~imp() {
-    }
-
     ast_manager & m() const { return m_manager; }
 
 
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
index 8c20a4cdac8..e48934b5b85 100644
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
@@ -89,10 +89,6 @@ hwf_manager::hwf_manager() :
     // to the precision (not sure about the rounding modes though).
 }
 
-hwf_manager::~hwf_manager()
-{
-}
-
 uint64_t RAW(double X) { uint64_t tmp; memcpy(&tmp, &(X), sizeof(uint64_t)); return tmp; }
 double DBL(uint64_t X) { double tmp; memcpy(&tmp, &(X), sizeof(double)); return tmp; }
 
diff --git a/src/util/hwf.h b/src/util/hwf.h
index 209a8fe77a9..92696393784 100644
--- a/src/util/hwf.h
+++ b/src/util/hwf.h
@@ -46,7 +46,6 @@ class hwf_manager {
 public:
     typedef hwf numeral;
     hwf_manager();
-    ~hwf_manager();
 
     void reset(hwf & o) { set(o, 0); }
     void set(hwf & o, int value);
diff --git a/src/util/map.h b/src/util/map.h
index 0068be31b1b..fb72db01f7b 100644
--- a/src/util/map.h
+++ b/src/util/map.h
@@ -24,19 +24,6 @@ template<typename Key, typename Value>
 struct _key_data {
     Key   m_key;
     Value m_value;
-    _key_data() {
-    }
-    _key_data(Key const & k):
-        m_key(k) {
-    }
-    _key_data(Key const & k, Value const & v):
-        m_key(k),
-        m_value(v) {
-    }
-    _key_data(Key const& k, Value&& v):
-        m_key(k),
-        m_value(std::move(v)) {
-    }
 };
 
 template<typename Entry, typename HashProc, typename EqProc>
@@ -108,27 +95,27 @@ class table2map {
     }
     
     void insert(key const & k, value const & v) {
-        m_table.insert(key_data(k, v));
+        m_table.insert(key_data{k, v});
     }
 
     void insert(key const& k, value&& v) {
-        m_table.insert(key_data(k, std::move(v)));
+        m_table.insert(key_data{k, std::move(v)});
     }
   
     bool insert_if_not_there_core(key const & k, value const & v, entry *& et) {
-        return m_table.insert_if_not_there_core(key_data(k,v), et);
+        return m_table.insert_if_not_there_core(key_data{k,v}, et);
     }
 
     value & insert_if_not_there(key const & k, value const & v) {
-        return m_table.insert_if_not_there2(key_data(k, v))->get_data().m_value;
+        return m_table.insert_if_not_there2(key_data{k, v})->get_data().m_value;
     }
     
     entry * insert_if_not_there3(key const & k, value const & v) {
-        return m_table.insert_if_not_there2(key_data(k, v));
+        return m_table.insert_if_not_there2(key_data{k, v});
     }
         
     entry * find_core(key const & k) const {
-        return m_table.find_core(key_data(k));
+        return m_table.find_core(key_data{k});
     }
 
     bool find(key const & k, value & v) const {
@@ -150,7 +137,7 @@ class table2map {
     }
         
     iterator find_iterator(key const & k) const { 
-        return m_table.find(key_data(k));
+        return m_table.find(key_data{k});
     }
     
     value const & find(key const& k) const {
@@ -175,7 +162,7 @@ class table2map {
     }
 
     void remove(key const & k) {
-        m_table.remove(key_data(k));
+        m_table.remove(key_data{k});
     }
     
     void erase(key const & k) {
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index dbb2b776ebb..2784439a8a8 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -60,7 +60,7 @@ class obj_map {
         Value  m_value;
         key_data() = default;
         key_data(Key * k):
-            m_key(k), m_value() {
+            m_key(k) {
         }
         key_data(Key * k, Value const & v):
             m_key(k),
diff --git a/src/util/ref.h b/src/util/ref.h
index 849e23b38cc..22e51b783fc 100644
--- a/src/util/ref.h
+++ b/src/util/ref.h
@@ -21,7 +21,7 @@ Revision History:
 
 template<typename T>
 class ref {
-    T * m_ptr;
+    T * m_ptr = nullptr;
 
     void inc_ref() {
         if (m_ptr) {
@@ -36,9 +36,7 @@ class ref {
     }
 
 public:
-    ref():
-        m_ptr(nullptr) {
-    }
+    ref() = default;
 
     ref(T * ptr):
         m_ptr(ptr) {
@@ -50,9 +48,9 @@ class ref {
         inc_ref();
     }
 
-   ref (ref && r) noexcept : m_ptr(nullptr) {
-       std::swap(m_ptr, r.m_ptr);
-   }
+    ref(ref && r) noexcept {
+        std::swap(m_ptr, r.m_ptr);
+    }
 
     ~ref() {
         dec_ref();