diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp
index 79cad2fb2..5ef783c93 100644
--- a/src/ackermannization/ackermannize_bv_tactic.cpp
+++ b/src/ackermannization/ackermannize_bv_tactic.cpp
@@ -29,8 +29,6 @@ public:
         updt_params(p);
     }
 
-    ~ackermannize_bv_tactic() override { }
-
     char const* name() const override { return "ackermannize_bv"; }
 
     void operator()(goal_ref const & g, goal_ref_buffer & result) override {
diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp
index 78fe6bef0..a38455e03 100644
--- a/src/ackermannization/ackr_model_converter.cpp
+++ b/src/ackermannization/ackr_model_converter.cpp
@@ -40,8 +40,6 @@ public:
           fixed_model(false)
     { }
 
-    ~ackr_model_converter() override { }
-
     void get_units(obj_map<expr, bool>& units) override { units.reset(); }
 
     void operator()(model_ref & md) override {
diff --git a/src/ackermannization/lackr_model_converter_lazy.cpp b/src/ackermannization/lackr_model_converter_lazy.cpp
index ec54b1d19..991fbed8e 100644
--- a/src/ackermannization/lackr_model_converter_lazy.cpp
+++ b/src/ackermannization/lackr_model_converter_lazy.cpp
@@ -28,8 +28,6 @@ public:
         , model_constructor(lmc)
     { }
 
-    ~lackr_model_converter_lazy() override { }
-
     void operator()(model_ref & md) override {
         SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
         SASSERT(model_constructor.get());
diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp
index 969de515c..8416b0636 100644
--- a/src/api/api_algebraic.cpp
+++ b/src/api/api_algebraic.cpp
@@ -344,7 +344,6 @@ extern "C" {
         scoped_anum_vector const & m_as;
     public:
         vector_var2anum(scoped_anum_vector & as):m_as(as) {}
-        ~vector_var2anum() override {}
         algebraic_numbers::manager & m() const override { return m_as.m(); }
         bool contains(polynomial::var x) const override { return static_cast<unsigned>(x) < m_as.size(); }
         algebraic_numbers::anum const & operator()(polynomial::var x) const override { return m_as.get(x); }
diff --git a/src/api/api_ast_vector.h b/src/api/api_ast_vector.h
index fe6203cb9..dc1fcb8e6 100644
--- a/src/api/api_ast_vector.h
+++ b/src/api/api_ast_vector.h
@@ -26,7 +26,6 @@ namespace api {
 struct Z3_ast_vector_ref : public api::object {
     ast_ref_vector  m_ast_vector;
     Z3_ast_vector_ref(api::context& c, ast_manager & m): api::object(c), m_ast_vector(m) {}
-    ~Z3_ast_vector_ref() override {}
 };
 
 inline Z3_ast_vector_ref * to_ast_vector(Z3_ast_vector v) { return reinterpret_cast<Z3_ast_vector_ref *>(v); }
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 8c6227d7d..19b488239 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -52,7 +52,6 @@ namespace api {
             m_context(m, m_register_engine, p),
             m_trail(m) {}
 
-        ~fixedpoint_context() override {}
         family_id get_family_id() const override { return const_cast<datalog::context&>(m_context).get_decl_util().get_family_id(); }
         void set_state(void* state) {
             SASSERT(!m_state);
diff --git a/src/api/api_goal.h b/src/api/api_goal.h
index 86f6a4331..56f48df91 100644
--- a/src/api/api_goal.h
+++ b/src/api/api_goal.h
@@ -23,7 +23,6 @@ Revision History:
 struct Z3_goal_ref : public api::object {
     goal_ref m_goal;
     Z3_goal_ref(api::context& c) : api::object(c) {}
-    ~Z3_goal_ref() override {}
 };
 
 inline Z3_goal_ref * to_goal(Z3_goal g) { return reinterpret_cast<Z3_goal_ref *>(g); }
diff --git a/src/api/api_model.h b/src/api/api_model.h
index c05c86ceb..c04fc088d 100644
--- a/src/api/api_model.h
+++ b/src/api/api_model.h
@@ -23,7 +23,6 @@ Revision History:
 struct Z3_model_ref : public api::object {
     model_ref  m_model;
     Z3_model_ref(api::context& c): api::object(c) {}
-    ~Z3_model_ref() override {}
 };
 
 inline Z3_model_ref * to_model(Z3_model s) { return reinterpret_cast<Z3_model_ref *>(s); }
@@ -34,7 +33,6 @@ struct Z3_func_interp_ref : public api::object {
     model_ref     m_model; // must have it to prevent reference to m_func_interp to be killed.
     func_interp * m_func_interp;
     Z3_func_interp_ref(api::context& c, model * m): api::object(c), m_model(m), m_func_interp(nullptr) {}
-    ~Z3_func_interp_ref() override {}
 };
 
 inline Z3_func_interp_ref * to_func_interp(Z3_func_interp s) { return reinterpret_cast<Z3_func_interp_ref *>(s); }
@@ -46,7 +44,6 @@ struct Z3_func_entry_ref : public api::object {
     func_interp *       m_func_interp;
     func_entry const *  m_func_entry;
     Z3_func_entry_ref(api::context& c, model * m):api::object(c), m_model(m), m_func_interp(nullptr), m_func_entry(nullptr) {}
-    ~Z3_func_entry_ref() override {}
 };
 
 inline Z3_func_entry_ref * to_func_entry(Z3_func_entry s) { return reinterpret_cast<Z3_func_entry_ref *>(s); }
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index 6355642fc..3a1fe7af1 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -47,8 +47,6 @@ extern "C" {
             ctx->register_plist();
             ctx->set_ignore_check(true);
         }
-
-        ~Z3_parser_context_ref() override {}
     };
 
     inline Z3_parser_context_ref * to_parser_context(Z3_parser_context pc) { return reinterpret_cast<Z3_parser_context_ref*>(pc); }
diff --git a/src/api/api_solver.h b/src/api/api_solver.h
index 5214d274c..71b7f9a46 100644
--- a/src/api/api_solver.h
+++ b/src/api/api_solver.h
@@ -51,7 +51,6 @@ struct Z3_solver_ref : public api::object {
 
     Z3_solver_ref(api::context& c, solver_factory * f): 
         api::object(c), m_solver_factory(f), m_solver(nullptr), m_logic(symbol::null), m_eh(nullptr) {}
-    ~Z3_solver_ref() override {}
 
     void assert_expr(expr* e);
     void assert_expr(expr* e, expr* t);
diff --git a/src/api/api_stats.h b/src/api/api_stats.h
index 209daafdd..ff6eeeea2 100644
--- a/src/api/api_stats.h
+++ b/src/api/api_stats.h
@@ -23,7 +23,6 @@ Revision History:
 struct Z3_stats_ref : public api::object {
     statistics m_stats;
     Z3_stats_ref(api::context& c): api::object(c) {}
-    ~Z3_stats_ref() override {}
 };
 
 inline Z3_stats_ref * to_stats(Z3_stats s) { return reinterpret_cast<Z3_stats_ref *>(s); }
diff --git a/src/api/api_tactic.h b/src/api/api_tactic.h
index a4d0f263e..91e2d76ab 100644
--- a/src/api/api_tactic.h
+++ b/src/api/api_tactic.h
@@ -28,13 +28,11 @@ namespace api {
 struct Z3_tactic_ref : public api::object {
     tactic_ref   m_tactic;
     Z3_tactic_ref(api::context& c): api::object(c) {}
-    ~Z3_tactic_ref() override {}
 };
 
 struct Z3_probe_ref : public api::object {
     probe_ref    m_probe;
     Z3_probe_ref(api::context& c):api::object(c) {}
-    ~Z3_probe_ref() override {}
 };
 
 inline Z3_tactic_ref * to_tactic(Z3_tactic g) { return reinterpret_cast<Z3_tactic_ref *>(g); }
@@ -50,7 +48,6 @@ struct Z3_apply_result_ref : public api::object {
     model_converter_ref  m_mc;
     proof_converter_ref  m_pc;
     Z3_apply_result_ref(api::context& c, ast_manager & m);
-    ~Z3_apply_result_ref() override {}
 };
 
 inline Z3_apply_result_ref * to_apply_result(Z3_apply_result g) { return reinterpret_cast<Z3_apply_result_ref *>(g); }
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 51f380243..6fe2c7657 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -107,7 +107,6 @@ class array_decl_plugin : public decl_plugin {
     bool is_array_sort(sort* s) const;
  public:
     array_decl_plugin();
-    ~array_decl_plugin() override {}
 
     decl_plugin * mk_fresh() override {
         return alloc(array_decl_plugin);
diff --git a/src/ast/ast_printer.cpp b/src/ast/ast_printer.cpp
index 7f717df96..46f39ffde 100644
--- a/src/ast/ast_printer.cpp
+++ b/src/ast/ast_printer.cpp
@@ -26,7 +26,6 @@ class simple_ast_printer_context : public ast_printer_context {
     smt2_pp_environment_dbg & env() const { return *(m_env.get()); }
 public:
     simple_ast_printer_context(ast_manager & m):m_manager(m) { m_env = alloc(smt2_pp_environment_dbg, m); }
-    ~simple_ast_printer_context() override {}
     ast_manager & m() const { return m_manager; }
     ast_manager & get_ast_manager() override { return m_manager; }
     void display(std::ostream & out, sort * s, unsigned indent = 0) const override { out << mk_ismt2_pp(s, m(), indent); }
diff --git a/src/ast/ast_printer.h b/src/ast/ast_printer.h
index d57a9b845..37023393f 100644
--- a/src/ast/ast_printer.h
+++ b/src/ast/ast_printer.h
@@ -45,7 +45,6 @@ public:
 
 class ast_printer_context : public ast_printer {
 public:
-    ~ast_printer_context() override {}
     virtual ast_manager & get_ast_manager() = 0;
     virtual std::ostream & regular_stream();
     virtual std::ostream & diagnostic_stream();
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 25c68819a..372eedb8e 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -241,7 +241,6 @@ protected:
 public:
     bv_decl_plugin();
 
-    ~bv_decl_plugin() override {}
     void finalize() override;
 
     decl_plugin * mk_fresh() override { return alloc(bv_decl_plugin); }
diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h
index 39cdbf835..c1cf08719 100644
--- a/src/ast/dl_decl_plugin.h
+++ b/src/ast/dl_decl_plugin.h
@@ -101,7 +101,6 @@ namespace datalog {
     public:
 
         dl_decl_plugin();
-        ~dl_decl_plugin() override {}
 
         decl_plugin * mk_fresh() override { return alloc(dl_decl_plugin); }
         
diff --git a/src/ast/format.cpp b/src/ast/format.cpp
index 4aeaf183d..a14d4b758 100644
--- a/src/ast/format.cpp
+++ b/src/ast/format.cpp
@@ -52,8 +52,6 @@ namespace format_ns {
             m_line_break_ext("cr++") {
         }
         
-        ~format_decl_plugin() override {}
-
         void finalize() override {
             if (m_format_sort)
                 m_manager->dec_ref(m_format_sort);
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index a5bdce3df..19315129a 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -239,7 +239,6 @@ class fpa2bv_converter_wrapped : public fpa2bv_converter {
     fpa2bv_converter_wrapped(ast_manager & m, th_rewriter& rw) :
         fpa2bv_converter(m),
         m_rw(rw) {}
-    ~fpa2bv_converter_wrapped() override {}
     void mk_const(func_decl * f, expr_ref & result) override;
     void mk_rm_const(func_decl * f, expr_ref & result) override;
     app_ref wrap(expr * e);
diff --git a/src/ast/normal_forms/name_exprs.cpp b/src/ast/normal_forms/name_exprs.cpp
index bb2543b3e..c500d92bd 100644
--- a/src/ast/normal_forms/name_exprs.cpp
+++ b/src/ast/normal_forms/name_exprs.cpp
@@ -77,9 +77,6 @@ public:
         m_rw(m, m.proofs_enabled(), m_cfg) {
     }
 
-    ~name_exprs_core() override {
-    }
-
     void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override {
         m_cfg.m_def_exprs  = &new_defs;
         m_cfg.m_def_proofs = &new_def_proofs;
@@ -113,9 +110,6 @@ public:
         name_exprs_core(m, n, m_pred),
         m_pred(m) {
     }
-
-    ~name_quantifier_labels() override {
-    }
 };
 
 name_exprs * mk_quantifier_label_namer(ast_manager & m, defined_names & n) {
@@ -145,9 +139,6 @@ public:
         m_pred(m) {
     }
 
-    ~name_nested_formulas() override {
-    }
-
     void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override {
         m_pred.m_root = n;
         TRACE("name_exprs", tout << "operator()\n";);
diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h
index 372e7b06f..89f566263 100644
--- a/src/ast/pb_decl_plugin.h
+++ b/src/ast/pb_decl_plugin.h
@@ -52,7 +52,6 @@ class pb_decl_plugin : public decl_plugin {
     func_decl * mk_eq(unsigned arity, rational const* coeffs, int k);
 public:
     pb_decl_plugin();
-    ~pb_decl_plugin() override {}
 
     sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override {
         UNREACHABLE();
diff --git a/src/ast/proofs/proof_checker.h b/src/ast/proofs/proof_checker.h
index 27f872d25..591fb1157 100644
--- a/src/ast/proofs/proof_checker.h
+++ b/src/ast/proofs/proof_checker.h
@@ -52,8 +52,6 @@ class proof_checker {
     public:
         hyp_decl_plugin();
 
-        ~hyp_decl_plugin() override {}
-
         void finalize() override;
         
         decl_plugin * mk_fresh() override { return alloc(hyp_decl_plugin); }
diff --git a/src/ast/rewriter/elim_bounds.h b/src/ast/rewriter/elim_bounds.h
index 378ac20cc..99d002f98 100644
--- a/src/ast/rewriter/elim_bounds.h
+++ b/src/ast/rewriter/elim_bounds.h
@@ -68,8 +68,6 @@ public:
         rewriter_tpl<elim_bounds_cfg>(m, m.proofs_enabled(), m_cfg),
         m_cfg(m)
     {} 
-
-    ~elim_bounds_rw() override {}
 };
 
 
diff --git a/src/ast/rewriter/expr_replacer.cpp b/src/ast/rewriter/expr_replacer.cpp
index e822c1775..4fa83bed0 100644
--- a/src/ast/rewriter/expr_replacer.cpp
+++ b/src/ast/rewriter/expr_replacer.cpp
@@ -129,8 +129,6 @@ public:
         m_r(m, p) {
     }
 
-    ~th_rewriter2expr_replacer() override {}
-
     ast_manager & m() const override { return m_r.m(); }
 
     void set_substitution(expr_substitution * s) override { m_r.set_substitution(s); }
diff --git a/src/ast/rewriter/push_app_ite.h b/src/ast/rewriter/push_app_ite.h
index e30feac1c..67c48c7ae 100644
--- a/src/ast/rewriter/push_app_ite.h
+++ b/src/ast/rewriter/push_app_ite.h
@@ -49,7 +49,6 @@ protected:
     bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override;
 public:
     ng_push_app_ite_cfg(ast_manager& m): push_app_ite_cfg(m) {}
-    ~ng_push_app_ite_cfg() override {}
 };
 
 struct push_app_ite_rw : public rewriter_tpl<push_app_ite_cfg> {
diff --git a/src/ast/rewriter/recfun_replace.h b/src/ast/rewriter/recfun_replace.h
index 09ee3c60d..edc0283a8 100644
--- a/src/ast/rewriter/recfun_replace.h
+++ b/src/ast/rewriter/recfun_replace.h
@@ -32,7 +32,6 @@ class recfun_replace : public recfun::replace {
     expr_safe_replace m_replace;
 public:
     recfun_replace(ast_manager& m): m(m), m_replace(m) {}
-    ~recfun_replace() override {}
     void reset() override { m_replace.reset(); }
     void insert(expr* s, expr* t) override { m_replace.insert(s, t); }
     expr_ref operator()(expr* e) override { expr_ref r(m); m_replace(e, r); return r; }
diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h
index d804fa179..daff802e7 100644
--- a/src/ast/special_relations_decl_plugin.h
+++ b/src/ast/special_relations_decl_plugin.h
@@ -40,8 +40,6 @@ class special_relations_decl_plugin : public decl_plugin {
 public:
     special_relations_decl_plugin();
 
-    ~special_relations_decl_plugin() override {}
-
     decl_plugin * mk_fresh() override {
         return alloc(special_relations_decl_plugin);
     }
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index dc8836138..b17bc3641 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -379,8 +379,6 @@ public:
         m_int_real_coercions(":int-real-coercions"),
         m_reproducible_resource_limit(":reproducible-resource-limit") {
     }
-    ~set_get_option_cmd() override {}
-
 };
 
 class set_option_cmd : public set_get_option_cmd {
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 32dd6aee5..644bf5c7b 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -493,7 +493,6 @@ protected:
 
 public:
     pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dtutil(o.m()), m_dlutil(o.m()) {}
-    ~pp_env() override {}
     ast_manager & get_manager() const override { return m_owner.m(); }
     arith_util & get_autil() override { return m_autil; }
     bv_util & get_bvutil() override { return m_bvutil; }
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 1545487c7..5c7058bb5 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -147,7 +147,6 @@ class psort_sort : public psort {
     sort * get_sort() const { return m_sort; }
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override { return m_sort; }
 public:
-    ~psort_sort() override {}
     bool is_sort_wrapper() const override { return true; }
     char const * hcons_kind() const override { return "psort_sort"; }
     unsigned hcons_hash() const override { return m_sort->get_id(); }
@@ -171,7 +170,6 @@ class psort_var : public psort {
     }
     size_t obj_size() const override { return sizeof(psort_var); }
 public:
-    ~psort_var() override {}
     char const * hcons_kind() const override { return "psort_var"; }
     unsigned hcons_hash() const override { return hash_u_u(m_num_params, m_idx); }
     bool hcons_eq(psort const * other) const override {
@@ -233,7 +231,6 @@ class psort_app : public psort {
     }
 
 public:
-    ~psort_app() override {}
     char const * hcons_kind() const override { return "psort_app"; }
     unsigned hcons_hash() const override {
         return get_composite_hash<psort_app*, khasher, chasher>(const_cast<psort_app*>(this), m_args.size());
@@ -800,8 +797,6 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
         m.m().inc_array_ref(n, s);
     }
 
-    ~app_sort_info() override {}
-
     unsigned obj_size() const override { return sizeof(app_sort_info); }
 
     void finalize(pdecl_manager & m) override {
@@ -843,8 +838,6 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
         m_indices(n, s) {
     }
 
-    ~indexed_sort_info() override {}
-
     unsigned obj_size() const override { return sizeof(indexed_sort_info); }
 
     void display(std::ostream & out, pdecl_manager const & m) const override {
diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h
index 4f9c56825..66e1e5e81 100644
--- a/src/cmd_context/pdecl.h
+++ b/src/cmd_context/pdecl.h
@@ -66,7 +66,6 @@ protected:
     psort(unsigned id, unsigned num_params):pdecl(id, num_params), m_inst_cache(nullptr) {}
     bool is_psort() const override { return true; }
     void finalize(pdecl_manager & m) override;
-    ~psort() override {}
     virtual void cache(pdecl_manager & m, sort * const * s, sort * r);
     virtual sort * find(sort * const * s) const;
 public:
@@ -98,7 +97,6 @@ protected:
     sort * find(sort * const * s);
     psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n);
     void finalize(pdecl_manager & m) override;
-    ~psort_decl() override {}
 public:
     virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) = 0;
     virtual sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) { return nullptr; }
@@ -120,7 +118,6 @@ protected:
     psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p);
     size_t obj_size() const override { return sizeof(psort_user_decl); }
     void finalize(pdecl_manager & m) override;
-    ~psort_user_decl() override {}
 public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
     std::ostream& display(std::ostream & out) const override;
@@ -133,7 +130,6 @@ protected:
     decl_kind m_kind;
     psort_builtin_decl(unsigned id, pdecl_manager & m, symbol const & n, family_id fid, decl_kind k);
     size_t obj_size() const override { return sizeof(psort_builtin_decl); }
-    ~psort_builtin_decl() override {}
 public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
     sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) override;
@@ -145,7 +141,6 @@ protected:
     friend class pdecl_manager;
     psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n);
     size_t obj_size() const override { return sizeof(psort_dt_decl); }
-    ~psort_dt_decl() override {}
 public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
     std::ostream& display(std::ostream & out) const override;
@@ -196,7 +191,6 @@ class paccessor_decl : public pdecl {
     accessor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
     symbol const & get_name() const { return m_name; }
     ptype const & get_type() const { return m_type; }
-    ~paccessor_decl() override {}
 public:
     std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
     void display(std::ostream & out, pdatatype_decl const * const * dts) const;
@@ -217,7 +211,6 @@ class pconstructor_decl : public pdecl {
     symbol const & get_name() const { return m_name; }
     symbol const & get_recognizer_name() const { return m_recogniser_name; }
     constructor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
-    ~pconstructor_decl() override {}
 public:
     std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
     void display(std::ostream & out, pdatatype_decl const * const * dts) const;
@@ -234,7 +227,6 @@ class pdatatype_decl : public psort_decl {
     size_t obj_size() const override { return sizeof(pdatatype_decl); }
     bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing);
     datatype_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
-    ~pdatatype_decl() override {}
 public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
     std::ostream& display(std::ostream & out) const override;
@@ -255,7 +247,6 @@ class pdatatypes_decl : public pdecl {
     size_t obj_size() const override { return sizeof(pdatatypes_decl); }
     bool fix_missing_refs(symbol & missing);
     bool instantiate(pdecl_manager & m, sort * const * s);
-    ~pdatatypes_decl() override {}
 public:
     pdatatype_decl const * const * children() const { return m_datatypes.data(); }
     pdatatype_decl * const * begin() const { return m_datatypes.begin(); }
diff --git a/src/cmd_context/simplify_cmd.cpp b/src/cmd_context/simplify_cmd.cpp
index 0c389a78a..d5200374c 100644
--- a/src/cmd_context/simplify_cmd.cpp
+++ b/src/cmd_context/simplify_cmd.cpp
@@ -46,10 +46,7 @@ public:
         p.insert("print_proofs", CPK_BOOL, "(default: false) print a proof showing the original term is equal to the resultant one.");
         p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
     }
-    
-    ~simplify_cmd() override {
-    }
-    
+
     void prepare(cmd_context & ctx) override {
         parametric_cmd::prepare(ctx);
         m_target   = nullptr;
diff --git a/src/math/automata/boolean_algebra.h b/src/math/automata/boolean_algebra.h
index 4bd80af4b..8c1ca55e6 100644
--- a/src/math/automata/boolean_algebra.h
+++ b/src/math/automata/boolean_algebra.h
@@ -38,7 +38,6 @@ public:
 template<class T>
 class boolean_algebra : public positive_boolean_algebra<T> {
 public:
-    ~boolean_algebra() override {}
     virtual T mk_not(T x) = 0;
 };
 
diff --git a/src/math/hilbert/heap_trie.h b/src/math/hilbert/heap_trie.h
index 7d4179de8..fcdce7311 100644
--- a/src/math/hilbert/heap_trie.h
+++ b/src/math/hilbert/heap_trie.h
@@ -80,7 +80,6 @@ class heap_trie {
         Value m_value;
     public:
         leaf(): node(leaf_t) {}
-        ~leaf() override {}
         Value const& get_value() const { return m_value; }
         void set_value(Value const& v) { m_value = v; }
         void display(std::ostream& out, unsigned indent) const override {
@@ -98,9 +97,6 @@ class heap_trie {
     public:
         trie(): node(trie_t) {}
 
-        ~trie() override {
-        }
-
         node* find_or_insert(Key k, node* n) {
             for (unsigned i = 0; i < m_nodes.size(); ++i) {
                 if (m_nodes[i].first == k) {
diff --git a/src/math/subpaving/subpaving.cpp b/src/math/subpaving/subpaving.cpp
index 19dd661c6..e9c72e2d7 100644
--- a/src/math/subpaving/subpaving.cpp
+++ b/src/math/subpaving/subpaving.cpp
@@ -38,7 +38,6 @@ namespace subpaving {
         CTX m_ctx;
     public:
         context_wrapper(reslimit& lim, typename CTX::numeral_manager & m, params_ref const & p, small_object_allocator * a):m_ctx(lim, m, p, a) {}
-        ~context_wrapper() override {}
         unsigned num_vars() const override { return m_ctx.num_vars(); }
         var mk_var(bool is_int) override { return m_ctx.mk_var(is_int); }
         bool is_int(var x) const override { return m_ctx.is_int(x); }
@@ -66,8 +65,6 @@ namespace subpaving {
             m_as(m) 
         {}
 
-        ~context_mpq_wrapper() override {}
-
         unsynch_mpq_manager & qm() const override { return m_ctx.nm(); }
 
         var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override {
@@ -108,8 +105,6 @@ namespace subpaving {
             m_q2(m_qm) {
         }
 
-        ~context_mpf_wrapper() override {}
-
         unsynch_mpq_manager & qm() const override { return m_qm; }
 
         var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override {
@@ -165,8 +160,6 @@ namespace subpaving {
             m_qm(qm) {
         }
 
-        ~context_hwf_wrapper() override {}
-
         unsynch_mpq_manager & qm() const override { return m_qm; }
 
         var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override {
@@ -223,8 +216,6 @@ namespace subpaving {
             m_z2(m_qm) {
         }
 
-        ~context_fpoint_wrapper() override {}
-
         unsynch_mpq_manager & qm() const override { return m_qm; }
 
         var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override {
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index 4aa8f6ccd..639528a7f 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -37,8 +37,6 @@ class subpaving_tactic : public tactic {
             e2v.mk_inv(m_inv);
         }
 
-        ~display_var_proc() override {}
-        
         ast_manager & m() const { return m_inv.get_manager(); }
         
         void operator()(std::ostream & out, subpaving::var x) const override {
diff --git a/src/model/array_factory.h b/src/model/array_factory.h
index c4bfc05df..c77e619c9 100644
--- a/src/model/array_factory.h
+++ b/src/model/array_factory.h
@@ -32,8 +32,6 @@ class array_factory : public struct_factory {
 public:
     array_factory(ast_manager & m, model_core & md);
 
-    ~array_factory() override {}
-
     expr * get_some_value(sort * s) override;
 
     bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override;
diff --git a/src/model/datatype_factory.h b/src/model/datatype_factory.h
index 8ee4170e3..b2a6b75d3 100644
--- a/src/model/datatype_factory.h
+++ b/src/model/datatype_factory.h
@@ -32,7 +32,6 @@ class datatype_factory : public struct_factory {
 
 public:
     datatype_factory(ast_manager & m, model_core & md);
-    ~datatype_factory() override {}
     expr * get_some_value(sort * s) override;
     expr * get_fresh_value(sort * s) override;
 };
diff --git a/src/model/fpa_factory.h b/src/model/fpa_factory.h
index ff2f18e35..1c2c98b25 100644
--- a/src/model/fpa_factory.h
+++ b/src/model/fpa_factory.h
@@ -34,8 +34,6 @@ class fpa_value_factory : public value_factory {
         value_factory(m, fid),
         m_util(m) {}
     
-    ~fpa_value_factory() override {}
-    
     expr * get_some_value(sort * s) override {
         mpf_manager & mpfm = m_util.fm();
         
diff --git a/src/model/numeral_factory.h b/src/model/numeral_factory.h
index 6d805dd90..174ea8757 100644
--- a/src/model/numeral_factory.h
+++ b/src/model/numeral_factory.h
@@ -25,7 +25,6 @@ Revision History:
 class numeral_factory : public simple_factory<rational> {
 public:
     numeral_factory(ast_manager & m, family_id fid):simple_factory<rational>(m, fid) {}
-    ~numeral_factory() override {}
 };    
 
 class arith_factory : public numeral_factory {
diff --git a/src/model/value_factory.h b/src/model/value_factory.h
index 8df61c181..cf56439d9 100644
--- a/src/model/value_factory.h
+++ b/src/model/value_factory.h
@@ -230,7 +230,6 @@ class user_sort_factory : public simple_factory<unsigned> {
     app * mk_value_core(unsigned const & val, sort * s) override;
 public:
     user_sort_factory(ast_manager & m);
-    ~user_sort_factory() override {}
 
     /**
        \brief Make the universe of \c s finite, by preventing new
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 01523e8d2..f6ce39518 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -159,8 +159,6 @@ namespace datalog {
     public:
         restore_rules(context& ctx, rule_set& r): ctx(ctx), m_old_rules(alloc(rule_set, r)) {}
 
-        ~restore_rules() override {}
-
         void undo() override {
             ctx.replace_rules(*m_old_rules);
             reset();
@@ -173,7 +171,6 @@ namespace datalog {
         unsigned m_old_size;
     public:
         restore_vec_size_trail(Vec& v): m_vector(v), m_old_size(v.size()) {}
-        ~restore_vec_size_trail() override {}
         void undo() override { m_vector.shrink(m_old_size); }
     };
 
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index c35cfd58a..e9ee4c690 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -105,7 +105,6 @@ namespace datalog {
     class rel_context_base : public engine_base {
     public:
         rel_context_base(ast_manager& m, char const* name): engine_base(m, name) {}
-        ~rel_context_base() override {}
         virtual relation_manager & get_rmanager() = 0;
         virtual const relation_manager & get_rmanager() const = 0;
         virtual relation_base & get_relation(func_decl * pred) = 0;
@@ -141,7 +140,6 @@ namespace datalog {
             context const& ctx;
         public:
             contains_pred(context& ctx): ctx(ctx) {}
-            ~contains_pred() override {}
 
             bool operator()(expr* e) override {
                 return ctx.is_predicate(e);
diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp
index ff2210610..24b109f35 100644
--- a/src/muz/rel/check_relation.cpp
+++ b/src/muz/rel/check_relation.cpp
@@ -190,7 +190,6 @@ namespace datalog {
                  const unsigned * cols1, const unsigned * cols2)
             : convenient_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2), m_join(j) 
         {}
-        ~join_fn() override {}
         relation_base * operator()(const relation_base & r1, const relation_base & r2) override {
             check_relation const& t1 = get(r1);
             check_relation const& t2 = get(r2);
@@ -219,7 +218,6 @@ namespace datalog {
             : convenient_join_project_fn(o1_sig, o2_sig, col_cnt, cols1, cols2,
                                          removed_col_cnt, removed_cols), m_join(j) 
         {}
-        ~join_project_fn() override {}
         relation_base * operator()(const relation_base & r1, const relation_base & r2) override {
             check_relation const& t1 = get(r1);
             check_relation const& t2 = get(r2);
@@ -527,8 +525,6 @@ namespace datalog {
               m_filter(f) {
         }
 
-        ~filter_identical_fn() override {}
-        
         void operator()(relation_base & _r) override {
             check_relation& r = get(_r);
             check_relation_plugin& p = r.get_plugin();            
@@ -563,8 +559,6 @@ namespace datalog {
             m_condition(condition) {
         }
 
-        ~filter_interpreted_fn() override {}
-        
         void operator()(relation_base & tb) override {
             check_relation& r = get(tb);
             check_relation_plugin& p = r.get_plugin();            
@@ -590,8 +584,6 @@ namespace datalog {
               m_project(p) {
         }
 
-        ~project_fn() override {}
-
         relation_base * operator()(const relation_base & tb) override {
             check_relation const& t = get(tb);
             check_relation_plugin& p = t.get_plugin();
@@ -618,8 +610,6 @@ namespace datalog {
               m_permute(permute) {
         }
 
-        ~rename_fn() override {}
-
         relation_base * operator()(const relation_base & _t) override {
             check_relation const& t = get(_t);
             check_relation_plugin& p = t.get_plugin();            
@@ -647,7 +637,6 @@ namespace datalog {
             m_val(val),
             m_col(col)
         {}
-        ~filter_equal_fn() override { }
         void operator()(relation_base & tb) override {
             check_relation & t = get(tb);
             check_relation_plugin& p = t.get_plugin();
@@ -760,8 +749,6 @@ namespace datalog {
             m_cond(cond),
             m_xform(xform)
         {}
-        
-        ~filter_proj_fn() override {}
 
         relation_base* operator()(const relation_base & tb) override {
             check_relation const & t = get(tb);
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index 909539a85..f0634f0d5 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -799,7 +799,6 @@ namespace datalog {
     protected:
         relation_base(relation_plugin & plugin, const relation_signature & s)
             : base_ancestor(plugin, s) {}
-        ~relation_base() override {}
     public:
         virtual relation_base * complement(func_decl* p) const = 0;
 
@@ -1040,7 +1039,6 @@ namespace datalog {
     protected:
         table_base(table_plugin & plugin, const table_signature & s)
             : base_ancestor(plugin, s) {}
-        ~table_base() override {}
     public:
         table_base * clone() const override;
         virtual table_base * complement(func_decl* p, const table_element * func_columns = nullptr) const;
diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp
index 07921a3be..a991c9e6c 100644
--- a/src/muz/rel/dl_finite_product_relation.cpp
+++ b/src/muz/rel/dl_finite_product_relation.cpp
@@ -794,8 +794,6 @@ namespace datalog {
                 m_delta_indexes(delta_indexes),
                 m_delta_rels(delta_rels) {}
 
-            ~union_mapper() override {}
-
             bool operator()(table_element * func_columns) override {
                 relation_base & otgt_orig = m_tgt.get_inner_rel(func_columns[0]);
                 const relation_base & osrc = m_src.get_inner_rel(func_columns[1]);
diff --git a/src/muz/rel/dl_lazy_table.h b/src/muz/rel/dl_lazy_table.h
index f9a846c3a..56bfc961f 100644
--- a/src/muz/rel/dl_lazy_table.h
+++ b/src/muz/rel/dl_lazy_table.h
@@ -128,8 +128,6 @@ namespace datalog {
             m_ref(t)
         {}
 
-        ~lazy_table() override {}
-
         lazy_table_plugin& get_lplugin() const { 
             return dynamic_cast<lazy_table_plugin&>(table_base::get_plugin()); 
         }
@@ -164,7 +162,6 @@ namespace datalog {
             m_table = table;
             // SASSERT(&p.m_plugin == &table->get_lplugin());
         }
-        ~lazy_table_base() override {}
         lazy_table_kind kind() const override { return LAZY_TABLE_BASE; }
         table_base* force() override { return m_table.get(); }
     };
@@ -183,7 +180,6 @@ namespace datalog {
               m_cols2(col_cnt, cols2),
               m_t1(t1.get_ref()),
               m_t2(t2.get_ref()) { }
-        ~lazy_table_join() override {}
         lazy_table_kind kind() const override { return LAZY_TABLE_JOIN; }
         unsigned_vector const& cols1() const { return m_cols1; }
         unsigned_vector const& cols2() const { return m_cols2; }
@@ -201,7 +197,6 @@ namespace datalog {
             : lazy_table_ref(src.get_lplugin(), sig), 
               m_cols(col_cnt, cols), 
               m_src(src.get_ref()) {}
-        ~lazy_table_project() override {}
         
         lazy_table_kind kind() const override { return LAZY_TABLE_PROJECT; }
         unsigned_vector const& cols() const { return m_cols; }
@@ -217,8 +212,7 @@ namespace datalog {
             : lazy_table_ref(src.get_lplugin(), sig), 
               m_cols(col_cnt, cols), 
               m_src(src.get_ref()) {}
-        ~lazy_table_rename() override {}
-        
+
         lazy_table_kind kind() const override { return LAZY_TABLE_RENAME; }
         unsigned_vector const& cols() const { return m_cols; }
         lazy_table_ref* src() const { return m_src.get(); }
@@ -231,8 +225,7 @@ namespace datalog {
     public:
         lazy_table_filter_identical(unsigned col_cnt, const unsigned * cols, lazy_table const& src)
             : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.get_ref()) {}
-        ~lazy_table_filter_identical() override {}
-        
+
         lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_IDENTICAL; }
         unsigned_vector const& cols() const { return m_cols; }
         lazy_table_ref* src() const { return m_src.get(); }
@@ -249,8 +242,7 @@ namespace datalog {
             m_col(col), 
             m_value(value), 
             m_src(src.get_ref()) {}
-        ~lazy_table_filter_equal() override {}
-        
+
         lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_EQUAL; }
         unsigned        col() const { return m_col; }
         table_element   value() const { return m_value; }
@@ -265,8 +257,7 @@ namespace datalog {
         lazy_table_filter_interpreted(lazy_table const& src, app* condition)
             : lazy_table_ref(src.get_lplugin(), src.get_signature()), 
               m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.get_ref()) {}
-        ~lazy_table_filter_interpreted() override {}
-        
+
         lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_INTERPRETED; }
         app* condition() const { return m_condition; }        
         lazy_table_ref* src() const { return m_src.get(); }
@@ -287,7 +278,6 @@ namespace datalog {
             m_src(src.get_ref()), 
             m_cols1(c1),
             m_cols2(c2) {}
-        ~lazy_table_filter_by_negation() override {}
         lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_BY_NEGATION; }
         lazy_table_ref* tgt() const { return m_tgt.get(); }
         lazy_table_ref* src() const { return m_src.get(); }
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 3b32a1532..51e7f4ac6 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -1589,8 +1589,6 @@ namespace datalog {
             m_union_fn = plugin.mk_union_fn(t, *m_aux_table, static_cast<table_base *>(nullptr));
         }
 
-        ~default_table_map_fn() override {}
-
         void operator()(table_base & t) override {
             SASSERT(t.get_signature()==m_aux_table->get_signature());
             if(!m_aux_table->empty()) {
@@ -1644,8 +1642,6 @@ namespace datalog {
             m_former_row.resize(get_result_signature().size());
         }
 
-        ~default_table_project_with_reduce_fn() override {}
-
         virtual void modify_fact(table_fact & f) const {
             unsigned ofs=1;
             unsigned r_i=1;
diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp
index 1481b5184..9f3304e7a 100644
--- a/src/muz/rel/dl_sparse_table.cpp
+++ b/src/muz/rel/dl_sparse_table.cpp
@@ -406,8 +406,6 @@ namespace datalog {
             m_key_fact.resize(t.get_signature().size());
         }
 
-        ~full_signature_key_indexer() override {}
-
         query_result get_matching_offsets(const key_value & key) const override {
             unsigned key_len = m_key_cols.size();
             for (unsigned i=0; i<key_len; i++) {
diff --git a/src/muz/spacer/spacer_generalizers.h b/src/muz/spacer/spacer_generalizers.h
index daa9dfbf2..ae1e53259 100644
--- a/src/muz/spacer/spacer_generalizers.h
+++ b/src/muz/spacer/spacer_generalizers.h
@@ -29,7 +29,6 @@ namespace spacer {
 class lemma_sanity_checker : public lemma_generalizer {
   public:
     lemma_sanity_checker(context &ctx) : lemma_generalizer(ctx) {}
-    ~lemma_sanity_checker() override {}
     void operator()(lemma_ref &lemma) override;
 };
 
@@ -59,7 +58,6 @@ class lemma_bool_inductive_generalizer : public lemma_generalizer {
                                      bool array_only = false)
         : lemma_generalizer(ctx), m_failure_limit(failure_limit),
           m_array_only(array_only) {}
-    ~lemma_bool_inductive_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
 
     void collect_statistics(statistics &st) const override;
@@ -83,7 +81,6 @@ class unsat_core_generalizer : public lemma_generalizer {
 
   public:
     unsat_core_generalizer(context &ctx) : lemma_generalizer(ctx) {}
-    ~unsat_core_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
 
     void collect_statistics(statistics &st) const override;
@@ -96,14 +93,12 @@ class lemma_array_eq_generalizer : public lemma_generalizer {
 
   public:
     lemma_array_eq_generalizer(context &ctx) : lemma_generalizer(ctx) {}
-    ~lemma_array_eq_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
 };
 
 class lemma_eq_generalizer : public lemma_generalizer {
   public:
     lemma_eq_generalizer(context &ctx) : lemma_generalizer(ctx) {}
-    ~lemma_eq_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
 };
 
@@ -130,7 +125,6 @@ class lemma_quantifier_generalizer : public lemma_generalizer {
 
   public:
     lemma_quantifier_generalizer(context &ctx, bool normalize_cube = true);
-    ~lemma_quantifier_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
 
     void collect_statistics(statistics &st) const override;
@@ -174,7 +168,6 @@ class limit_num_generalizer : public lemma_generalizer {
 
   public:
     limit_num_generalizer(context &ctx, unsigned failure_limit);
-    ~limit_num_generalizer() override {}
 
     void operator()(lemma_ref &lemma) override;
 
diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h
index 739588c6b..8b75adf88 100644
--- a/src/muz/spacer/spacer_iuc_solver.h
+++ b/src/muz/spacer/spacer_iuc_solver.h
@@ -88,8 +88,6 @@ public:
         m_old_hyp_reducer(old_hyp_reducer)
     {}
 
-    ~iuc_solver() override {}
-
     /* iuc solver specific */
     virtual void get_iuc(expr_ref_vector &core);
     void set_split_literals(bool v) { m_split_literals = v; }
diff --git a/src/muz/transforms/dl_mk_karr_invariants.cpp b/src/muz/transforms/dl_mk_karr_invariants.cpp
index 4436368ce..18d67f549 100644
--- a/src/muz/transforms/dl_mk_karr_invariants.cpp
+++ b/src/muz/transforms/dl_mk_karr_invariants.cpp
@@ -105,8 +105,6 @@ namespace datalog {
         
         add_invariant_model_converter(ast_manager& m): m(m), a(m), m_funcs(m), m_invs(m) {}
 
-        ~add_invariant_model_converter() override { }
-
         void add(func_decl* p, expr* inv) {
             if (!m.is_true(inv)) {
                 m_funcs.push_back(p);
diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
index a0ceb8c73..b8a68a443 100644
--- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
@@ -46,8 +46,6 @@ namespace datalog {
         qa_model_converter(ast_manager& m):
             m(m), m_old_funcs(m), m_new_funcs(m) {}
 
-        ~qa_model_converter() override {}
-
         model_converter * translate(ast_translation & translator) override {
             return alloc(qa_model_converter, m);
         }
diff --git a/src/muz/transforms/dl_mk_rule_inliner.h b/src/muz/transforms/dl_mk_rule_inliner.h
index feae5405b..c0693fde0 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.h
+++ b/src/muz/transforms/dl_mk_rule_inliner.h
@@ -195,7 +195,6 @@ namespace datalog {
             m_head_visitor(ctx, m_subst),
             m_tail_visitor(ctx, m_subst)
         {}
-        ~mk_rule_inliner() 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 efa932fec..38305a04e 100644
--- a/src/muz/transforms/dl_mk_scale.cpp
+++ b/src/muz/transforms/dl_mk_scale.cpp
@@ -30,8 +30,6 @@ namespace datalog {
     public:
         scale_model_converter(ast_manager& m): m(m), m_trail(m), a(m) {}
 
-        ~scale_model_converter() override {}
-
         void add_new2old(func_decl* new_f, func_decl* old_f) {
             m_trail.push_back(old_f);
             m_trail.push_back(new_f);
diff --git a/src/muz/transforms/dl_mk_slice.h b/src/muz/transforms/dl_mk_slice.h
index 4a6d707f0..807c6dac4 100644
--- a/src/muz/transforms/dl_mk_slice.h
+++ b/src/muz/transforms/dl_mk_slice.h
@@ -99,8 +99,6 @@ namespace datalog {
          */
         mk_slice(context & ctx);
 
-        ~mk_slice() override { }
-        
         rule_set * operator()(rule_set const & source) override;
 
         func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; }
diff --git a/src/nlsat/nlsat_assignment.h b/src/nlsat/nlsat_assignment.h
index 3f4c3b95a..6729b73cd 100644
--- a/src/nlsat/nlsat_assignment.h
+++ b/src/nlsat/nlsat_assignment.h
@@ -32,7 +32,6 @@ namespace nlsat {
         bool_vector      m_assigned;
     public:
         assignment(anum_manager & _m):m_values(_m) {}
-        ~assignment() override {}
         anum_manager & am() const { return m_values.m(); }
         void swap(assignment & other) {
             m_values.swap(other.m_values);
diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp
index 20cc028aa..1789f0675 100644
--- a/src/opt/maxcore.cpp
+++ b/src/opt/maxcore.cpp
@@ -100,7 +100,6 @@ private:
     struct lns_maxcore : public lns_context {
         maxcore& i;
         lns_maxcore(maxcore& i) :i(i) {}
-        ~lns_maxcore() override {}
         void update_model(model_ref& mdl) override { i.update_assignment(mdl); }
         void relax_cores(vector<expr_ref_vector> const& cores) override { i.relax_cores(cores); }
         rational cost(model& mdl) override { return i.cost(mdl); }
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 2f8992e01..72195467f 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -85,7 +85,6 @@ namespace opt {
     public:
         maxsmt_solver_base(maxsat_context& c, vector<soft>& soft, unsigned index);
         
-        ~maxsmt_solver_base() override {}
         rational get_lower() const override { return m_lower; }
         rational get_upper() const override { return m_upper; }
         bool get_assignment(unsigned index) const override { return m_soft[index].is_true(); }
diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index 41f7bedb3..1daed0e3b 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -56,9 +56,6 @@ public:
         m_opt(opt)
     {}
 
-    ~assert_soft_cmd() override {
-    }
-
     void reset(cmd_context & ctx) override {
         m_idx = 0; 
         m_formula = nullptr;
diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h
index a814ac0f8..ab5a90237 100644
--- a/src/opt/opt_pareto.h
+++ b/src/opt/opt_pareto.h
@@ -87,7 +87,6 @@ namespace opt {
                    params_ref & p):
             pareto_base(m, cb, s, p) {            
         }
-        ~gia_pareto() override {}
 
         lbool operator()() override;
     };
@@ -101,7 +100,6 @@ namespace opt {
                    params_ref & p):
             pareto_base(m, cb, s, p) {            
         }
-        ~oia_pareto() override {}
 
         lbool operator()() override;
     };
diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp
index 962369bf2..da25e2285 100644
--- a/src/opt/sortmax.cpp
+++ b/src/opt/sortmax.cpp
@@ -39,8 +39,6 @@ namespace opt {
         sortmax(maxsat_context& c, vector<soft>& s, unsigned index): 
             maxsmt_solver_base(c, s, index), m_sort(*this), m_trail(m), m_fresh(m) {}
 
-        ~sortmax() override {}
-
         lbool operator()() override {
             if (!init()) 
                 return l_undef;
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 1fbd26cb8..1fb6c05dd 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -49,8 +49,6 @@ namespace opt {
             m_trail(m),
             m_defs(m) {}
 
-        ~wmax() override {}
-
         lbool operator()() override {
             TRACE("opt", tout << "weighted maxsat\n";);
             scoped_ensure_theory wth(*this);
diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp
index 4a4997de6..e86e42091 100644
--- a/src/qe/nlarith_util.cpp
+++ b/src/qe/nlarith_util.cpp
@@ -1616,7 +1616,6 @@ namespace nlarith {
         public:
             simple_branch(ast_manager& m, app* cnstr):
               m_cnstr(cnstr, m), m_atoms(m) {}
-            ~simple_branch() override {}
             app* get_constraint() override { return m_cnstr.get(); }
             void get_updates(ptr_vector<app>& atoms, svector<util::atom_update>& updates) override {
                 for (unsigned i = 0; i < m_atoms.size(); ++i) {
@@ -1636,7 +1635,6 @@ namespace nlarith {
         public:
             ins_rem_branch(ast_manager& m, app* a, app* r, app* cnstr):
               simple_branch(m, cnstr) { insert(a); remove(r); }             
-            ~ins_rem_branch() override {}
         };
 
         /**
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 37924496a..3a1fa19c6 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -835,9 +835,6 @@ namespace qe {
             m_nftactic = mk_tseitin_cnf_tactic(m);
         }
 
-        ~nlqsat() override {
-        }
-
         char const* name() const override { return "nlqsat"; }
 
         void updt_params(params_ref const & p) override {
diff --git a/src/qe/qe_array_plugin.cpp b/src/qe/qe_array_plugin.cpp
index 43d2f9686..ce0e61d02 100644
--- a/src/qe/qe_array_plugin.cpp
+++ b/src/qe/qe_array_plugin.cpp
@@ -27,9 +27,6 @@ namespace qe {
         {
         }
 
-        ~array_plugin() override {}
-
-        
         void assign(contains_app& x, expr* fml, rational const& vl) override {
             UNREACHABLE();
         }
diff --git a/src/qe/qe_cmd.cpp b/src/qe/qe_cmd.cpp
index f708d5223..12605defd 100644
--- a/src/qe/qe_cmd.cpp
+++ b/src/qe/qe_cmd.cpp
@@ -26,9 +26,6 @@ public:
         p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
     }
     
-    ~qe_cmd() override {
-    }
-    
     void prepare(cmd_context & ctx) override {
         parametric_cmd::prepare(ctx);
         m_target   = nullptr;
diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h
index d7b825fcd..e35822813 100644
--- a/src/qe/qe_mbi.h
+++ b/src/qe/qe_mbi.h
@@ -106,7 +106,6 @@ namespace qe {
         solver_ref m_solver;
     public:
         prop_mbi_plugin(solver* s);
-        ~prop_mbi_plugin() override {}
         mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
         void block(expr_ref_vector const& lits) override;
     };
@@ -134,7 +133,6 @@ namespace qe {
                          expr_ref_vector& uflits);
     public:
         uflia_mbi(solver* s, solver* emptySolver);
-        ~uflia_mbi() override {}
         mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
         void project(model_ref& mdl, expr_ref_vector& lits);
         void block(expr_ref_vector const& lits) override;
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 3d46ec643..a83cb6a45 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -115,8 +115,6 @@ public:
         return m_solver.get_config().m_incremental;
     }
 
-    ~inc_sat_solver() override {}
-
     solver* translate(ast_manager& dst_m, params_ref const& p) override {
         if (m_num_scopes > 0) {
             throw default_exception("Cannot translate sat solver at non-base level");
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index b72754f4f..5920f70f6 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -313,7 +313,6 @@ namespace bv {
        
     public:
         solver(euf::solver& ctx, theory_id id);
-        ~solver() override {}
         void set_lookahead(sat::lookahead* s) override { }
         void init_search() override {}
         double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;
diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
index 4be554633..fa8b2bc26 100644
--- a/src/sat/smt/q_mam.cpp
+++ b/src/sat/smt/q_mam.cpp
@@ -3744,9 +3744,6 @@ namespace q {
             reset_pp_pc();
         }
 
-        ~mam_impl() override {
-        }
-
         void add_pattern(quantifier * qa, app * mp) override {
             SASSERT(m.is_pattern(mp));
             TRACE("trigger_bug", tout << "adding pattern\n" << mk_ismt2_pp(qa, m) << "\n" << mk_ismt2_pp(mp, m) << "\n";);
diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp
index 52d1a064c..37e2424ce 100644
--- a/src/sat/smt/q_model_fixer.cpp
+++ b/src/sat/smt/q_model_fixer.cpp
@@ -45,7 +45,6 @@ namespace q {
         arith_util   a;
     public:
         arith_projection(ast_manager& m) : projection_function(m), a(m) {}
-        ~arith_projection() override {}
         bool operator()(expr* e1, expr* e2) const override { return lt(a, e1, e2); }
         expr* mk_lt(expr* x, expr* y) override { return a.mk_lt(x, y); }
     };
@@ -54,7 +53,6 @@ namespace q {
         bv_util bvu;
     public:
         ubv_projection(ast_manager& m) : projection_function(m), bvu(m) {}
-        ~ubv_projection() override {}
         bool operator()(expr* e1, expr* e2) const override { return lt(bvu, e1, e2); }
         expr* mk_lt(expr* x, expr* y) override { return m.mk_not(bvu.mk_ule(y, x)); }
     };
diff --git a/src/sat/smt/q_model_fixer.h b/src/sat/smt/q_model_fixer.h
index a843d3825..9653268e6 100644
--- a/src/sat/smt/q_model_fixer.h
+++ b/src/sat/smt/q_model_fixer.h
@@ -95,7 +95,6 @@ namespace q {
     public:
 
         model_fixer(euf::solver& ctx, solver& qs);
-        ~model_fixer() override {}
 
         /**
          * Update model in order to best satisfy quantifiers.
diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h
index 5d6a52c8f..32025888b 100644
--- a/src/sat/smt/q_solver.h
+++ b/src/sat/smt/q_solver.h
@@ -65,7 +65,6 @@ namespace q {
     public:
 
         solver(euf::solver& ctx, family_id fid);
-        ~solver() override {}
         bool is_external(sat::bool_var v) override { return false; }
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override;
         void asserted(sat::literal l) override;
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index 430b1c431..7209fa051 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -189,7 +189,6 @@ namespace euf {
 
     public:
         th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id);
-        ~th_euf_solver() override {}
         virtual theory_var mk_var(enode* n);
         unsigned get_num_vars() const { return m_var2enode.size(); }
         euf::enode* e_internalize(expr* e); 
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 73d8561df..a5d9dec4e 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -93,10 +93,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         updt_params(p);
     }
 
-    ~imp() override {
-    }
-        
-
     sat::cut_simplifier* aig() {
         return m_solver.get_cut_simplifier();
     }
diff --git a/src/sat/tactic/sat2goal.h b/src/sat/tactic/sat2goal.h
index b911f7b47..1e1dfcd5e 100644
--- a/src/sat/tactic/sat2goal.h
+++ b/src/sat/tactic/sat2goal.h
@@ -51,7 +51,6 @@ public:
         
     public:
         mc(ast_manager& m);
-        ~mc() override {}
         // flush model converter from SAT solver to this structure.
         void flush_smc(sat::solver& s, atom2bool_var const& map);
         void operator()(sat::model& m);
diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp
index f251d01ae..b77a38927 100644
--- a/src/smt/arith_eq_adapter.cpp
+++ b/src/smt/arith_eq_adapter.cpp
@@ -67,8 +67,6 @@ namespace smt {
             m_ge(ge) {
         }
 
-        ~arith_eq_relevancy_eh() override {}
-
         void operator()(relevancy_propagator & rp) override {
             if (!rp.is_relevant(m_n1))
                 return;
diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index 42844f575..978f1fbe3 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -346,7 +346,6 @@ namespace smt {
         dyn_ack_clause_del_eh(dyn_ack_manager & m):
             m(m) {
         }
-        ~dyn_ack_clause_del_eh() override {}
         void operator()(ast_manager & _m, clause * cls) override {
             m.del_clause_eh(cls);
             dealloc(this);
diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h
index d0c1b97f2..f069e0a60 100644
--- a/src/smt/proto_model/proto_model.h
+++ b/src/smt/proto_model/proto_model.h
@@ -59,7 +59,6 @@ class proto_model : public model_core {
 
 public:
     proto_model(ast_manager & m, params_ref const & p = params_ref());
-    ~proto_model() override {}
 
     void register_factory(value_factory * f) { m_factories.register_plugin(f); }
 
diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index 2189b64e0..9f5bdb0d4 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -150,8 +150,6 @@ namespace {
             if (!first)
                 out << "\n";            
         }
-
-        ~act_case_split_queue() override {};
     };
 
     /**
@@ -1244,8 +1242,6 @@ namespace {
                 out << "\n";
 
         }
-
-        ~theory_aware_branching_queue() override {};
     };
 }
 
diff --git a/src/smt/smt_for_each_relevant_expr.h b/src/smt/smt_for_each_relevant_expr.h
index ef687ae01..4b4492b7f 100644
--- a/src/smt/smt_for_each_relevant_expr.h
+++ b/src/smt/smt_for_each_relevant_expr.h
@@ -92,7 +92,6 @@ namespace smt {
             for_each_relevant_expr(ctx),
             m_buffer(b) {
         }
-        ~collect_relevant_label_lits() override {}
         void operator()(expr * n) override;
     };
 
@@ -103,7 +102,6 @@ namespace smt {
             for_each_relevant_expr(ctx),
             m_buffer(b) {
         }
-        ~collect_relevant_labels() override {}
         void operator()(expr * n) override;
     };
 
diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h
index 48987e746..b90233792 100644
--- a/src/smt/smt_justification.h
+++ b/src/smt/smt_justification.h
@@ -239,7 +239,6 @@ namespace smt {
             unsigned num_params, parameter* params):
             simple_justification(r, num_lits, lits),
             m_th_id(fid), m_params(num_params, params) {}
-        ~simple_theory_justification() override {}
 
         bool has_del_eh() const override { return !m_params.empty(); }
 
@@ -323,8 +322,6 @@ namespace smt {
                                         unsigned num_eqs, enode_pair const * eqs, 
                                         unsigned num_params = 0, parameter* params = nullptr):
             ext_simple_justification(r, num_lits, lits, num_eqs, eqs), m_th_id(fid), m_params(num_params, params) {}
-            
-        ~ext_theory_simple_justification() override {}
 
         bool has_del_eh() const override { return !m_params.empty(); }
 
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 35b350e79..24ec4d5b9 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1180,7 +1180,6 @@ namespace smt {
             unsigned    m_var_j;
         public:
             f_var(ast_manager& m, func_decl* f, unsigned i, unsigned j) : qinfo(m), m_f(f), m_arg_i(i), m_var_j(j) {}
-            ~f_var() override {}
 
             char const* get_kind() const override {
                 return "f_var";
@@ -1261,7 +1260,6 @@ namespace smt {
                 f_var(m, f, i, j),
                 m_offset(offset, m) {
             }
-            ~f_var_plus_offset() override {}
 
             char const* get_kind() const override {
                 return "f_var_plus_offset";
@@ -1427,7 +1425,6 @@ namespace smt {
 
         public:
             select_var(ast_manager& m, app* s, unsigned i, unsigned j) :qinfo(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {}
-            ~select_var() override {}
 
             char const* get_kind() const override {
                 return "select_var";
@@ -1497,8 +1494,6 @@ namespace smt {
                     std::swap(m_var_i, m_var_j);
             }
 
-            ~var_pair() override {}
-
             bool is_equal(qinfo const* qi) const override {
                 if (qi->get_kind() != get_kind())
                     return false;
@@ -1577,7 +1572,6 @@ namespace smt {
             var_expr_pair(ast_manager& m, unsigned i, expr* t) :
                 qinfo(m),
                 m_var_i(i), m_t(t, m) {}
-            ~var_expr_pair() override {}
 
             bool is_equal(qinfo const* qi) const override {
                 if (qi->get_kind() != get_kind())
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index b67599a99..b0696049b 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -606,9 +606,6 @@ namespace smt {
             m_active(false) {
         }
 
-        ~default_qm_plugin() override {
-        }
-
         void set_manager(quantifier_manager & qm) override {
             SASSERT(m_qm == nullptr);
             m_qm            = &qm;
diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp
index 4b787561d..649d75737 100644
--- a/src/smt/smt_relevancy.cpp
+++ b/src/smt/smt_relevancy.cpp
@@ -52,7 +52,6 @@ namespace smt {
         app * m_parent;
     public:
         and_relevancy_eh(app * p):m_parent(p) {}
-        ~and_relevancy_eh() override {}
         void operator()(relevancy_propagator & rp) override;
     };
 
@@ -60,7 +59,6 @@ namespace smt {
         app * m_parent;
     public:
         or_relevancy_eh(app * p):m_parent(p) {}
-        ~or_relevancy_eh() override {}
         void operator()(relevancy_propagator & rp) override;
     };
 
@@ -68,7 +66,6 @@ namespace smt {
         app * m_parent;
     public:
         ite_relevancy_eh(app * p):m_parent(p) {}
-        ~ite_relevancy_eh() override {}
         void operator()(relevancy_propagator & rp) override;
     };
 
@@ -78,7 +75,6 @@ namespace smt {
         app  * m_else_eq;
     public:
         ite_term_relevancy_eh(app * p, app * then_eq, app * else_eq):m_parent(p), m_then_eq(then_eq), m_else_eq(else_eq) {}
-        ~ite_term_relevancy_eh() override {}
         void operator()(relevancy_propagator & rp) override;
     };
 
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index a1054423a..af7b97c72 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -319,7 +319,6 @@ namespace smt {
         public:
             atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind);
             atom_kind get_atom_kind() const { return static_cast<atom_kind>(m_atom_kind); }
-            ~atom() override {}
             inline inf_numeral const & get_k() const { return m_k; }
             bool_var get_bool_var() const { return m_bvar; }
             bool is_true() const { return m_is_true; }
@@ -341,7 +340,6 @@ namespace smt {
                 m_rhs(rhs) {
                 SASSERT(m_lhs->get_root() == m_rhs->get_root());
             }
-            ~eq_bound() override {}
             bool has_justification() const override { return true; }
             void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override {
                 SASSERT(m_lhs->get_root() == m_rhs->get_root());
@@ -357,7 +355,6 @@ namespace smt {
             friend class theory_arith;
         public:
             derived_bound(theory_var v, inf_numeral const & val, bound_kind k):bound(v, val, k, false) {}
-            ~derived_bound() override {}
             literal_vector const& lits() const { return m_lits; }
             eq_vector const& eqs() const { return m_eqs; }
             bool has_justification() const override { return true; }
@@ -374,7 +371,6 @@ namespace smt {
             friend class theory_arith;
         public:
             justified_derived_bound(theory_var v, inf_numeral const & val, bound_kind k):derived_bound(v, val, k) {}
-            ~justified_derived_bound() override {}
             bool has_justification() const override { return true; }
             void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override;
             void push_lit(literal l, numeral const& coeff) override;
diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp
index 9379c939f..988f3fdad 100644
--- a/src/smt/theory_array_bapa.cpp
+++ b/src/smt/theory_array_bapa.cpp
@@ -450,7 +450,6 @@ namespace smt {
             app*                     m_obj;
         public:
             remove_sz(ast_manager& m, obj_map<app, sz_info*>& tab, app* t): m(m), m_table(tab), m_obj(t) { }
-            ~remove_sz() override {}
             void undo() override { m.dec_ref(m_obj); dealloc(m_table[m_obj]); m_table.remove(m_obj); }
         };
 
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index d1a01c807..1be88a6de 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -890,8 +890,6 @@ namespace smt {
             m_unspecified_else(true) {
         }
 
-        ~array_value_proc() override {}
-     
         void add_entry(unsigned num_args, enode * const * args, enode * value) {
             SASSERT(num_args > 0);
             SASSERT(m_dim == 0 || m_dim == num_args);
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index d73b7a008..e26db51d0 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -56,7 +56,6 @@ namespace smt {
         struct bit_atom : public atom {
             var_pos_occ * m_occs;
             bit_atom():m_occs(nullptr) {}
-            ~bit_atom() override {}
             bool is_bit() const override { return true; }
         };
 
@@ -64,7 +63,6 @@ namespace smt {
             literal    m_var;
             literal    m_def;
             le_atom(literal v, literal d):m_var(v), m_def(d) {}
-            ~le_atom() override {}
             bool is_bit() const override { return false; }
         };
 
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index d11172691..febd2763c 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -823,7 +823,6 @@ namespace smt {
     public:
         datatype_value_proc(func_decl * d):m_constructor(d) {}
         void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); }
-        ~datatype_value_proc() override {}
         void get_dependencies(buffer<model_value_dependency> & result) override {
             result.append(m_dependencies.size(), m_dependencies.data());
         }
diff --git a/src/smt/theory_dummy.h b/src/smt/theory_dummy.h
index 6f2e641fd..817d1fda1 100644
--- a/src/smt/theory_dummy.h
+++ b/src/smt/theory_dummy.h
@@ -46,7 +46,6 @@ namespace smt {
 
     public:
         theory_dummy(context& ctx, family_id fid, char const * name);
-        ~theory_dummy() override {}
 
         theory * mk_fresh(context * new_ctx) override { return alloc(theory_dummy, *new_ctx, get_family_id(), m_name); }
 
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index 9d5df855e..9aa70d9bf 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -47,8 +47,6 @@ namespace smt {
                 m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util),
                 m_ebits(ebits), m_sbits(sbits) {}
 
-            ~fpa_value_proc() override {}
-
             void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
 
             void get_dependencies(buffer<model_value_dependency> & result) override {
@@ -75,7 +73,6 @@ namespace smt {
                 result.append(m_deps);
             }
 
-            ~fpa_rm_value_proc() override {}
             app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
         };
 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 634350a62..9a05ccfbf 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1923,7 +1923,6 @@ public:
     seq_value_proc(theory_seq& th, enode* n, sort* s): th(th), m_node(n), m_sort(s) {
         (void)m_node;
     }
-    ~seq_value_proc() override {}
     void add_unit(enode* n) { 
         m_dependencies.push_back(model_value_dependency(n)); 
         m_source.push_back(unit_source);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index cf7e9da23..fb5a821d5 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -230,7 +230,6 @@ namespace smt {
             expr_ref m_e;
         public:
             replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
-            ~replay_length_coherence() override {}
             void operator()(theory_seq& th) override {
                 th.check_length_coherence(m_e);
                 m_e.reset();
@@ -241,7 +240,6 @@ namespace smt {
             expr_ref m_e;
         public:
             replay_fixed_length(ast_manager& m, expr* e) : m_e(e, m) {}
-            ~replay_fixed_length() override {}
             void operator()(theory_seq& th) override {
                 th.fixed_length(m_e, false, false);
                 m_e.reset();
@@ -252,7 +250,6 @@ namespace smt {
             expr_ref m_e;
         public:
             replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
-            ~replay_axiom() override {}
             void operator()(theory_seq& th) override {
                 th.enque_axiom(m_e);
                 m_e.reset();
@@ -264,7 +261,6 @@ namespace smt {
             bool     m_sign;
         public:
             replay_unit_literal(ast_manager& m, expr* e, bool sign) : m_e(e, m), m_sign(sign) {}
-            ~replay_unit_literal() override {}
             void operator()(theory_seq& th) override {
                 literal lit = th.mk_literal(m_e);
                 if (m_sign) lit.neg();
@@ -278,7 +274,6 @@ namespace smt {
             expr_ref m_e;
         public:
             replay_is_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
-            ~replay_is_axiom() override {}
             void operator()(theory_seq& th) override {
                 th.check_int_string(m_e);
                 m_e.reset();
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 090a5fe36..27ee97c97 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -51,7 +51,6 @@ public:
     str_value_factory(ast_manager & m, family_id fid) :
         value_factory(m, fid),
         u(m), delim("!"), m_next(0) {}
-    ~str_value_factory() override {}
     expr * get_some_value(sort * s) override {
         return u.str.mk_string("some value");
     }
@@ -93,7 +92,6 @@ class binary_search_trail : public trail {
 public:
     binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) :
         target(target), entry(entry) {}
-    ~binary_search_trail() override {}
     void undo() override {
         TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;);
         if (target.contains(entry)) {
diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h
index 236f56bee..03a205ca6 100644
--- a/src/smt/theory_wmaxsat.h
+++ b/src/smt/theory_wmaxsat.h
@@ -74,10 +74,7 @@ namespace smt {
                 m_old_values(old) {
                 old.push_back(value);
             }
-            
-            ~numeral_trail() override {
-            }
-            
+
             void undo() override {
                 m_value = m_old_values.back();
                 m_old_values.shrink(m_old_values.size() - 1);
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 29a5c0a8f..6e414816f 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -398,7 +398,6 @@ class combined_solver_factory : public solver_factory {
     scoped_ptr<solver_factory> m_f2;
 public:
     combined_solver_factory(solver_factory * f1, solver_factory * f2):m_f1(f1), m_f2(f2) {}
-    ~combined_solver_factory() override {}
 
     solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
         return mk_combined_solver((*m_f1)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic),
diff --git a/src/solver/solver.h b/src/solver/solver.h
index dde4ccbe0..09daf3b29 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -53,7 +53,6 @@ class solver : public check_sat_result, public user_propagator::core {
     symbol      m_cancel_backup_file;
 public:
     solver() {}
-    ~solver() override {}
 
     /**
     \brief Creates a clone of the solver.
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 09ede0c35..b178929bd 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -357,9 +357,7 @@ class tactic2solver_factory : public solver_factory {
 public:
     tactic2solver_factory(tactic * t):m_tactic(t) {
     }
-    
-    ~tactic2solver_factory() override {}
-    
+
     solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
         return mk_tactic2solver(m, m_tactic.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
     }
diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index 33ffbf282..a544c6810 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -51,7 +51,6 @@ public:
     result operator()(goal const & g) override {
         return is_unbounded(g);
     }
-    ~is_unbounded_probe() override {}
 };
 
 probe * mk_is_unbounded_probe() {
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 3cc7436d1..25c5620c2 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -39,9 +39,6 @@ public:
         return alloc(card2bv_tactic, m, m_params);
     }
 
-    ~card2bv_tactic() override {
-    }
-
     char const* name() const override { return "card2bv"; }
 
     void updt_params(params_ref const & p) override {
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index a1a1a56cc..1711a34ac 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -165,10 +165,6 @@ public:
         m_bounds(m) {
     }
 
-    ~eq2bv_tactic() override {
-    }
-        
-        
     void updt_params(params_ref const & p) override {
     }
     
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 560b7b265..36df89da5 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -434,9 +434,6 @@ public:
         return alloc(nla2bv_tactic, m_params);
     }
 
-    ~nla2bv_tactic() override {
-    }
-
     char const* name() const override { return "nla2bv"; }
 
     void updt_params(params_ref const & p) override {
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 843d32828..afcecd7d3 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -902,9 +902,6 @@ public:
     tactic * translate(ast_manager & m) override {
         return alloc(purify_arith_tactic, m, m_params);
     }
-        
-    ~purify_arith_tactic() override {
-    }
 
     char const* name() const override { return "purify_arith"; }
 
diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp
index fe3294e4c..5c26fb2b5 100644
--- a/src/tactic/bv/bit_blaster_model_converter.cpp
+++ b/src/tactic/bv/bit_blaster_model_converter.cpp
@@ -50,10 +50,7 @@ struct bit_blaster_model_converter : public model_converter {
         for (func_decl* f : newbits) 
             m_newbits.push_back(f);
     }
-    
-    ~bit_blaster_model_converter() override {
-    }
-    
+
     void collect_bits(obj_hashtable<func_decl> & bits) {
         unsigned sz = m_bits.size();
         for (unsigned i = 0; i < sz; i++) {
diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp
index 7ea7c0a69..b0e6be1bd 100644
--- a/src/tactic/bv/bv_bound_chk_tactic.cpp
+++ b/src/tactic/bv/bv_bound_chk_tactic.cpp
@@ -109,8 +109,6 @@ struct bv_bound_chk_rewriter : public rewriter_tpl<bv_bound_chk_rewriter_cfg> {
         updt_params(p);
     }
 
-    ~bv_bound_chk_rewriter() override {}
-
     void updt_params(params_ref const & _p) {
         m_cfg.updt_params(_p);
     }
diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp
index 4f9ae6e9d..650095207 100644
--- a/src/tactic/bv/dt2bv_tactic.cpp
+++ b/src/tactic/bv/dt2bv_tactic.cpp
@@ -93,7 +93,6 @@ class dt2bv_tactic : public tactic {
     struct sort_pred : public i_sort_pred {
         dt2bv_tactic& m_t;
         sort_pred(dt2bv_tactic& t): m_t(t) {}
-        ~sort_pred() override {}
         bool operator()(sort* s) override {
             return m_t.m_fd_sorts.contains(s);
         }
diff --git a/src/tactic/converter.h b/src/tactic/converter.h
index 3146058bb..60602557e 100644
--- a/src/tactic/converter.h
+++ b/src/tactic/converter.h
@@ -57,8 +57,6 @@ protected:
 
 public:
     concat_converter(T * c1, T * c2):m_c1(c1), m_c2(c2) {}
-    
-    ~concat_converter() override {}
 
     void cancel() override {
         m_c2->cancel();
diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp
index 234b7262c..b65fd8353 100644
--- a/src/tactic/core/cofactor_term_ite_tactic.cpp
+++ b/src/tactic/core/cofactor_term_ite_tactic.cpp
@@ -50,7 +50,6 @@ public:
         return alloc(cofactor_term_ite_tactic, m, m_params);
     }
 
-    ~cofactor_term_ite_tactic() override {}
     char const* name() const override { return "cofactor"; }
     void updt_params(params_ref const & p) override { m_params.append(p); m_elim_ite.updt_params(m_params); }
     void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); }
diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp
index 04750a7c3..b02adad6e 100644
--- a/src/tactic/core/collect_statistics_tactic.cpp
+++ b/src/tactic/core/collect_statistics_tactic.cpp
@@ -52,8 +52,6 @@ public:
         m_params(p) {
     }
 
-    ~collect_statistics_tactic() override {}
-
     char const* name() const override { return "collect_statistics"; }
 
     tactic * translate(ast_manager & m_) override {
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 47b2fa389..9ef1cf224 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -32,7 +32,6 @@ class ctx_propagate_assertions : public ctx_simplify_tactic::simplifier {
     void assert_eq_core(expr * t, app * val);
 public:
     ctx_propagate_assertions(ast_manager& m);
-    ~ctx_propagate_assertions() override {}
     bool assert_expr(expr * t, bool sign) override;
     bool simplify(expr* t, expr_ref& result) override;
     void push();
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 1dda062c8..9bf70ab16 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -541,7 +541,6 @@ class expr_substitution_simplifier : public dom_simplifier {
 
 public:
     expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {}
-    ~expr_substitution_simplifier() override {}
 
     bool assert_expr(expr * t, bool sign) override {
         expr* tt;
diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp
index fccfdf53e..959a1fc18 100644
--- a/src/tactic/core/nnf_tactic.cpp
+++ b/src/tactic/core/nnf_tactic.cpp
@@ -47,8 +47,6 @@ public:
         return alloc(nnf_tactic, m_params);
     }
 
-    ~nnf_tactic() override {}
-
     char const* name() const override { return "nnf"; }
 
     void updt_params(params_ref const & p) override { m_params.append(p); }
diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index 0313899ac..2c4b80b93 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -102,8 +102,6 @@ public:
     pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): 
         m(m), m_trail(m), pb(m), m_r(m) {}
 
-    ~pb_preprocess_tactic() override {}
-
     tactic * translate(ast_manager & m) override {
         return alloc(pb_preprocess_tactic, m);
     }
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index cfcc42482..df3de8219 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -45,8 +45,6 @@ public:
         m_arith(m)
     {}
 
-    ~reduce_invertible_tactic() override { }
-
     char const* name() const override { return "reduce_invertible"; }
 
     tactic * translate(ast_manager & m) override {
diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h
index dae38304a..85fa8ed24 100644
--- a/src/tactic/core/special_relations_tactic.h
+++ b/src/tactic/core/special_relations_tactic.h
@@ -47,8 +47,6 @@ public:
     special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()): 
         m(m), m_params(ref), m_pm(m) {}
 
-    ~special_relations_tactic() override {}
-
     void updt_params(params_ref const & p) override { m_params.append(p); }
     
     void collect_param_descrs(param_descrs & r) override { }
diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp
index 12b76b638..99a69395b 100644
--- a/src/tactic/core/split_clause_tactic.cpp
+++ b/src/tactic/core/split_clause_tactic.cpp
@@ -52,8 +52,6 @@ class split_clause_tactic : public tactic {
         split_pc(ast_manager & m, app * cls, proof * pr):m_clause(cls, m), m_clause_pr(pr, m) {
         }
 
-        ~split_pc() override { }
-
         proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override {
             // Let m_clause be of the form (l_0 or ... or l_{num_source - 1})
             // Each source[i] proof is a proof for "false" using l_i as a hypothesis
@@ -87,9 +85,6 @@ public:
         t->m_largest_clause = m_largest_clause;
         return t;
     }
-    
-    ~split_clause_tactic() override {
-    }
 
     char const* name() const override { return "split_clause"; }
 
diff --git a/src/tactic/equiv_proof_converter.h b/src/tactic/equiv_proof_converter.h
index 4a479a7ae..87a8f7131 100644
--- a/src/tactic/equiv_proof_converter.h
+++ b/src/tactic/equiv_proof_converter.h
@@ -32,8 +32,6 @@ public:
 
     equiv_proof_converter(ast_manager& m): m(m), m_replace(m) {}
 
-    ~equiv_proof_converter() override {}
-
     proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override {
         return m_replace(m, num_source, source);
     }
diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp
index cb136ad9f..5322b523d 100644
--- a/src/tactic/fd_solver/enum2bv_solver.cpp
+++ b/src/tactic/fd_solver/enum2bv_solver.cpp
@@ -46,8 +46,6 @@ public:
         solver::updt_params(p);
     }
 
-    ~enum2bv_solver() override {}
-
     solver* translate(ast_manager& dst_m, params_ref const& p) override {   
         solver* result = alloc(enum2bv_solver, dst_m, p, m_solver->translate(dst_m, p));
         model_converter_ref mc = external_model_converter();
diff --git a/src/tactic/fd_solver/pb2bv_solver.cpp b/src/tactic/fd_solver/pb2bv_solver.cpp
index cd19b0dca..ee4a03d31 100644
--- a/src/tactic/fd_solver/pb2bv_solver.cpp
+++ b/src/tactic/fd_solver/pb2bv_solver.cpp
@@ -46,8 +46,6 @@ public:
         solver::updt_params(p);
     }
 
-    ~pb2bv_solver() override {}
-
     solver* translate(ast_manager& dst_m, params_ref const& p) override {
         flush_assertions();
         solver* result = alloc(pb2bv_solver, dst_m, p, m_solver->translate(dst_m, p));
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 18b97d116..f653e22e2 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -1867,9 +1867,7 @@ namespace smtfd {
             updt_params(p);
             add_toggle(m.mk_true());
         }
-        
-        ~solver() override {}
-        
+
         ::solver* translate(ast_manager& dst_m, params_ref const& p) override {
             solver* result = alloc(solver, m_indent, dst_m, p);
             if (m_fd_sat_solver) result->m_fd_sat_solver = m_fd_sat_solver->translate(dst_m, p);
diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index a9294471e..9595cc606 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -70,7 +70,6 @@ public:
     result operator()(goal const & g) override {
         return !test<is_non_fp_qfnra_predicate>(g);
     }
-    ~is_fp_qfnra_probe() override {}
 };
 
 probe * mk_is_fp_qfnra_probe() {
@@ -145,8 +144,6 @@ public:
     result operator()(goal const & g) override {
         return !test<is_non_qffp_predicate>(g);
     }
-
-    ~is_qffp_probe() override {}
 };
 
 probe * mk_is_qffp_probe() {
diff --git a/src/tactic/fpa/qffplra_tactic.cpp b/src/tactic/fpa/qffplra_tactic.cpp
index 0fdad5943..711eadc8f 100644
--- a/src/tactic/fpa/qffplra_tactic.cpp
+++ b/src/tactic/fpa/qffplra_tactic.cpp
@@ -82,8 +82,6 @@ public:
             test<is_fpa_function>(g) && 
             !test<is_non_qffplra_predicate>(g);
     }
-
-    ~is_qffplra_probe() override {}
 };
 
 probe * mk_is_qffplra_probe() {
diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp
index 55b7b27b4..5c08da76f 100644
--- a/src/tactic/model_converter.cpp
+++ b/src/tactic/model_converter.cpp
@@ -136,8 +136,6 @@ public:
 
     model2mc(model * m, labels_vec const & r):m_model(m), m_labels(r) {}
 
-    ~model2mc() override {}
-
     void operator()(model_ref & m) override {
         if (!m || !m_model) {
             m = m_model;
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 0c304aa3f..483be4cca 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -130,8 +130,7 @@ class smt_strategic_solver_factory : public solver_factory {
     symbol m_logic;
 public:
     smt_strategic_solver_factory(symbol const & logic):m_logic(logic) {}
-    
-    ~smt_strategic_solver_factory() override {}
+
     solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
         symbol l;
         if (m_logic != symbol::null)
diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp
index c92968c8c..96458c711 100644
--- a/src/tactic/portfolio/solver_subsumption_tactic.cpp
+++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp
@@ -131,8 +131,6 @@ public:
         return alloc(solver_subsumption_tactic, other_m, m_params);
     }
 
-    ~solver_subsumption_tactic() override {}
-
     char const* name() const override { return "solver_subsumption"; }
 
     void updt_params(params_ref const& p) override { 
diff --git a/src/tactic/proof_converter.cpp b/src/tactic/proof_converter.cpp
index b876f1216..d1905b383 100644
--- a/src/tactic/proof_converter.cpp
+++ b/src/tactic/proof_converter.cpp
@@ -86,7 +86,6 @@ class proof2pc : public proof_converter {
     proof_ref m_pr;
 public:
     proof2pc(ast_manager & m, proof * pr):m_pr(pr, m) {}
-    ~proof2pc() override {}
 
     proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override {
         SASSERT(num_source == 0);
diff --git a/src/tactic/proof_converter.h b/src/tactic/proof_converter.h
index fd4df7311..88152ce5b 100644
--- a/src/tactic/proof_converter.h
+++ b/src/tactic/proof_converter.h
@@ -25,7 +25,6 @@ class goal;
 
 class proof_converter : public converter {
 public:
-    ~proof_converter() override { }
     virtual proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) = 0;
     virtual proof_converter * translate(ast_translation & translator) = 0;
 };
diff --git a/src/tactic/replace_proof_converter.h b/src/tactic/replace_proof_converter.h
index cc9a9c6c2..37bbf55b3 100644
--- a/src/tactic/replace_proof_converter.h
+++ b/src/tactic/replace_proof_converter.h
@@ -31,8 +31,6 @@ public:
 
     replace_proof_converter(ast_manager& _m): m(_m), m_proofs(m) {}
 
-    ~replace_proof_converter() override {}
-
     proof_ref operator()(ast_manager & _m, unsigned num_source, proof * const * source) override;
 
     proof_converter * translate(ast_translation & translator) override;
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 57c6ae99a..d93a17ce1 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -51,8 +51,6 @@ public:
         , m_inc_use_sat(false)
     {}
 
-    ~qfufbv_ackr_tactic() override { }
-
     char const* name() const override { return "qfufbv_ackr"; }
 
     void operator()(goal_ref const & g, goal_ref_buffer & result) override {
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index bc87cdf18..d919f51ee 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -35,7 +35,6 @@ class tactic : public user_propagator::core {
     unsigned m_ref_count;
 public:
     tactic():m_ref_count(0) {}
-    ~tactic() override {}
 
     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/tactic_exception.h b/src/tactic/tactic_exception.h
index f230d417b..c6be82daa 100644
--- a/src/tactic/tactic_exception.h
+++ b/src/tactic/tactic_exception.h
@@ -26,7 +26,6 @@ protected:
     std::string m_msg;
 public:
     tactic_exception(std::string && msg) : m_msg(std::move(msg)) {}
-    ~tactic_exception() override {}
     char const * msg() const override { return m_msg.c_str(); }
 };
 
diff --git a/src/util/z3_exception.h b/src/util/z3_exception.h
index cb0a58e37..1d54fb7b5 100644
--- a/src/util/z3_exception.h
+++ b/src/util/z3_exception.h
@@ -42,7 +42,6 @@ public:
     struct fmt {};
     default_exception(std::string && msg) : m_msg(std::move(msg)) {}
     default_exception(fmt, char const* msg, ...);
-    ~default_exception() override {}
     char const * msg() const override;
 };