diff --git a/src/api/api_util.h b/src/api/api_util.h
index 80f4f5ec7..0ff2c8ddd 100644
--- a/src/api/api_util.h
+++ b/src/api/api_util.h
@@ -40,7 +40,7 @@ namespace api {
         context& m_context;
     public:
         object(context& c);
-        virtual ~object() {}
+        virtual ~object() = default;
         unsigned ref_count() const { return m_ref_count; }
         unsigned id() const { return m_id; }
         void inc_ref();
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 4012c00d4..8d3a70b8b 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -87,7 +87,7 @@ namespace z3 {
     class exception : public std::exception {
         std::string m_msg;
     public:
-        virtual ~exception() throw() {}
+        virtual ~exception() throw() = default;
         exception(char const * msg):m_msg(msg) {}
         char const * msg() const { return m_msg.c_str(); }
         char const * what() const throw() { return m_msg.c_str(); }
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 798280d2c..d8eb072e3 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1024,7 +1024,7 @@ protected:
     friend class ast_manager;
 
 public:
-    virtual ~decl_plugin() {}
+    virtual ~decl_plugin() = default;
     virtual void finalize() {}
 
 
@@ -2582,7 +2582,7 @@ class ast_mark {
     obj_mark<expr>                        m_expr_marks;
     obj_mark<decl, bit_vector, decl2uint> m_decl_marks;
 public:
-    virtual ~ast_mark() {}
+    virtual ~ast_mark() = default;
     bool is_marked(ast * n) const;
     virtual void mark(ast * n, bool flag);
     virtual void reset();
diff --git a/src/ast/ast_printer.h b/src/ast/ast_printer.h
index 37023393f..bea01e826 100644
--- a/src/ast/ast_printer.h
+++ b/src/ast/ast_printer.h
@@ -24,7 +24,7 @@ Revision History:
 
 class ast_printer {
 public:
-    virtual ~ast_printer() {}
+    virtual ~ast_printer() = default;
     virtual void pp(sort * s, format_ns::format_ref & r) const { UNREACHABLE(); }
     virtual void pp(func_decl * f, format_ns::format_ref & r) const { UNREACHABLE(); }
     virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const { UNREACHABLE(); }
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index dbf9340ad..47649b9b2 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -46,7 +46,7 @@ protected:
     format_ns::format * pp_as(format_ns::format * fname, sort * s);
     format_ns::format * pp_signature(format_ns::format * f_name, func_decl * f);
 public:
-    virtual ~smt2_pp_environment() {}
+    virtual ~smt2_pp_environment() = default;
     virtual ast_manager & get_manager() const = 0;
     virtual arith_util & get_autil() = 0;
     virtual bv_util & get_bvutil() = 0;
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 0698bf821..310175781 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -105,7 +105,7 @@ namespace datatype {
         class size {
             unsigned m_ref{ 0 };
         public:
-            virtual ~size() { }
+            virtual ~size() = default;
             void inc_ref() { ++m_ref; }
             void dec_ref();
             static size* mk_offset(sort_size const& s); 
diff --git a/src/ast/expr_functors.h b/src/ast/expr_functors.h
index 4e87fb39e..af669f48e 100644
--- a/src/ast/expr_functors.h
+++ b/src/ast/expr_functors.h
@@ -27,14 +27,14 @@ Revision History:
 class i_expr_pred {
 public:
     virtual bool operator()(expr* e) = 0;
-    virtual ~i_expr_pred() {}
+    virtual ~i_expr_pred() = default;
 };
 
 
 class i_sort_pred {
 public:
     virtual bool operator()(sort* s) = 0;
-    virtual ~i_sort_pred() {}
+    virtual ~i_sort_pred() = default;
 };
 
 
diff --git a/src/ast/macros/quantifier_macro_info.h b/src/ast/macros/quantifier_macro_info.h
index 82790e937..646b31c88 100644
--- a/src/ast/macros/quantifier_macro_info.h
+++ b/src/ast/macros/quantifier_macro_info.h
@@ -39,7 +39,7 @@ protected:
     void collect_macro_candidates(quantifier* q);
 public:
     quantifier_macro_info(ast_manager& m, quantifier* q);
-    virtual ~quantifier_macro_info() {}
+    virtual ~quantifier_macro_info() = default;
     bool is_auf() const { return m_is_auf; }
     quantifier* get_flat_q() const { return m_flat_q; }
     bool has_cond_macros() const { return !m_cond_macros.empty(); }
diff --git a/src/ast/normal_forms/elim_term_ite.h b/src/ast/normal_forms/elim_term_ite.h
index 60f2ad8f7..36302ad1e 100644
--- a/src/ast/normal_forms/elim_term_ite.h
+++ b/src/ast/normal_forms/elim_term_ite.h
@@ -31,7 +31,7 @@ public:
     elim_term_ite_cfg(ast_manager & m, defined_names & d): m(m), m_defined_names(d) { 
         // TBD enable_ac_support(false);
     }
-    virtual ~elim_term_ite_cfg() {}
+    virtual ~elim_term_ite_cfg() = default;
     vector<justified_expr> const& new_defs() const { return m_new_defs; }
     br_status reduce_app(func_decl* f, unsigned n, expr *const* args, expr_ref& result, proof_ref& result_pr);
     void push() { m_lim.push_back(m_new_defs.size()); }
diff --git a/src/ast/normal_forms/name_exprs.h b/src/ast/normal_forms/name_exprs.h
index 268df8821..4f652bce8 100644
--- a/src/ast/normal_forms/name_exprs.h
+++ b/src/ast/normal_forms/name_exprs.h
@@ -29,7 +29,7 @@ public:
 
 class name_exprs {
 public:
-    virtual ~name_exprs() {}
+    virtual ~name_exprs() = default;
     virtual void operator()(expr * n,                          // [IN] expression that contain the sub-expressions to be named
                             expr_ref_vector & new_defs,        // [OUT] new definitions
                             proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions 
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index bbc4e5810..dcff35e82 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -49,7 +49,7 @@ namespace recfun {
 
     class replace {
     public:
-        virtual ~replace() {}
+        virtual ~replace() = default;
         virtual void reset() = 0;
         virtual void insert(expr* d, expr* r) = 0;
         virtual expr_ref operator()(expr* e) = 0;
diff --git a/src/ast/rewriter/expr_replacer.h b/src/ast/rewriter/expr_replacer.h
index e587faad7..82982adff 100644
--- a/src/ast/rewriter/expr_replacer.h
+++ b/src/ast/rewriter/expr_replacer.h
@@ -28,7 +28,7 @@ Notes:
 class expr_replacer {
     struct scoped_set_subst;
 public:
-    virtual ~expr_replacer() {}
+    virtual ~expr_replacer() = default;
 
     virtual ast_manager & m() const = 0;
     virtual void set_substitution(expr_substitution * s) = 0;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 4c7c3883a..cb00938d7 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -83,7 +83,7 @@ public:
 
 class expr_solver {
 public:
-    virtual ~expr_solver() {}
+    virtual ~expr_solver() = default;
     virtual lbool check_sat(expr* e) = 0;
 };
 
diff --git a/src/ast/substitution/substitution_tree.h b/src/ast/substitution/substitution_tree.h
index c94bb4eea..13993c171 100644
--- a/src/ast/substitution/substitution_tree.h
+++ b/src/ast/substitution/substitution_tree.h
@@ -29,7 +29,7 @@ protected:
     substitution & m_subst;
 public:
     st_visitor(substitution & s):m_subst(s) {}
-    virtual ~st_visitor() {}
+    virtual ~st_visitor() = default;
     substitution & get_substitution() { return m_subst; }
     virtual bool operator()(expr * e) { return true; }
 };
diff --git a/src/ast/value_generator.h b/src/ast/value_generator.h
index 7b77b144e..f3a459389 100644
--- a/src/ast/value_generator.h
+++ b/src/ast/value_generator.h
@@ -23,7 +23,7 @@
 
 class value_generator_core {
  public:        
-    virtual ~value_generator_core() {}
+    virtual ~value_generator_core() = default;
     virtual family_id get_fid() const = 0;
     virtual expr_ref get_value(sort* s, unsigned index) = 0;
 };
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 3dc49624b..d54a90143 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -96,7 +96,7 @@ public:
 class object_ref {
     unsigned m_ref_count = 0;
 public:
-    virtual ~object_ref() {}
+    virtual ~object_ref() = default;
     virtual void finalize(cmd_context & ctx) = 0;
     void inc_ref(cmd_context & ctx) {
         m_ref_count++;
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 5c7058bb5..b8dd01aea 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -781,7 +781,7 @@ struct pdecl_manager::sort_info {
         m_decl(d) {
         m.inc_ref(d);
     }
-    virtual ~sort_info() {}
+    virtual ~sort_info() = default;
     virtual unsigned obj_size() const { return sizeof(sort_info); }
     virtual void finalize(pdecl_manager & m) { m.dec_ref(m_decl); }
     virtual void display(std::ostream & out, pdecl_manager const & m) const = 0;
diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h
index 66e1e5e81..a55f782f0 100644
--- a/src/cmd_context/pdecl.h
+++ b/src/cmd_context/pdecl.h
@@ -38,7 +38,7 @@ protected:
     virtual size_t obj_size() const { UNREACHABLE(); return sizeof(*this); }
     pdecl(unsigned id, unsigned num_params):m_id(id), m_num_params(num_params), m_ref_count(0) {}
     virtual void finalize(pdecl_manager & m) {}
-    virtual ~pdecl() {}
+    virtual ~pdecl() = default;
 public:
     virtual bool check_num_params(pdecl * other) const { return m_num_params == other->m_num_params; }
     unsigned get_num_params() const { return m_num_params; }
@@ -257,7 +257,7 @@ public:
 
 class new_datatype_eh {
 public:
-    virtual ~new_datatype_eh() {}
+    virtual ~new_datatype_eh() = default;
     virtual void operator()(sort * dt, pdecl* pd) = 0;
 };
 
diff --git a/src/math/automata/boolean_algebra.h b/src/math/automata/boolean_algebra.h
index 8c1ca55e6..a642ceb41 100644
--- a/src/math/automata/boolean_algebra.h
+++ b/src/math/automata/boolean_algebra.h
@@ -25,7 +25,7 @@ Revision History:
 template<class T>
 class positive_boolean_algebra {
 public:
-    virtual ~positive_boolean_algebra() {}
+    virtual ~positive_boolean_algebra() = default;
     virtual T mk_false() = 0;
     virtual T mk_true() = 0;
     virtual T mk_and(T x, T y) = 0;
diff --git a/src/math/hilbert/heap_trie.h b/src/math/hilbert/heap_trie.h
index fcdce7311..b492fb7ee 100644
--- a/src/math/hilbert/heap_trie.h
+++ b/src/math/hilbert/heap_trie.h
@@ -66,7 +66,7 @@ class heap_trie {
         unsigned m_ref;
     public:
         node(node_t t): m_type(t), m_ref(0) {}
-        virtual ~node() {}
+        virtual ~node() = default;
         node_t type() const { return m_type; }
         void inc_ref() { ++m_ref; }
         void dec_ref() { SASSERT(m_ref > 0); --m_ref; }
diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h
index 3bcd62d00..8e6311683 100644
--- a/src/math/lp/lar_constraints.h
+++ b/src/math/lp/lar_constraints.h
@@ -57,7 +57,7 @@ public:
 
     virtual vector<std::pair<mpq, var_index>> coeffs() const = 0;
     lar_base_constraint(unsigned j, lconstraint_kind kind, const mpq& right_side) :m_kind(kind), m_right_side(right_side), m_active(false), m_j(j) {}
-    virtual ~lar_base_constraint() {}
+    virtual ~lar_base_constraint() = default;
 
     lconstraint_kind kind() const { return m_kind; }
     mpq const& rhs() const { return m_right_side; }
diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h
index 8c05f8354..2a4e5058d 100644
--- a/src/math/lp/lp_api.h
+++ b/src/math/lp/lp_api.h
@@ -49,7 +49,7 @@ namespace lp_api {
             m_constraints[1] = ct;
         }
 
-        virtual ~bound() {}
+        virtual ~bound() = default;
 
         theory_var get_var() const { return m_var; }
 
diff --git a/src/math/lp/matrix.h b/src/math/lp/matrix.h
index 80ddb1228..88a405614 100644
--- a/src/math/lp/matrix.h
+++ b/src/math/lp/matrix.h
@@ -22,7 +22,7 @@ public:
     virtual void set_number_of_rows(unsigned m)  = 0;
     virtual void set_number_of_columns(unsigned n) = 0;
 
-    virtual ~matrix() {}
+    virtual ~matrix() = default;
 
     bool is_equal(const matrix<T, X>& other);
     bool operator == (matrix<T, X> const & other) {
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 083b935a4..e4087a407 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -85,7 +85,7 @@ public:
     bool is_scalar() const { return type() == expr_type::SCALAR; }
     virtual bool is_pure_monomial() const { return false; }
     std::string str() const { std::stringstream ss; print(ss); return ss.str(); }
-    virtual ~nex() {}
+    virtual ~nex() = default;
     virtual bool contains(lpvar j) const { return false; }
     virtual unsigned get_degree() const = 0;
     // simplifies the expression and also assigns the address of "this" to *e
diff --git a/src/math/lp/tail_matrix.h b/src/math/lp/tail_matrix.h
index 2047e8c7e..9fa1a4a47 100644
--- a/src/math/lp/tail_matrix.h
+++ b/src/math/lp/tail_matrix.h
@@ -37,7 +37,7 @@ public:
     virtual void apply_from_left(vector<X> & w, lp_settings & settings) = 0;
     virtual void apply_from_right(vector<T> & w) = 0;
     virtual void apply_from_right(indexed_vector<T> & w) = 0;
-    virtual ~tail_matrix() {}
+    virtual ~tail_matrix() = default;
     virtual bool is_dense() const = 0;
     struct ref_row {
         const tail_matrix & m_A;
diff --git a/src/math/simplex/network_flow.h b/src/math/simplex/network_flow.h
index 9be3b1191..b2c9cd9b3 100644
--- a/src/math/simplex/network_flow.h
+++ b/src/math/simplex/network_flow.h
@@ -87,7 +87,7 @@ namespace smt {
                   m_states(states),
                   m_enter_id(enter_id) {
             }
-            virtual ~pivot_rule_impl() {}
+            virtual ~pivot_rule_impl() = default;
             virtual bool choose_entering_edge() = 0;
             virtual pivot_rule rule() const = 0;
         };
diff --git a/src/math/subpaving/subpaving.h b/src/math/subpaving/subpaving.h
index 96d05f4de..b76f5e831 100644
--- a/src/math/subpaving/subpaving.h
+++ b/src/math/subpaving/subpaving.h
@@ -39,7 +39,7 @@ namespace subpaving {
 
 class context {
 public:
-    virtual ~context() {}
+    virtual ~context() = default;
 
     virtual unsynch_mpq_manager & qm() const = 0;
 
diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h
index cfe3aea70..7300e3da3 100644
--- a/src/math/subpaving/subpaving_t.h
+++ b/src/math/subpaving/subpaving_t.h
@@ -385,7 +385,7 @@ public:
         context_t * m_ctx;
     public:
         node_selector(context_t * ctx):m_ctx(ctx) {}
-        virtual ~node_selector() {}
+        virtual ~node_selector() = default;
 
         context_t * ctx() const { return m_ctx; }
 
@@ -403,7 +403,7 @@ public:
         context_t * m_ctx;
     public:
         var_selector(context_t * ctx):m_ctx(ctx) {}
-        virtual ~var_selector() {}
+        virtual ~var_selector() = default;
 
         context_t * ctx() const { return m_ctx; }
 
@@ -436,7 +436,7 @@ public:
         context_t * m_ctx;
     public:
         node_splitter(context_t * ctx):m_ctx(ctx) {}
-        virtual ~node_splitter() {}
+        virtual ~node_splitter() = default;
         
         context_t * ctx() const { return m_ctx; }
         node * mk_node(node * p) { return ctx()->mk_node(p); }
diff --git a/src/model/model_macro_solver.h b/src/model/model_macro_solver.h
index 1c04f8ec1..8070b4ada 100644
--- a/src/model/model_macro_solver.h
+++ b/src/model/model_macro_solver.h
@@ -20,7 +20,7 @@ Author:
 
 class quantifier2macro_infos {
 public:
-    virtual ~quantifier2macro_infos() {}
+    virtual ~quantifier2macro_infos() = default;
     virtual quantifier_macro_info* operator()(quantifier* q) = 0;
 };
 
@@ -48,7 +48,7 @@ public:
         m_model(nullptr) {
     }
 
-    virtual ~base_macro_solver() {}
+    virtual ~base_macro_solver() = default;
 
     /**
        \brief Try to satisfy quantifiers in qs by using macro definitions.
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index f6ce39518..4efe79dd3 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -53,7 +53,7 @@ namespace datalog {
                 m_limited_size = ctx.get_decl_util().try_get_size(s, m_size);
         }
     public:
-        virtual ~sort_domain() {}
+        virtual ~sort_domain() = default;
 
         sort_kind get_kind() const { return m_kind; }
         virtual unsigned get_constant_count() const = 0;
diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h
index fcf45abf9..64218f7d6 100644
--- a/src/muz/base/dl_engine_base.h
+++ b/src/muz/base/dl_engine_base.h
@@ -42,7 +42,7 @@ namespace datalog {
         std::string m_name;
     public:
         engine_base(ast_manager& m, char const* name): m(m), m_name(name) {}
-        virtual ~engine_base() {}
+        virtual ~engine_base() = default;
 
         virtual expr_ref get_answer() = 0;
         virtual expr_ref get_ground_sat_answer () {
diff --git a/src/muz/base/dl_rule_transformer.h b/src/muz/base/dl_rule_transformer.h
index 59eb24f55..c446593bd 100644
--- a/src/muz/base/dl_rule_transformer.h
+++ b/src/muz/base/dl_rule_transformer.h
@@ -89,7 +89,7 @@ namespace datalog {
             m_can_destratify_negation(can_destratify_negation), m_transformer(nullptr) {}
 
     public:
-        virtual ~plugin() {}
+        virtual ~plugin() = default;
 
         unsigned get_priority() { return m_priority; }
         bool can_destratify_negation() const { return m_can_destratify_negation; }
diff --git a/src/muz/fp/datalog_parser.h b/src/muz/fp/datalog_parser.h
index 2369f1d84..e836cbaec 100644
--- a/src/muz/fp/datalog_parser.h
+++ b/src/muz/fp/datalog_parser.h
@@ -27,7 +27,7 @@ namespace datalog {
     public:        
         static parser * create(context& ctx, ast_manager & ast_manager);
 
-        virtual ~parser() {}
+        virtual ~parser() = default;
 
         virtual bool parse_file(char const * path) = 0;
         virtual bool parse_string(char const * string) = 0;
@@ -37,7 +37,7 @@ namespace datalog {
     public:        
         static wpa_parser * create(context& ctx, ast_manager & ast_manager);
 
-        virtual ~wpa_parser() {}
+        virtual ~wpa_parser() = default;
 
         virtual bool parse_directory(char const * path) = 0;
     };
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index 376b41d34..ea317ca45 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -179,7 +179,7 @@ namespace datalog {
         class base_fn {
         public:
             base_fn() = default;
-            virtual ~base_fn() {}
+            virtual ~base_fn() = default;
 
             base_fn(const base_fn &) = delete;
             base_fn& operator=(const base_fn &) = delete;
@@ -260,7 +260,7 @@ namespace datalog {
             */
             bool check_kind(base_object const& r) const { return &r.get_plugin()==this; }
         public:
-            virtual ~plugin_object() {}
+            virtual ~plugin_object() = default;
 
             virtual void initialize(family_id fid) { m_kind = fid; }
 
@@ -423,7 +423,7 @@ namespace datalog {
             }
 #endif
 
-            virtual ~base_ancestor() {}
+            virtual ~base_ancestor() = default;
 
             void set_kind(family_id kind) { SASSERT(kind>=0); m_kind = kind; }
 
@@ -865,7 +865,7 @@ namespace datalog {
 
     class table_row_mutator_fn {
     public:
-        virtual ~table_row_mutator_fn() {}
+        virtual ~table_row_mutator_fn() = default;
         /**
             \brief The function is called for a particular table row. The \c func_columns contains
             a pointer to an array of functional column values that can be modified. If the function
@@ -879,7 +879,7 @@ namespace datalog {
 
     class table_row_pair_reduce_fn {
     public:
-        virtual ~table_row_pair_reduce_fn() {}
+        virtual ~table_row_pair_reduce_fn() = default;
         /**
             \brief The function is called for pair of table rows that became duplicated due to projection.
             The values that are in the first array after return from the function will be used for the
@@ -1095,7 +1095,7 @@ namespace datalog {
             unsigned m_ref_cnt;
         public:
             iterator_core() : m_ref_cnt(0) {}
-            virtual ~iterator_core() {}
+            virtual ~iterator_core() = default;
 
             iterator_core(const iterator_core &) = delete;
             iterator_core & operator=(const iterator_core &) = delete;
@@ -1124,7 +1124,7 @@ namespace datalog {
             unsigned m_ref_cnt;
         public:
             row_iterator_core() : m_ref_cnt(0) {}
-            virtual ~row_iterator_core() {}
+            virtual ~row_iterator_core() = default;
 
             row_iterator_core(const row_iterator_core &) = delete;
             row_iterator_core & operator=(const row_iterator_core &) = delete;
@@ -1205,7 +1205,7 @@ namespace datalog {
             typedef row_iterator const_iterator;
 
             row_interface(const table_base & parent_table) : m_parent_table(parent_table) {}
-            virtual ~row_interface() {}
+            virtual ~row_interface() = default;
 
             virtual table_element operator[](unsigned col) const = 0;
 
diff --git a/src/muz/rel/dl_external_relation.h b/src/muz/rel/dl_external_relation.h
index 4b5689465..17e9a2364 100644
--- a/src/muz/rel/dl_external_relation.h
+++ b/src/muz/rel/dl_external_relation.h
@@ -26,7 +26,7 @@ namespace datalog {
 
     class external_relation_context {
     public:
-        virtual ~external_relation_context() {}
+        virtual ~external_relation_context() = default;
 
         virtual family_id get_family_id() const = 0;
 
diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h
index 1edacc94f..a008c2b73 100644
--- a/src/muz/rel/dl_instruction.h
+++ b/src/muz/rel/dl_instruction.h
@@ -317,7 +317,7 @@ namespace datalog {
     class instruction_block {
     public:
         struct instruction_observer {
-            virtual ~instruction_observer() {}
+            virtual ~instruction_observer() = default;
             virtual void notify(instruction * i) {}
         };
     private:
diff --git a/src/muz/rel/dl_lazy_table.h b/src/muz/rel/dl_lazy_table.h
index 56bfc961f..9f88e6aa2 100644
--- a/src/muz/rel/dl_lazy_table.h
+++ b/src/muz/rel/dl_lazy_table.h
@@ -107,7 +107,7 @@ namespace datalog {
     public:
         lazy_table_ref(lazy_table_plugin& p, table_signature const& sig): 
             m_plugin(p), m_signature(sig), m_ref(0) {}
-        virtual ~lazy_table_ref() {}
+        virtual ~lazy_table_ref() = default;
         void inc_ref() { ++m_ref; }
         void dec_ref() { --m_ref; if (0 == m_ref) dealloc(this);  }
         void release_table() { m_table.release(); }
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index a782cc143..9410e2ab0 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -999,7 +999,7 @@ namespace datalog {
     class relation_manager::auxiliary_table_transformer_fn {
         table_fact m_row;
     public:
-        virtual ~auxiliary_table_transformer_fn() {}
+        virtual ~auxiliary_table_transformer_fn() = default;
         virtual const table_signature & get_result_signature() const = 0;
         virtual void modify_fact(table_fact & f) const = 0;
 
@@ -1241,7 +1241,7 @@ namespace datalog {
         table_fact m_row;
         svector<table_element> m_to_remove;
     public:
-        virtual ~auxiliary_table_filter_fn() {}
+        virtual ~auxiliary_table_filter_fn() = default;
         virtual bool should_remove(const table_fact & f) const = 0;
 
         void operator()(table_base & r) {
diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp
index 9f3304e7a..6c2373d54 100644
--- a/src/muz/rel/dl_sparse_table.cpp
+++ b/src/muz/rel/dl_sparse_table.cpp
@@ -274,7 +274,7 @@ namespace datalog {
         key_indexer(unsigned key_len, const unsigned * key_cols) 
             : m_key_cols(key_len, key_cols) {}
 
-        virtual ~key_indexer() {}
+        virtual ~key_indexer() = default;
 
         virtual void update(const sparse_table & t) {}
 
diff --git a/src/muz/rel/dl_table_plugin.h b/src/muz/rel/dl_table_plugin.h
index 51e54d3ea..d0f239f79 100644
--- a/src/muz/rel/dl_table_plugin.h
+++ b/src/muz/rel/dl_table_plugin.h
@@ -40,7 +40,7 @@ namespace datalog {
 
         class base_fn {
         public:
-            virtual ~base_fn() {}
+            virtual ~base_fn() = default;
         };
 
         class join_fn : public base_fn {
@@ -113,7 +113,7 @@ namespace datalog {
             base_ancestor(kind k, relation_manager & m, const signature & s) 
                 : m_kind(k), m_manager(m), m_signature(s) {}
         public:
-            virtual ~base_ancestor() {}
+            virtual ~base_ancestor() = default;
 
             kind get_kind() const { return m_kind; }
             relation_manager & get_manager() const { return m_manager; }
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index b62da0766..6ef56c737 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -857,7 +857,7 @@ protected:
     context& m_ctx;
 public:
     lemma_generalizer(context& ctx): m_ctx(ctx) {}
-    virtual ~lemma_generalizer() {}
+    virtual ~lemma_generalizer() = default;
     virtual void operator()(lemma_ref &lemma) = 0;
     virtual void collect_statistics(statistics& st) const {}
     virtual void reset_statistics() {}
diff --git a/src/muz/spacer/spacer_unsat_core_plugin.h b/src/muz/spacer/spacer_unsat_core_plugin.h
index 581a877cf..a7ea4c89b 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.h
+++ b/src/muz/spacer/spacer_unsat_core_plugin.h
@@ -31,7 +31,7 @@ namespace spacer {
         ast_manager& m;
     public:
         unsat_core_plugin(unsat_core_learner& learner);
-        virtual ~unsat_core_plugin() {};
+        virtual ~unsat_core_plugin() = default;
         virtual void compute_partial_core(proof* step) = 0;
         virtual void finalize(){};
 
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 72195467f..ac39d7891 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -42,7 +42,7 @@ namespace opt {
 
     class maxsmt_solver {
     public:        
-        virtual ~maxsmt_solver() {}
+        virtual ~maxsmt_solver() = default;
         virtual lbool operator()() = 0;
         virtual rational get_lower() const = 0;
         virtual rational get_upper() const = 0;
diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h
index 8e16ec5c8..1bc27f9b1 100644
--- a/src/opt/opt_lns.h
+++ b/src/opt/opt_lns.h
@@ -28,7 +28,7 @@ namespace opt {
 
     class lns_context {
     public:
-        virtual ~lns_context() {}
+        virtual ~lns_context() = default;
         virtual void update_model(model_ref& mdl) = 0;
         virtual void relax_cores(vector<expr_ref_vector> const& cores) = 0;
         virtual rational cost(model& mdl) = 0;
diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h
index ab5a90237..105f4007f 100644
--- a/src/opt/opt_pareto.h
+++ b/src/opt/opt_pareto.h
@@ -52,7 +52,7 @@ namespace opt {
             m_solver(s),
             m_params(p) {
         }
-        virtual ~pareto_base() {}
+        virtual ~pareto_base() = default;
         virtual void updt_params(params_ref & p) {
             m_solver->updt_params(p);
             m_params.copy(p);
diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h
index 5256dd47a..2867f52a3 100644
--- a/src/opt/opt_sls_solver.h
+++ b/src/opt/opt_sls_solver.h
@@ -55,7 +55,7 @@ namespace opt {
         {            
             updt_params(p);
         }
-        virtual ~sls_solver() {}
+        virtual ~sls_solver() = default;
 
         virtual void updt_params(params_ref & p) {
             m_solver->updt_params(p);
diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h
index 12b592960..4f73b92e6 100644
--- a/src/qe/mbp/mbp_plugin.h
+++ b/src/qe/mbp/mbp_plugin.h
@@ -59,7 +59,7 @@ namespace mbp {
 
     public:
         project_plugin(ast_manager& m) :m(m), m_cache(m), m_args(m), m_pure_eqs(m) {}
-        virtual ~project_plugin() {}
+        virtual ~project_plugin() = default;
         virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { return false; }
         /**
            \brief partial solver.
diff --git a/src/qe/mbp/mbp_solve_plugin.h b/src/qe/mbp/mbp_solve_plugin.h
index 27e7f85a8..2450eab4f 100644
--- a/src/qe/mbp/mbp_solve_plugin.h
+++ b/src/qe/mbp/mbp_solve_plugin.h
@@ -36,7 +36,7 @@ namespace mbp {
         bool is_variable(expr* e) const { return m_is_var(e); }
     public:
         solve_plugin(ast_manager& m, family_id fid, is_variable_proc& is_var) : m(m), m_id(fid), m_is_var(is_var) {}
-        virtual ~solve_plugin() {}
+        virtual ~solve_plugin() = default;
         family_id get_family_id() const { return m_id; }
         /// Process (and potentially augment) a literal
         expr_ref operator() (expr *lit);
diff --git a/src/qe/nlarith_util.h b/src/qe/nlarith_util.h
index acbe4889e..dccc4f606 100644
--- a/src/qe/nlarith_util.h
+++ b/src/qe/nlarith_util.h
@@ -116,7 +116,7 @@ namespace nlarith {
 
         class eval {
         public:
-            virtual ~eval() {}
+            virtual ~eval() = default;
             virtual lbool operator()(app* a) = 0;
         };
 
@@ -124,7 +124,7 @@ namespace nlarith {
         
         class branch {
         public:
-            virtual ~branch() {}
+            virtual ~branch() = default;
             virtual app* get_constraint() = 0;
             virtual void get_updates(ptr_vector<app>& atoms, svector<atom_update>& updates) = 0;
         };
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 509b73835..d859880d8 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -877,7 +877,7 @@ namespace qe {
 
     class quant_elim {
     public:
-        virtual ~quant_elim() {}
+        virtual ~quant_elim() = default;
     
         virtual lbool eliminate_exists(
             unsigned num_vars, app* const* vars, 
diff --git a/src/qe/qe.h b/src/qe/qe.h
index a5152522f..55729d0b5 100644
--- a/src/qe/qe.h
+++ b/src/qe/qe.h
@@ -149,7 +149,7 @@ namespace qe {
             m_ctx(ctx)
         {}
         
-        virtual ~qe_solver_plugin() {}
+        virtual ~qe_solver_plugin() = default;
         
         family_id get_family_id() { return m_fid; }
 
diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h
index e35822813..70c0f98bb 100644
--- a/src/qe/qe_mbi.h
+++ b/src/qe/qe_mbi.h
@@ -43,7 +43,7 @@ namespace qe {
         lbool is_shared_cached(expr* e);
     public:
         mbi_plugin(ast_manager& m): m(m), m_shared_trail(m) {}
-        virtual ~mbi_plugin() {}
+        virtual ~mbi_plugin() = default;
 
         /**
          * Set the shared symbols.
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index 1bb37b7d7..ffcb95587 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -70,7 +70,7 @@ namespace sat {
         solver* m_solver { nullptr };
     public:        
         extension(symbol const& name, int id): m_id(id), m_name(name) { }
-        virtual ~extension() {}
+        virtual ~extension() = default;
         int get_id() const { return m_id; }
         void set_solver(solver* s) { m_solver = s; }        
         solver& s() { return *m_solver; }
diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h
index 407deae5c..5c8b7e315 100644
--- a/src/sat/sat_solver_core.h
+++ b/src/sat/sat_solver_core.h
@@ -31,7 +31,7 @@ namespace sat {
         reslimit&               m_rlimit;
     public:
         solver_core(reslimit& l) : m_rlimit(l) {}
-        virtual ~solver_core() {}
+        virtual ~solver_core() = default;
 
         // add clauses
         virtual void add_clause(unsigned n, literal* lits, status st) = 0;
diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h
index fa42f0712..db13db054 100644
--- a/src/sat/sat_types.h
+++ b/src/sat/sat_types.h
@@ -80,7 +80,7 @@ namespace sat {
 
     class i_local_search {
     public:
-        virtual ~i_local_search() {}
+        virtual ~i_local_search() = default;
         virtual void add(solver const& s) = 0;
         virtual void updt_params(params_ref const& p) = 0;
         virtual void set_seed(unsigned s) = 0;
diff --git a/src/sat/smt/q_mam.h b/src/sat/smt/q_mam.h
index c396a319b..9fc6d18f1 100644
--- a/src/sat/smt/q_mam.h
+++ b/src/sat/smt/q_mam.h
@@ -45,7 +45,7 @@ namespace q {
 
         static mam * mk(euf::solver& ctx, ematch& em);
         
-        virtual ~mam() {}
+        virtual ~mam() = default;
         
         virtual void add_pattern(quantifier * q, app * mp) = 0;
 
diff --git a/src/sat/smt/q_model_fixer.h b/src/sat/smt/q_model_fixer.h
index 9653268e6..2c16504c6 100644
--- a/src/sat/smt/q_model_fixer.h
+++ b/src/sat/smt/q_model_fixer.h
@@ -43,7 +43,7 @@ namespace q {
         ast_manager& m;
     public:
         projection_function(ast_manager& m) : m(m) {}
-        virtual ~projection_function() {}
+        virtual ~projection_function() = default;
         virtual expr* mk_lt(expr* a, expr* b) = 0;
         expr* mk_le(expr* a, expr* b) { return m.mk_not(mk_lt(b, a)); }
         virtual bool operator()(expr* a, expr* b) const = 0;
diff --git a/src/sat/smt/sat_internalizer.h b/src/sat/smt/sat_internalizer.h
index 43413a893..e7d0d9b43 100644
--- a/src/sat/smt/sat_internalizer.h
+++ b/src/sat/smt/sat_internalizer.h
@@ -21,7 +21,7 @@ Author:
 namespace sat {
     class sat_internalizer {
     public:
-        virtual ~sat_internalizer() {}
+        virtual ~sat_internalizer() = default;
         virtual bool is_bool_op(expr* e) const = 0;
         virtual literal internalize(expr* e, bool learned) = 0;
         virtual bool_var to_bool_var(expr* e) = 0;
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index 7209fa051..833b6c05e 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -39,7 +39,7 @@ namespace euf {
         virtual bool post_visit(expr* e, bool sign, bool root) { return false; }
 
     public:
-        virtual ~th_internalizer() {}
+        virtual ~th_internalizer() = default;
 
         virtual sat::literal internalize(expr* e, bool sign, bool root, bool redundant) = 0;
 
@@ -60,7 +60,7 @@ namespace euf {
 
     class th_decompile {
     public:
-        virtual ~th_decompile() {}
+        virtual ~th_decompile() = default;
 
         virtual bool to_formulas(std::function<expr_ref(sat::literal)>& lit2expr, expr_ref_vector& fmls) { return false; }
     };
@@ -68,7 +68,7 @@ namespace euf {
     class th_model_builder {
     public:
 
-        virtual ~th_model_builder() {}
+        virtual ~th_model_builder() = default;
 
         /**
            \brief compute the value for enode \c n and store the value in \c values
diff --git a/src/smt/mam.h b/src/smt/mam.h
index bf23b24a6..e7051b3f7 100644
--- a/src/smt/mam.h
+++ b/src/smt/mam.h
@@ -37,8 +37,7 @@ namespace smt {
             m_context(ctx) {
         }
         
-        virtual ~mam() {
-        }
+        virtual ~mam() = default;
         
         virtual void add_pattern(quantifier * q, app * mp) = 0;
 
diff --git a/src/smt/smt_case_split_queue.h b/src/smt/smt_case_split_queue.h
index 91f7fc036..a84b5ea4f 100644
--- a/src/smt/smt_case_split_queue.h
+++ b/src/smt/smt_case_split_queue.h
@@ -45,7 +45,7 @@ namespace smt {
         virtual void pop_scope(unsigned num_scopes) = 0;
         virtual void next_case_split(bool_var & next, lbool & phase) = 0;
         virtual void display(std::ostream & out) = 0;
-        virtual ~case_split_queue() {}
+        virtual ~case_split_queue() = default;
 
         // theory-aware branching hint
         virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {}
diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h
index 950d0e17c..89d8f2d66 100644
--- a/src/smt/smt_clause.h
+++ b/src/smt/smt_clause.h
@@ -33,7 +33,7 @@ namespace smt {
     */
     class clause_del_eh {
     public:
-        virtual ~clause_del_eh() {}
+        virtual ~clause_del_eh() = default;
         virtual void operator()(ast_manager & m, clause * cls) = 0;
     };
 
diff --git a/src/smt/smt_for_each_relevant_expr.h b/src/smt/smt_for_each_relevant_expr.h
index 4b4492b7f..20be165c6 100644
--- a/src/smt/smt_for_each_relevant_expr.h
+++ b/src/smt/smt_for_each_relevant_expr.h
@@ -65,7 +65,7 @@ namespace smt {
 
     public:
         for_each_relevant_expr(context & ctx);
-        virtual ~for_each_relevant_expr() {}
+        virtual ~for_each_relevant_expr() = default;
         /**
            \brief Visit the relevant sub-expressions of n.
            That is, only subexpressions m of n, such that m_context.is_relevant(m).
diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h
index b90233792..b13d12743 100644
--- a/src/smt/smt_justification.h
+++ b/src/smt/smt_justification.h
@@ -49,7 +49,7 @@ namespace smt {
         unsigned m_in_region:1; // true if the object was allocated in a region.
     public:
         justification(bool in_region = true):m_mark(false), m_in_region(in_region) {}
-        virtual ~justification() {}
+        virtual ~justification() = default;
 
         /**
            \brief This method should return true if the method del_eh needs to be invoked 
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 24ec4d5b9..94a0992f3 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1157,7 +1157,7 @@ namespace smt {
             ast_manager& m;
         public:
             qinfo(ast_manager& m) :m(m) {}
-            virtual ~qinfo() {}
+            virtual ~qinfo() = default;
             virtual char const* get_kind() const = 0;
             virtual bool is_equal(qinfo const* qi) const = 0;
             virtual void display(std::ostream& out) const { out << "[" << get_kind() << "]"; }
diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h
index 80bd59799..632557e98 100644
--- a/src/smt/smt_model_generator.h
+++ b/src/smt/smt_model_generator.h
@@ -136,7 +136,7 @@ namespace smt {
     */
     class model_value_proc {
     public:
-        virtual ~model_value_proc() {}
+        virtual ~model_value_proc() = default;
         /**
            \brief Fill result with the dependencies of this functor.
            That is, to invoke mk_value, the dependencies in result must be constructed.
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index d9a43ddea..abb3cac7c 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -106,7 +106,7 @@ namespace smt {
 
     class quantifier_manager_plugin {
     public:
-        virtual ~quantifier_manager_plugin() {}
+        virtual ~quantifier_manager_plugin() = default;
 
         virtual void set_manager(quantifier_manager & qm) = 0;
 
diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h
index 87cc3847c..f64b7d059 100644
--- a/src/smt/smt_relevancy.h
+++ b/src/smt/smt_relevancy.h
@@ -29,7 +29,7 @@ namespace smt {
         void mark_as_relevant(relevancy_propagator & rp, expr * n);
         void mark_args_as_relevant(relevancy_propagator & rp, app * n);
     public:
-        virtual ~relevancy_eh() {}
+        virtual ~relevancy_eh() = default;
         /**
            \brief This method is invoked when n is marked as relevant.
         */
@@ -87,7 +87,7 @@ namespace smt {
         context & m_context;
     public:
         relevancy_propagator(context & ctx);
-        virtual ~relevancy_propagator() {}
+        virtual ~relevancy_propagator() = default;
 
         context & get_context() { return m_context; }
 
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index af7b97c72..32a9314f0 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -294,7 +294,7 @@ namespace smt {
                 m_bound_kind(k),
                 m_atom(a) {
             }
-            virtual ~bound() {}
+            virtual ~bound() = default;
             theory_var get_var() const { return m_var; }
             bound_kind get_bound_kind() const { return static_cast<bound_kind>(m_bound_kind); }
             bool is_atom() const { return m_atom; }
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index e26db51d0..5a5e1e6f2 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -42,7 +42,7 @@ namespace smt {
 
         class atom {
         public:
-            virtual ~atom() {}
+            virtual ~atom() = default;
             virtual bool is_bit() const = 0;
         };
 
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index fb5a821d5..48acb6ad8 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -222,7 +222,7 @@ namespace smt {
 
         class apply {
         public:
-            virtual ~apply() {}
+            virtual ~apply() = default;
             virtual void operator()(theory_seq& th) = 0;
         };
 
diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h
index 53ffd2a1d..86941f590 100644
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -45,7 +45,7 @@ protected:
     double      m_time;
 public:
     check_sat_result():m_ref_count(0), m_status(l_undef), m_time(0) {}
-    virtual ~check_sat_result() {}
+    virtual ~check_sat_result() = default;
     void inc_ref() { m_ref_count++; }
     void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
     lbool set_status(lbool r) { return m_status = r; }
diff --git a/src/solver/progress_callback.h b/src/solver/progress_callback.h
index e8c463609..f49609daf 100644
--- a/src/solver/progress_callback.h
+++ b/src/solver/progress_callback.h
@@ -20,7 +20,7 @@ Revision History:
 
 class progress_callback {
 public:
-    virtual ~progress_callback() {}
+    virtual ~progress_callback() = default;
     
     // Called on every check for resource limit exceeded (much more frequent).
     virtual void fast_progress_sample() {}
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 09daf3b29..8b7d56a8c 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -29,7 +29,7 @@ class model_converter;
 
 class solver_factory {
 public:
-    virtual ~solver_factory() {}
+    virtual ~solver_factory() = default;
     virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) = 0;
 };
 
@@ -113,7 +113,7 @@ public:
     virtual void set_phase(expr* e) = 0;
     virtual void move_to_front(expr* e) = 0; 
 
-    class phase { public: virtual ~phase() {} };
+    class phase { public: virtual ~phase() = default; };
     
     virtual phase* get_phase() = 0;
 
diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp
index b0e6be1bd..3a2f85831 100644
--- a/src/tactic/bv/bv_bound_chk_tactic.cpp
+++ b/src/tactic/bv/bv_bound_chk_tactic.cpp
@@ -147,7 +147,7 @@ public:
     imp(ast_manager & m, params_ref const & p, bv_bound_chk_stats& stats)
         : m_rw(m, p, stats) {    }
 
-    virtual ~imp() {    }
+    virtual ~imp() = default;
 
     ast_manager& m() { return m_rw.m(); }
 
diff --git a/src/tactic/converter.h b/src/tactic/converter.h
index 60602557e..bbd30c351 100644
--- a/src/tactic/converter.h
+++ b/src/tactic/converter.h
@@ -26,7 +26,7 @@ class converter {
     unsigned m_ref_count;
 public:
     converter():m_ref_count(0) {}
-    virtual ~converter() {}
+    virtual ~converter() = default;
 
     void inc_ref() { ++m_ref_count;  }
 
diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h
index 0beced06e..c8e34f33d 100644
--- a/src/tactic/core/ctx_simplify_tactic.h
+++ b/src/tactic/core/ctx_simplify_tactic.h
@@ -26,7 +26,7 @@ public:
     class simplifier {
         goal_num_occurs* m_occs;
     public:
-        virtual ~simplifier() {}
+        virtual ~simplifier() = default;
         virtual bool assert_expr(expr * t, bool sign) = 0;
         virtual bool simplify(expr* t, expr_ref& result) = 0;
         virtual bool may_simplify(expr* t) { return true; }
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index b5d5e1ce9..43e13d961 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -64,7 +64,7 @@ public:
 
 class dom_simplifier {
  public:
-    virtual ~dom_simplifier() {}
+    virtual ~dom_simplifier() = default;
     /**
        \brief assert_expr performs an implicit push
     */
diff --git a/src/tactic/probe.h b/src/tactic/probe.h
index ae2879163..4d1af66a8 100644
--- a/src/tactic/probe.h
+++ b/src/tactic/probe.h
@@ -44,7 +44,7 @@ private:
 
 public:
     probe():m_ref_count(0) {}
-    virtual ~probe() {}
+    virtual ~probe() = default;
 
     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/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h
index 46b5eda8a..18d71b514 100644
--- a/src/tactic/user_propagator_base.h
+++ b/src/tactic/user_propagator_base.h
@@ -53,7 +53,7 @@ namespace user_propagator {
     class core {
     public:
 
-        virtual ~core() {}
+        virtual ~core() = default;
         
         virtual void user_propagate_init(
             void* ctx, 
diff --git a/src/test/ex.cpp b/src/test/ex.cpp
index 444431475..10b5f8a90 100644
--- a/src/test/ex.cpp
+++ b/src/test/ex.cpp
@@ -21,7 +21,7 @@ Revision History:
 
 class ex {
 public:
-    virtual ~ex() {}
+    virtual ~ex() = default;
     virtual char const * msg() const = 0;
 };
 
diff --git a/src/util/cmd_context_types.h b/src/util/cmd_context_types.h
index 5195333fc..b8c3d4758 100644
--- a/src/util/cmd_context_types.h
+++ b/src/util/cmd_context_types.h
@@ -87,7 +87,7 @@ protected:
     int    m_pos;
 public:
     cmd(char const * n):m_name(n), m_line(0), m_pos(0) {}
-    virtual ~cmd() {}
+    virtual ~cmd() = default;
     virtual void reset(cmd_context & ctx) {}
     virtual void finalize(cmd_context & ctx) {}
     virtual symbol get_name() const { return m_name; }
diff --git a/src/util/event_handler.h b/src/util/event_handler.h
index 8993162e6..cabbca4c9 100644
--- a/src/util/event_handler.h
+++ b/src/util/event_handler.h
@@ -31,7 +31,7 @@ protected:
     event_handler_caller_t m_caller_id;
 public:
     event_handler(): m_caller_id(UNSET_EH_CALLER) {}
-    virtual ~event_handler() {}
+    virtual ~event_handler() = default;
     virtual void operator()(event_handler_caller_t caller_id) = 0;
     event_handler_caller_t caller_id() const { return m_caller_id; }
 };
diff --git a/src/util/trail.h b/src/util/trail.h
index 9a7ec4303..20a525cf7 100644
--- a/src/util/trail.h
+++ b/src/util/trail.h
@@ -26,7 +26,7 @@ Revision History:
 
 class trail {
 public:
-    virtual ~trail() {}
+    virtual ~trail() = default;
     virtual void undo() = 0;
 };
 
diff --git a/src/util/z3_exception.h b/src/util/z3_exception.h
index 1d54fb7b5..b6875257c 100644
--- a/src/util/z3_exception.h
+++ b/src/util/z3_exception.h
@@ -22,7 +22,7 @@ Notes:
 
 class z3_exception {
 public:
-    virtual ~z3_exception() {}
+    virtual ~z3_exception() = default;
     virtual char const * msg() const = 0;
     virtual unsigned error_code() const;
     bool has_error_code() const;