diff --git a/src/ast/converters/expr_inverter.h b/src/ast/converters/expr_inverter.h
index e57820f35..6f46d9c51 100644
--- a/src/ast/converters/expr_inverter.h
+++ b/src/ast/converters/expr_inverter.h
@@ -35,7 +35,7 @@ protected:
 
 public:
     iexpr_inverter(ast_manager& m): m(m) {}
-    virtual ~iexpr_inverter() {}
+    virtual ~iexpr_inverter() = default;
     virtual void set_is_var(std::function<bool(expr*)>& is_var) { m_is_var = is_var; }
     virtual void set_model_converter(generic_model_converter* mc) { m_mc = mc; }
     virtual void set_produce_proofs(bool p) { m_produce_proofs = true; }
diff --git a/src/ast/euf/euf_plugin.h b/src/ast/euf/euf_plugin.h
index 5f56e1a17..ba6b2d5f9 100644
--- a/src/ast/euf/euf_plugin.h
+++ b/src/ast/euf/euf_plugin.h
@@ -39,7 +39,7 @@ namespace euf {
             g(g)
         {}
 
-        virtual ~plugin() {}
+        virtual ~plugin() = default;
 
         virtual theory_id get_id() const = 0;
 
diff --git a/src/ast/rewriter/bv2int_translator.h b/src/ast/rewriter/bv2int_translator.h
index 97b8b76b8..d8d3b7f59 100644
--- a/src/ast/rewriter/bv2int_translator.h
+++ b/src/ast/rewriter/bv2int_translator.h
@@ -18,7 +18,7 @@ Author:
 
 class bv2int_translator_trail {
 public:
-    virtual ~bv2int_translator_trail() {}
+    virtual ~bv2int_translator_trail() = default;
     virtual void push(push_back_vector<expr_ref_vector> const& c) = 0;
     virtual void push(push_back_vector<ptr_vector<app>> const& c) = 0;
     virtual void push_idx(set_vector_idx_trail<expr_ref_vector> const& c) = 0;
diff --git a/src/ast/simplifiers/bv_bounds_simplifier.cpp b/src/ast/simplifiers/bv_bounds_simplifier.cpp
index 72010c507..e1f4f2817 100644
--- a/src/ast/simplifiers/bv_bounds_simplifier.cpp
+++ b/src/ast/simplifiers/bv_bounds_simplifier.cpp
@@ -25,8 +25,7 @@ public:
         updt_params(p);
     }
     
-    ~dom_bv_bounds_simplifier() override {
-    }
+    ~dom_bv_bounds_simplifier() override = default;
     
     void updt_params(params_ref const & p) override {
         m_propagate_eq = p.get_bool("propagate_eq", false);
diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index 047dc4652..f30671bef 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -66,7 +66,7 @@ class dependent_expr_state {
     };
 public:
     dependent_expr_state(ast_manager& m) : m_frozen_trail(m) {}
-    virtual ~dependent_expr_state() {}
+    virtual ~dependent_expr_state() = default;
     unsigned qhead() const { return m_qhead; }
     virtual unsigned qtail() const = 0;
     virtual dependent_expr const& operator[](unsigned i) = 0;
@@ -227,7 +227,7 @@ protected:
     proof* tr(proof* a, proof* b) { return m.mk_transitivity(a, b); }
 public:
     dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s), m_trail(s.m_trail) {}
-    virtual ~dependent_expr_simplifier() {}
+    virtual ~dependent_expr_simplifier() = default;
     virtual char const* name() const = 0;
     virtual void push() { }
     virtual void pop(unsigned n) { }
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 1c33b63ba..9bbf5bbb3 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -140,9 +140,6 @@ namespace euf {
 
     }
 
-    completion::~completion() {
-    }
-
     bool completion::should_stop() {
         return
             !m.inc() ||
diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h
index ecf258986..2e8424a2a 100644
--- a/src/ast/simplifiers/euf_completion.h
+++ b/src/ast/simplifiers/euf_completion.h
@@ -226,7 +226,7 @@ namespace euf {
         bool is_gt(expr* a, expr* b) const;
     public:
         completion(ast_manager& m, dependent_expr_state& fmls);
-        ~completion() override;
+        ~completion() override = default;
         char const* name() const override { return "euf-completion"; }
         void push() override;
         void pop(unsigned n) override;
diff --git a/src/ast/simplifiers/extract_eqs.h b/src/ast/simplifiers/extract_eqs.h
index b88a3e8a5..0035bde87 100644
--- a/src/ast/simplifiers/extract_eqs.h
+++ b/src/ast/simplifiers/extract_eqs.h
@@ -40,7 +40,7 @@ namespace euf {
 
     class extract_eq {
     public:
-        virtual ~extract_eq() {}
+        virtual ~extract_eq() = default;
         virtual void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) = 0;
         virtual void pre_process(dependent_expr_state& fmls) {}
         virtual void updt_params(params_ref const& p) {}
diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index 1e9c484af..4d5c948d9 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -32,9 +32,6 @@
 
 namespace sat {
 
-    ddfw::~ddfw() {
-    }
-
     lbool ddfw::check(unsigned sz, literal const* assumptions) {
         init(sz, assumptions);   
         if (m_plugin)
diff --git a/src/ast/sls/sat_ddfw.h b/src/ast/sls/sat_ddfw.h
index 81bbb6fbe..73db66e03 100644
--- a/src/ast/sls/sat_ddfw.h
+++ b/src/ast/sls/sat_ddfw.h
@@ -35,7 +35,7 @@ namespace sat {
 
     class local_search_plugin {
     public:
-        virtual ~local_search_plugin() {}
+        virtual ~local_search_plugin() = default;
         virtual void on_rescale() = 0;
         virtual lbool on_save_model() = 0;
         virtual void on_restart() = 0;
@@ -225,7 +225,7 @@ namespace sat {
 
         ddfw() {}
 
-        ~ddfw();
+        ~ddfw() = default;
 
         void set_plugin(local_search_plugin* p) { m_plugin = p; }
 
diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
index 481d66b74..18d496dff 100644
--- a/src/ast/sls/sls_arith_base.h
+++ b/src/ast/sls/sls_arith_base.h
@@ -348,7 +348,7 @@ namespace sls {
         bool update_num(var_t v, num_t const& delta);
     public:
         arith_base(context& ctx);
-        ~arith_base() override {}        
+        ~arith_base() override = default;
         void register_term(expr* e) override;
         bool set_value(expr* e, expr* v) override;
         expr_ref get_value(expr* e) override;
diff --git a/src/ast/sls/sls_arith_plugin.h b/src/ast/sls/sls_arith_plugin.h
index 15dca5b4e..6b18714e3 100644
--- a/src/ast/sls/sls_arith_plugin.h
+++ b/src/ast/sls/sls_arith_plugin.h
@@ -29,7 +29,7 @@ namespace sls {
         void init_backup();
     public:
         arith_plugin(context& ctx);
-        ~arith_plugin() override {}
+        ~arith_plugin() override = default;
         void register_term(expr* e) override;
         expr_ref get_value(expr* e) override;
         void start_propagation() override;
diff --git a/src/ast/sls/sls_array_plugin.h b/src/ast/sls/sls_array_plugin.h
index 8bc3de45a..9726672dd 100644
--- a/src/ast/sls/sls_array_plugin.h
+++ b/src/ast/sls/sls_array_plugin.h
@@ -115,7 +115,7 @@ namespace sls {
         
     public:
         array_plugin(context& ctx);
-        ~array_plugin() override {}
+        ~array_plugin() override = default;
         void register_term(expr* e) override { if (a.is_array(e->get_sort())) m_has_arrays = true; }
         expr_ref get_value(expr* e) override;
         void initialize() override { m_g = nullptr; }
diff --git a/src/ast/sls/sls_basic_plugin.h b/src/ast/sls/sls_basic_plugin.h
index 1c263884e..600ec3b30 100644
--- a/src/ast/sls/sls_basic_plugin.h
+++ b/src/ast/sls/sls_basic_plugin.h
@@ -36,7 +36,7 @@ namespace sls {
             plugin(ctx) { 
             m_fid = basic_family_id;
         }
-        ~basic_plugin() override {}
+        ~basic_plugin() override = default;
         void register_term(expr* e) override;
         expr_ref get_value(expr* e) override;
         void initialize() override;
diff --git a/src/ast/sls/sls_bv_plugin.h b/src/ast/sls/sls_bv_plugin.h
index 4ad2df806..fd983a8fd 100644
--- a/src/ast/sls/sls_bv_plugin.h
+++ b/src/ast/sls/sls_bv_plugin.h
@@ -38,7 +38,7 @@ namespace sls {
 
     public:
         bv_plugin(context& ctx);
-        ~bv_plugin() override {}
+        ~bv_plugin() override = default;
         void register_term(expr* e) override;
         expr_ref get_value(expr* e) override;
         void start_propagation() override;
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index 4178c9d05..577dc46ee 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -38,7 +38,7 @@ namespace sls {
         family_id m_fid;
     public:
         plugin(context& c);
-        virtual ~plugin() {}
+        virtual ~plugin() = default;
         virtual family_id fid() { return m_fid; }
         virtual void register_term(expr* e) = 0;
         virtual expr_ref get_value(expr* e) = 0;
@@ -65,7 +65,7 @@ namespace sls {
 
     class sat_solver_context {
     public:
-        virtual ~sat_solver_context() {}
+        virtual ~sat_solver_context() = default;
         virtual vector<sat::clause_info> const& clauses() const = 0;
         virtual sat::clause_info const& get_clause(unsigned idx) const = 0;
         virtual ptr_iterator<unsigned> get_use_list(sat::literal lit) = 0;
diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index b2b6baa2c..91419cc1d 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -91,8 +91,6 @@ namespace sls {
         m_eval(m) {
         m_fid = dt.get_family_id();
     }
-    
-    datatype_plugin::~datatype_plugin() {}
 
     void datatype_plugin::collect_path_axioms() {
         expr* t = nullptr, *z = nullptr;
diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h
index 5c0310e43..395654385 100644
--- a/src/ast/sls/sls_datatype_plugin.h
+++ b/src/ast/sls/sls_datatype_plugin.h
@@ -81,7 +81,7 @@ namespace sls {
 
     public:
         datatype_plugin(context& c);
-        ~datatype_plugin() override;
+        ~datatype_plugin() override = default;
         family_id fid() override { return m_fid; }
         expr_ref get_value(expr* e) override;
         void initialize() override;
diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index 870b5ec61..d1d135d1e 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -33,8 +33,6 @@ namespace sls {
         m_values(8U, value_hash(*this), value_eq(*this)) {
         m_fid = user_sort_family_id;
     }
-    
-    euf_plugin::~euf_plugin() {}
 
     void euf_plugin::initialize() {
     }
diff --git a/src/ast/sls/sls_euf_plugin.h b/src/ast/sls/sls_euf_plugin.h
index 1520f7736..34708f3b5 100644
--- a/src/ast/sls/sls_euf_plugin.h
+++ b/src/ast/sls/sls_euf_plugin.h
@@ -60,7 +60,7 @@ namespace sls {
 
     public:
         euf_plugin(context& c);
-        ~euf_plugin() override;
+        ~euf_plugin() override = default;
         expr_ref get_value(expr* e) override;
         void initialize() override;
         void start_propagation() override;
diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h
index 48eb4721c..ad29c4e9a 100644
--- a/src/ast/sls/sls_seq_plugin.h
+++ b/src/ast/sls/sls_seq_plugin.h
@@ -169,7 +169,7 @@ namespace sls {
         bool is_value(expr* e);
     public:
         seq_plugin(context& c);
-        ~seq_plugin() override {}
+        ~seq_plugin() override = default;
         expr_ref get_value(expr* e) override;
         void initialize() override;
         void start_propagation() override {}
diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
index c91b5c90f..e0b4cbcfe 100644
--- a/src/ast/sls/sls_smt_plugin.h
+++ b/src/ast/sls/sls_smt_plugin.h
@@ -27,7 +27,7 @@ namespace sls {
 
     class smt_context {
     public:
-        virtual ~smt_context() {}
+        virtual ~smt_context() = default;
         virtual ast_manager& get_manager() = 0;
         virtual params_ref get_params() = 0;
         virtual void set_value(expr* t, expr* v) = 0;
diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp
index cab62a674..58aeb5eb7 100644
--- a/src/ast/sls/sls_smt_solver.cpp
+++ b/src/ast/sls/sls_smt_solver.cpp
@@ -140,10 +140,7 @@ namespace sls {
 
         m_solver_ctx->updt_params(p);
     }
-    
-    smt_solver::~smt_solver() {        
-    }
-    
+
     void smt_solver::assert_expr(expr* e) {
         if (m.is_and(e)) {
             for (expr* arg : *to_app(e))
diff --git a/src/ast/sls/sls_smt_solver.h b/src/ast/sls/sls_smt_solver.h
index 914397fc1..6f24b708d 100644
--- a/src/ast/sls/sls_smt_solver.h
+++ b/src/ast/sls/sls_smt_solver.h
@@ -32,7 +32,7 @@ namespace sls {
         
     public:
         smt_solver(ast_manager& m, params_ref const& p);
-        ~smt_solver();
+        ~smt_solver() = default;
         void assert_expr(expr* e);
         lbool check();
         model_ref get_model();
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index b08944616..8a742824b 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -97,7 +97,7 @@ public:
 
 class proof_cmds {
 public:
-    virtual ~proof_cmds() {}
+    virtual ~proof_cmds() = default;
     virtual void add_literal(expr* e) = 0;
     virtual void end_assumption() = 0;
     virtual void end_infer() = 0;
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
index cd67218ad..99d9dcef0 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -136,9 +136,7 @@ public:
     void allocate_basis_heading();
     void init();
 
-    virtual ~lp_core_solver_base() {
-        
-    }
+    virtual ~lp_core_solver_base() = default;
 
     vector<unsigned> & non_basis() {
         return m_nbasis;
diff --git a/src/muz/spacer/spacer_arith_kernel.h b/src/muz/spacer/spacer_arith_kernel.h
index 683fed2ba..e470283aa 100644
--- a/src/muz/spacer/spacer_arith_kernel.h
+++ b/src/muz/spacer/spacer_arith_kernel.h
@@ -30,7 +30,7 @@ class spacer_arith_kernel {
   public:
     class plugin {
       public:
-        virtual ~plugin() {}
+        virtual ~plugin() = default;
         virtual bool compute_kernel(const spacer_matrix &in_matrix,
                                     spacer_matrix &out_kernel,
                                     vector<unsigned> &basics) = 0;
diff --git a/src/qe/mbp/mbp_euf.cpp b/src/qe/mbp/mbp_euf.cpp
index bd92be83a..6c550dcbc 100644
--- a/src/qe/mbp/mbp_euf.cpp
+++ b/src/qe/mbp/mbp_euf.cpp
@@ -12,9 +12,6 @@ namespace mbp {
     euf_project_plugin::euf_project_plugin(ast_manager& m): project_plugin(m) {        
     }
 
-    euf_project_plugin::~euf_project_plugin() {
-    }
-    
     bool euf_project_plugin::project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
         return false;
     }
diff --git a/src/qe/mbp/mbp_euf.h b/src/qe/mbp/mbp_euf.h
index f706b0664..c3e6e4015 100644
--- a/src/qe/mbp/mbp_euf.h
+++ b/src/qe/mbp/mbp_euf.h
@@ -21,7 +21,7 @@ namespace mbp {
         bool try_unify(term_graph& g, app* a, expr_ref_vector const& partitions, app_ref_vector& vars, vector<def>& defs);
     public:
         euf_project_plugin(ast_manager& m);
-        ~euf_project_plugin() override;
+        ~euf_project_plugin() override = default;
         
         bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; }
diff --git a/src/sat/sat_ddfw_wrapper.h b/src/sat/sat_ddfw_wrapper.h
index 720b71c03..8da7607a0 100644
--- a/src/sat/sat_ddfw_wrapper.h
+++ b/src/sat/sat_ddfw_wrapper.h
@@ -37,7 +37,7 @@ namespace sat {
 
         ddfw_wrapper() {}
         
-        ~ddfw_wrapper() override {}
+        ~ddfw_wrapper() override = default;
 
         void set_plugin(local_search_plugin* p) { m_ddfw.set_plugin(p); }
 
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index 2836d1130..0c03ed167 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -29,7 +29,7 @@ namespace sat {
     class clause;
 
     struct clause_eh {
-        virtual ~clause_eh() {}
+        virtual ~clause_eh() = default;
         virtual void on_clause(unsigned, literal const*, status) = 0;        
     };
 
diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h
index 427b6fb70..0a0695b68 100644
--- a/src/sat/sat_types.h
+++ b/src/sat/sat_types.h
@@ -96,7 +96,7 @@ namespace sat {
 
     class proof_hint {
     public:
-        virtual ~proof_hint() {}
+        virtual ~proof_hint() = default;
     };
 
     class status {
diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h
index 0da57ee9e..b78ff33ac 100644
--- a/src/sat/smt/euf_proof_checker.h
+++ b/src/sat/smt/euf_proof_checker.h
@@ -31,7 +31,7 @@ namespace euf {
 
     class theory_checker_plugin {
     public:
-        virtual ~theory_checker_plugin() {}
+        virtual ~theory_checker_plugin() = default;
         virtual bool check(app* jst) = 0;
         virtual expr_ref_vector clause(app* jst) = 0;
         virtual void register_plugins(theory_checker& pc) = 0;
diff --git a/src/smt/theory_intblast.cpp b/src/smt/theory_intblast.cpp
index d238ae60d..db244e6ed 100644
--- a/src/smt/theory_intblast.cpp
+++ b/src/smt/theory_intblast.cpp
@@ -35,9 +35,7 @@ namespace smt {
         bv(m),
         a(m)
     {}
-    
-    theory_intblast::~theory_intblast() {}
-        
+
     final_check_status theory_intblast::final_check_eh(unsigned) {
         for (auto e : m_translator.bv2int()) {
             auto* n = ctx.get_enode(e);
diff --git a/src/smt/theory_intblast.h b/src/smt/theory_intblast.h
index 1a2e2c78d..dd720a6ff 100644
--- a/src/smt/theory_intblast.h
+++ b/src/smt/theory_intblast.h
@@ -50,7 +50,7 @@ namespace smt {
 
     public:
         theory_intblast(context& ctx);
-        ~theory_intblast() override;
+        ~theory_intblast() override = default;
 
         char const* get_name() const override { return "bv-intblast"; }
         smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_intblast, *new_ctx); }
diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h
index e8d9b22b4..3585db61c 100644
--- a/src/smt/theory_sls.h
+++ b/src/smt/theory_sls.h
@@ -30,7 +30,7 @@ namespace smt {
         model_ref m_model;
     public:
         theory_sls(context& ctx);
-        ~theory_sls() override {}
+        ~theory_sls() override = default;
         model_ref get_model() { return m_model; }
         char const* get_name() const override { return "sls"; }
         smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_sls, *new_ctx); }