diff --git a/src/ackermannization/ackr_bound_probe.cpp b/src/ackermannization/ackr_bound_probe.cpp
index b518adccc..48a54543f 100644
--- a/src/ackermannization/ackr_bound_probe.cpp
+++ b/src/ackermannization/ackr_bound_probe.cpp
@@ -60,8 +60,6 @@ class ackr_bound_probe : public probe {
     };
 
 public:
-    ackr_bound_probe() {}
-
     result operator()(goal const & g) override {
         proc p(g.m());
         unsigned sz = g.size();
diff --git a/src/ast/converters/model_converter.h b/src/ast/converters/model_converter.h
index 354b51854..baf5e422d 100644
--- a/src/ast/converters/model_converter.h
+++ b/src/ast/converters/model_converter.h
@@ -71,9 +71,6 @@ protected:
     void display_del(std::ostream& out, func_decl* f) const;
     void display_add(std::ostream& out, ast_manager& m);
 public:
-
-    model_converter() {}
-
     void set_completion(bool f) { m_completion = f; }
 
     virtual void operator()(model_ref & m) = 0;
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index a976ee3c9..5f2534a51 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -417,7 +417,6 @@ namespace recfun {
     }
 
     namespace decl {
-        plugin::plugin() : decl_plugin(), m_defs(), m_case_defs() {}
         plugin::~plugin() { finalize(); }
 
         void plugin::finalize() {
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index e078c7ef9..73e2b5244 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -173,7 +173,6 @@ namespace recfun {
             void compute_scores(expr* e, obj_map<expr, unsigned>& scores);
 
         public:
-            plugin();
             ~plugin() override;
             void finalize() override;
 
diff --git a/src/ast/rewriter/var_subst.h b/src/ast/rewriter/var_subst.h
index e9d39740d..aa905cb0e 100644
--- a/src/ast/rewriter/var_subst.h
+++ b/src/ast/rewriter/var_subst.h
@@ -94,7 +94,7 @@ class expr_free_vars {
     ptr_vector<sort> m_sorts;
     ptr_vector<expr> m_todo;
 public:
-    expr_free_vars() {}
+    expr_free_vars() = default;
     expr_free_vars(expr* e) { (*this)(e); }
     void reset();
     void operator()(expr* e);
diff --git a/src/ast/simplifiers/linear_equation.h b/src/ast/simplifiers/linear_equation.h
index 5220a1e46..662c8c9fc 100644
--- a/src/ast/simplifiers/linear_equation.h
+++ b/src/ast/simplifiers/linear_equation.h
@@ -35,7 +35,7 @@ private:
     mpz *      m_as;        // precise coefficients
     double *   m_approx_as; // approximated coefficients
     var *      m_xs;        // var ids
-    linear_equation() {}
+    linear_equation() = default;
 public:
     unsigned size() const { return m_size; }
     mpz const & a(unsigned idx) const { SASSERT(idx < m_size); return m_as[idx]; }
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index d113eb881..6dc60c9dd 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -47,7 +47,7 @@ class func_decls {
     bool signatures_collide(func_decl* f, func_decl* g) const;
     bool signatures_collide(unsigned n, sort*const* domain, sort* range, func_decl* g) const;
 public:
-    func_decls() {}
+    func_decls() = default;
     func_decls(ast_manager & m, func_decl * f);
     void finalize(ast_manager & m);
     bool contains(func_decl * f) const;
diff --git a/src/math/interval/mod_interval.h b/src/math/interval/mod_interval.h
index ed189fe7b..28b69b003 100644
--- a/src/math/interval/mod_interval.h
+++ b/src/math/interval/mod_interval.h
@@ -26,7 +26,7 @@ namespace bv {
         bool tight = true;
         
         interval_tpl(T const& l, T const& h, unsigned sz, bool tight = false): l(l), h(h), sz(sz), tight(tight) {}
-        interval_tpl() {}
+        interval_tpl() = default;
 
         bool invariant() const {
             return 
@@ -167,7 +167,7 @@ namespace bv {
         iinterval i;
         rinterval r;
         
-        interval() {}
+        interval() = default;
            
         interval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
             if (sz <= 64) {
diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h
index e1096a75f..be3a024e3 100644
--- a/src/math/lp/factorization.h
+++ b/src/math/lp/factorization.h
@@ -24,7 +24,7 @@ class factor {
     factor_type  m_type = factor_type::VAR;
     bool         m_sign = false;
 public:
-    factor() { }
+    factor() = default;
     explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t) {}
     unsigned var() const { return m_var; }
     factor_type type() const { return m_type; }
diff --git a/src/math/lp/indexed_value.h b/src/math/lp/indexed_value.h
index 92d8f2adf..c0194670d 100644
--- a/src/math/lp/indexed_value.h
+++ b/src/math/lp/indexed_value.h
@@ -29,7 +29,7 @@ public:
     // m_other is the offset of the corresponding element in its vector : for a row element it points to the column element offset,
     // for a column element it points to the row element offset
     unsigned m_other;
-    indexed_value() {}
+    indexed_value() = default;
 
     indexed_value(T v, unsigned i, unsigned other) :
         m_value(v), m_index(i), m_other(other) {
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index e4087a407..7217374d5 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -92,7 +92,7 @@ public:
     virtual const rational& coeff() const { return rational::one(); }
 
     #ifdef Z3DEBUG
-    virtual void sort() {};
+    virtual void sort() {}
     #endif
     bool virtual is_linear() const = 0;
 };
diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h
index 93780f7be..dbebbf998 100644
--- a/src/math/lp/numeric_pair.h
+++ b/src/math/lp/numeric_pair.h
@@ -116,10 +116,7 @@ template <typename T>
 struct numeric_pair {
     T x;
     T y;
-    // empty constructor
-    numeric_pair() {}
-    // another constructor
-
+    numeric_pair() = default;
     numeric_pair(T xp, T yp) : x(xp), y(yp) {}
 
     template <typename X>
diff --git a/src/math/lp/permutation_matrix.h b/src/math/lp/permutation_matrix.h
index a3fff4f7f..df0897dbe 100644
--- a/src/math/lp/permutation_matrix.h
+++ b/src/math/lp/permutation_matrix.h
@@ -52,7 +52,7 @@ class permutation_matrix
         };
 
     public:
-        permutation_matrix() {}
+        permutation_matrix() = default;
         permutation_matrix(unsigned length);
 
         permutation_matrix(unsigned length, vector<unsigned> const & values);
diff --git a/src/math/lp/stacked_vector.h b/src/math/lp/stacked_vector.h
index ecd61eb10..69ff99263 100644
--- a/src/math/lp/stacked_vector.h
+++ b/src/math/lp/stacked_vector.h
@@ -98,9 +98,6 @@ private:
         }
     }
 public:
-
-    stacked_vector() { }
-
     ref operator[] (unsigned a) {
         return ref(*this, a);
     }
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
index 42dd476b5..5bbd000ca 100644
--- a/src/math/lp/static_matrix.h
+++ b/src/math/lp/static_matrix.h
@@ -105,7 +105,7 @@ public:
     void init_row_columns(unsigned m, unsigned n);
 
         // constructor with no parameters
-    static_matrix() {}
+    static_matrix() = default;
 
     // constructor
     static_matrix(unsigned m, unsigned n): m_vector_of_row_offsets(n, -1)  {
diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h
index a639a9a5e..56c39c460 100644
--- a/src/math/lp/var_eqs.h
+++ b/src/math/lp/var_eqs.h
@@ -81,7 +81,7 @@ class var_eqs {
         
     mutable stats m_stats;
 public:    
-    var_eqs(): m_merge_handler(nullptr), m_uf(*this), m_stack() {}    
+    var_eqs(): m_merge_handler(nullptr), m_uf(*this) {}    
     /**
        \brief push a scope    */
     void push() {
diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h
index bd7e6efe8..84ac8236d 100644
--- a/src/math/lp/var_register.h
+++ b/src/math/lp/var_register.h
@@ -27,7 +27,7 @@ class ext_var_info {
     bool m_is_integer;
     std::string m_name;
 public:
-    ext_var_info() {}
+    ext_var_info() = default;
     ext_var_info(unsigned j): ext_var_info(j, true) {}
     ext_var_info(unsigned j , bool is_int) : m_external_j(j), m_is_integer(is_int) {}
     ext_var_info(unsigned j , bool is_int, std::string name) : m_external_j(j), m_is_integer(is_int), m_name(name) {}
diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index 74c5e05d7..76f717da0 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -91,7 +91,7 @@ namespace polynomial {
     */
     class power : public std::pair<var, unsigned> {
     public:
-        power():std::pair<var, unsigned>() {}
+        power() = default;
         power(var v, unsigned d):std::pair<var, unsigned>(v, d) {}
         var get_var() const { return first; }
         unsigned degree() const { return second; }
@@ -1895,7 +1895,7 @@ namespace polynomial {
            Invoke add(...), addmul(...) several times, and then invoke mk() to obtain the final polynomial.
         */
         class som_buffer {
-            imp *              m_owner;
+            imp *              m_owner = nullptr;
             monomial2pos       m_m2pos;
             numeral_vector     m_tmp_as;
             monomial_vector    m_tmp_ms;
@@ -1939,8 +1939,6 @@ namespace polynomial {
             }
 
         public:
-            som_buffer():m_owner(nullptr) {}
-
             void reset() {
                 if (empty())
                     return;
@@ -2236,12 +2234,10 @@ namespace polynomial {
            In this buffer, each monomial can be added at most once.
         */
         class cheap_som_buffer {
-            imp *              m_owner;
+            imp *              m_owner = nullptr;
             numeral_vector     m_tmp_as;
             monomial_vector    m_tmp_ms;
         public:
-            cheap_som_buffer():m_owner(nullptr) {}
-
             void set_owner(imp * o) { m_owner = o; }
             bool empty() const { return m_tmp_ms.empty(); }
 
@@ -3072,11 +3068,9 @@ namespace polynomial {
         }
 
         class newton_interpolator_vector {
-            imp *                           m_imp;
+            imp *                           m_imp = nullptr;
             ptr_vector<newton_interpolator> m_data;
         public:
-            newton_interpolator_vector():m_imp(nullptr) {}
-
             ~newton_interpolator_vector() {
                 flush();
             }
diff --git a/src/math/polynomial/upolynomial_factorization_int.h b/src/math/polynomial/upolynomial_factorization_int.h
index a65e5ee62..f47610b65 100644
--- a/src/math/polynomial/upolynomial_factorization_int.h
+++ b/src/math/polynomial/upolynomial_factorization_int.h
@@ -64,7 +64,7 @@ namespace upolynomial {
         
     public:
 
-        factorization_degree_set() { }
+        factorization_degree_set() = default;
 
         factorization_degree_set(zp_factors const & factors)
         {
diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h
index 35516283d..891df598b 100644
--- a/src/math/simplex/model_based_opt.h
+++ b/src/math/simplex/model_based_opt.h
@@ -43,7 +43,7 @@ namespace opt {
         struct var {
             unsigned m_id { 0 };
             rational m_coeff;
-            var() {}
+            var() = default;
             var(unsigned id, rational const& c): m_id(id), m_coeff(c) {}
             struct compare {
                 bool operator()(var x, var y) {
@@ -76,11 +76,11 @@ namespace opt {
 
         // A definition is a linear term of the form (vars + coeff) / div 
         struct def {
-            def(): m_div(1) {}
+            def() = default;
             def(row const& r, unsigned x);
             vector<var> m_vars;
             rational    m_coeff;
-            rational    m_div; 
+            rational    m_div{1};
             def operator+(def const& other) const;
             def operator/(unsigned n) const { return *this / rational(n); }
             def operator/(rational const& n) const;
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index 03a8f1c99..7b01c2b3f 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -393,8 +393,6 @@ namespace datalog {
 
     class skip_model_converter : public model_converter {
     public:
-        skip_model_converter() {}
- 
         model_converter * translate(ast_translation & translator) override { 
             return alloc(skip_model_converter);
         }
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index f40400167..508b79ace 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -56,8 +56,7 @@ struct dl_context {
         m_cmd(ctx),
         m_collected_cmds(collected_cmds),
         m_ref_count(0),
-        m_decl_plugin(nullptr),
-        m_trail() {}
+        m_decl_plugin(nullptr) {}
 
     void inc_ref() {
         ++m_ref_count;
diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp
index 37fd3ef36..f60760fab 100644
--- a/src/muz/rel/dl_mk_simple_joins.cpp
+++ b/src/muz/rel/dl_mk_simple_joins.cpp
@@ -54,8 +54,6 @@ namespace datalog {
             var_idx_set m_all_nonlocal_vars;
             rule_vector m_rules;
 
-            pair_info() {}
-
             pair_info & operator=(const pair_info &) = delete;
             bool can_be_joined() const {
                 return m_consumers > 0;
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 8de25c8f3..5e96dc487 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -1043,7 +1043,6 @@ namespace datalog {
     class relation_manager::null_signature_table_project_fn : public table_transformer_fn {
         const table_signature m_empty_sig;
     public:
-        null_signature_table_project_fn() : m_empty_sig() {}
         table_base * operator()(const table_base & t) override {
             relation_manager & m = t.get_plugin().get_manager();
             table_base * res = m.mk_empty_table(m_empty_sig);
diff --git a/src/muz/rel/dl_sieve_relation.h b/src/muz/rel/dl_sieve_relation.h
index 72c246e99..0166bec98 100644
--- a/src/muz/rel/dl_sieve_relation.h
+++ b/src/muz/rel/dl_sieve_relation.h
@@ -36,7 +36,7 @@ namespace datalog {
             /**
                Create uninitialized rel_spec.
             */
-            rel_spec() {} 
+            rel_spec() = default; 
             /**
                \c inner_kind==null_family_id means we will not specify a relation kind when requesting
                the relation object from the relation_manager.
diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp
index d01056960..7a2ba5179 100644
--- a/src/muz/rel/karr_relation.cpp
+++ b/src/muz/rel/karr_relation.cpp
@@ -674,8 +674,6 @@ namespace datalog {
 
     class karr_relation_plugin::union_fn : public relation_union_fn {
     public:
-        union_fn() {}
-
         void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) override {
 
             karr_relation& r = get(_r);
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 2b28a6c82..8240f7f9e 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -491,8 +491,6 @@ namespace datalog {
     }
     class udoc_plugin::union_fn : public relation_union_fn {
     public:
-        union_fn() {}
-
         void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) override {
             TRACE("doc", _r.display(tout << "dst:\n"); _src.display(tout  << "src:\n"););
             udoc_relation& r = get(_r);
@@ -1040,8 +1038,6 @@ namespace datalog {
 
     class udoc_plugin::join_project_and_fn : public relation_join_fn {
     public:
-      join_project_and_fn() {}
-
       relation_base* operator()(relation_base const& t1, relation_base const& t2) override {
           udoc_relation *result = get(t1.clone());
           result->get_udoc().intersect(result->get_dm(), get(t2).get_udoc());
diff --git a/src/muz/spacer/spacer_arith_kernel.cpp b/src/muz/spacer/spacer_arith_kernel.cpp
index fdcb6b0d6..25aff0273 100644
--- a/src/muz/spacer/spacer_arith_kernel.cpp
+++ b/src/muz/spacer/spacer_arith_kernel.cpp
@@ -45,8 +45,6 @@ bool spacer_arith_kernel::compute_kernel() {
 namespace {
 class simplex_arith_kernel_plugin : public spacer_arith_kernel::plugin {
   public:
-    simplex_arith_kernel_plugin() {}
-
     bool compute_kernel(const spacer_matrix &in, spacer_matrix &out,
                         vector<unsigned> &basics) override {
         using qmatrix = simplex::sparse_matrix<simplex::mpq_ext>;
diff --git a/src/muz/transforms/dl_mk_magic_sets.h b/src/muz/transforms/dl_mk_magic_sets.h
index aa4c30274..3a8a92580 100644
--- a/src/muz/transforms/dl_mk_magic_sets.h
+++ b/src/muz/transforms/dl_mk_magic_sets.h
@@ -65,7 +65,7 @@ namespace datalog {
             func_decl * m_pred;
             adornment m_adornment;
 
-            adornment_desc() {}
+            adornment_desc() = default;
             adornment_desc(func_decl * pred) : m_pred(pred) {}
             adornment_desc(func_decl * pred, const adornment & a) 
                 : m_pred(pred), m_adornment(a) {}
diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp
index d29da86f7..84906cbaa 100644
--- a/src/opt/maxcore.cpp
+++ b/src/opt/maxcore.cpp
@@ -777,7 +777,7 @@ public:
         ptr_vector<expr> es;
         unsigned         k = 0;
         rational         weight;
-        bound_info() {}
+        bound_info() = default;
         bound_info(ptr_vector<expr> const& es, unsigned k, rational const& weight):
             es(es), k(k), weight(weight) {}
         bound_info(expr_ref_vector const& es, unsigned k, rational const& weight):
diff --git a/src/sat/sat_ddfw.h b/src/sat/sat_ddfw.h
index ff86e9b8c..3454d47da 100644
--- a/src/sat/sat_ddfw.h
+++ b/src/sat/sat_ddfw.h
@@ -95,7 +95,6 @@ namespace sat {
         };
 
         struct var_info {
-            var_info() {}
             bool     m_value = false;
             double   m_reward = 0;
             double   m_last_reward = 0;
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index f940af8b4..d4850e67d 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -428,19 +428,11 @@ namespace arith {
          * Facility to put a small box around integer variables used in branch and bounds.
          */
 
-        struct bound_info {
-            rational m_offset;
-            unsigned m_range;
-            bound_info() {}
-            bound_info(rational const& o, unsigned r) :m_offset(o), m_range(r) {}
-        };
         unsigned                  m_bounded_range_idx;  // current size of bounded range.
         literal                   m_bounded_range_lit;  // current bounded range literal
         expr_ref_vector           m_bound_terms; // predicates used for bounds
         expr_ref                  m_bound_predicate;
 
-        obj_map<expr, expr*>      m_predicate2term;
-        obj_map<expr, bound_info> m_term2bound_info;
         bool                      m_model_is_initialized = false;
 
         unsigned small_lemma_size() const { return get_config().m_arith_small_lemma_size; }
diff --git a/src/sat/smt/q_mam.h b/src/sat/smt/q_mam.h
index 9fc6d18f1..e642f9e44 100644
--- a/src/sat/smt/q_mam.h
+++ b/src/sat/smt/q_mam.h
@@ -39,7 +39,7 @@ namespace q {
     class mam {
         friend class mam_impl;
 
-        mam() {}
+        mam() = default;
 
     public:
 
diff --git a/src/smt/params/theory_array_params.h b/src/smt/params/theory_array_params.h
index b6da32ba5..8c56093a8 100644
--- a/src/smt/params/theory_array_params.h
+++ b/src/smt/params/theory_array_params.h
@@ -41,8 +41,6 @@ struct theory_array_params {
     unsigned        m_array_lazy_ieq_delay = 10;
     bool            m_array_fake_support = false;       // fake support for all array operations to pretend they are satisfiable.
 
-    theory_array_params() {}
-
     void updt_params(params_ref const & _p);
 
     void display(std::ostream & out) const;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 6de623bb7..135744f02 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3806,19 +3806,10 @@ public:
      * Facility to put a small box around integer variables used in branch and bounds.
      */
 
-    struct bound_info {
-        rational m_offset;
-        unsigned m_range;
-        bound_info() {}
-        bound_info(rational const& o, unsigned r):m_offset(o), m_range(r) {}
-    };
     unsigned                  m_bounded_range_idx;  // current size of bounded range.
     literal                   m_bounded_range_lit;  // current bounded range literal
     expr_ref_vector           m_bound_terms; // predicates used for bounds
     expr_ref                  m_bound_predicate;
-    
-    obj_map<expr, expr*>      m_predicate2term;
-    obj_map<expr, bound_info> m_term2bound_info;
 
     unsigned init_range() const { return 5; }
     unsigned max_range() const { return 20; }
@@ -3828,8 +3819,6 @@ public:
         m_bounded_range_lit = null_literal;
         m_bound_terms.reset();
         m_bound_predicate = nullptr;
-        m_predicate2term.reset();
-        m_term2bound_info.reset();
     }
 
 
diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index 05ed6eee9..2d82a12a1 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -25,7 +25,7 @@ Author:
 #include "ast/ast_pp.h"
 
 class pb_preprocess_tactic : public tactic {
-    struct rec { unsigned_vector pos, neg; rec() { } };
+    struct rec { unsigned_vector pos, neg; };
     typedef obj_map<app, rec> var_map;
     ast_manager&     m;
     expr_ref_vector  m_trail;
diff --git a/src/util/array.h b/src/util/array.h
index 2954035f6..d844692ef 100644
--- a/src/util/array.h
+++ b/src/util/array.h
@@ -26,7 +26,7 @@ public:
     
 private:
 #define ARRAY_SIZE_IDX     -1
-    T * m_data;
+    T * m_data = nullptr;
     void destroy_elements() {
         iterator it = begin();
         iterator e  = end();
@@ -71,7 +71,7 @@ public:
     typedef T * iterator;
     typedef const T * const_iterator;
 
-    array():m_data(nullptr) {}
+    array() = default;
 
     /**
        \brief Store the array in the given chunk of memory (mem).
@@ -193,7 +193,7 @@ public:
 template<typename T>
 class ptr_array : public array<T *, false> {
 public:
-    ptr_array() {}
+    ptr_array() = default;
     ptr_array(void * mem, unsigned sz, T * const * vs):array<T*, false>(mem, sz, vs) {}
     template<typename Allocator>
     ptr_array(Allocator & a, unsigned sz, T * const * vs):array<T*, false>(a, sz, vs) {}
@@ -205,7 +205,7 @@ public:
 template<typename T>
 class sarray : public array<T, false> {
 public:
-    sarray() {}
+    sarray() = default;
     sarray(void * mem, unsigned sz, T const * vs):array<T, false>(mem, sz, vs) {}
     template<typename Allocator>
     sarray(Allocator & a, unsigned sz, T const * vs):array<T, false>(a, sz, vs) {}
diff --git a/src/util/buffer.h b/src/util/buffer.h
index 3ca597af2..b71717fe6 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -275,6 +275,6 @@ public:
 template<typename T, unsigned INITIAL_SIZE=16>
 class sbuffer : public buffer<T, false, INITIAL_SIZE> {
 public:
-    sbuffer(): buffer<T, false, INITIAL_SIZE>() {}
+    sbuffer() = default;
     sbuffer(unsigned sz, const T& elem) : buffer<T, false, INITIAL_SIZE>(sz,elem) {}
 };
diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h
index 2d7963ff0..7e8487d9d 100644
--- a/src/util/inf_rational.h
+++ b/src/util/inf_rational.h
@@ -65,7 +65,7 @@ class inf_rational {
         return s;
     }
 
-    inf_rational() {}
+    inf_rational() = default;
 
     explicit inf_rational(int n):
         m_first(rational(n)),
diff --git a/src/util/sat_literal.h b/src/util/sat_literal.h
index 58088e628..61ee5f657 100644
--- a/src/util/sat_literal.h
+++ b/src/util/sat_literal.h
@@ -119,7 +119,7 @@ namespace sat {
         literal_set(literal_vector const& v) {
             for (unsigned i = 0; i < v.size(); ++i) insert(v[i]);
         }
-        literal_set() {}
+        literal_set() = default;
         literal_vector to_vector() const {
             literal_vector result;
             for (literal lit : *this) result.push_back(lit);
@@ -146,7 +146,6 @@ namespace sat {
             literal operator*() const { return to_literal(*m_it); }
             iterator& operator++() { ++m_it; return *this; }
             iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; }
-            bool operator==(iterator const& it) const { return m_it == it.m_it; }
             bool operator!=(iterator const& it) const { return m_it != it.m_it; }
         };
         iterator begin() const { return iterator(m_set.begin()); }
diff --git a/src/util/stacked_value.h b/src/util/stacked_value.h
index 89be6fa53..a3a0d933b 100644
--- a/src/util/stacked_value.h
+++ b/src/util/stacked_value.h
@@ -52,7 +52,7 @@ public:
         }
     }
 
-    stacked_value() {}
+    stacked_value() = default;
     stacked_value(const T& m) {
         m_value = m;
     }