From 399a929d17a1cb0c26fa306dd9f7ba4db051add1 Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 13:25:39 +0200
Subject: [PATCH 01/10] rewriter: fix unused variable warnings

---
 src/ast/rewriter/seq_rewriter.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index f75ccb25522..9eebc26b97a 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3046,7 +3046,6 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
     auto nothing = [&]() { return expr_ref(re().mk_empty(r->get_sort()), m()); };
     auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };
     auto dotstar = [&]() { return expr_ref(re().mk_full_seq(r->get_sort()), m()); };
-    auto dotplus = [&]() { return expr_ref(re().mk_plus(re().mk_full_char(r->get_sort())), m()); };
     unsigned lo = 0, hi = 0;
     if (re().is_empty(r) || re().is_epsilon(r))
         // D(e,[]) = D(e,()) = []
@@ -3260,7 +3259,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) {
 }
 
 expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* d) {
-    sort* seq_sort = nullptr, * ele_sort = nullptr;
+    sort* seq_sort = nullptr;
     VERIFY(m_util.is_re(d, seq_sort));
     auto nothing = [&]() { return expr_ref(re().mk_empty(d->get_sort()), m()); };
     auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };

From 6582947e73d03b32404b86de4abcfaeaad83ae73 Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 13:55:06 +0200
Subject: [PATCH 02/10] cmake: make missing non-virtual dtors error

---
 cmake/compiler_warnings.cmake | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake
index 4a5819fe099..403acdc3bc3 100644
--- a/cmake/compiler_warnings.cmake
+++ b/cmake/compiler_warnings.cmake
@@ -39,6 +39,10 @@ set(CLANG_WARNINGS_AS_ERRORS
   "-Werror=delete-non-virtual-dtor"
   # https://clang.llvm.org/docs/DiagnosticsReference.html#woverloaded-virtual
   "-Werror=overloaded-virtual"
+  # warn the user if a class with virtual functions has a
+  # non-virtual destructor. This helps catch hard to
+  # track down memory errors
+  "-Werror=non-virtual-dtor"
 )
 
 ################################################################################

From 9190347ab32a09f7d8227656a0cfd8fc0b4d377a Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 14:24:47 +0200
Subject: [PATCH 03/10] treewide: add missing virtual destructors

---
 src/ast/ast.h                                       | 1 +
 src/ast/ast_smt_pp.h                                | 1 +
 src/ast/fpa/fpa2bv_converter.h                      | 2 +-
 src/ast/is_variable_test.h                          | 1 +
 src/ast/normal_forms/name_exprs.h                   | 1 +
 src/ast/num_occurs.h                                | 2 ++
 src/ast/recfun_decl_plugin.h                        | 1 +
 src/ast/rewriter/push_app_ite.h                     | 1 +
 src/ast/rewriter/seq_eq_solver.h                    | 1 +
 src/math/hilbert/heap_trie.h                        | 1 +
 src/math/lp/column_namer.h                          | 1 +
 src/math/lp/factorization.h                         | 2 ++
 src/math/lp/lp_settings.h                           | 1 +
 src/math/polynomial/polynomial.h                    | 3 +++
 src/math/polynomial/upolynomial_factorization_int.h | 2 ++
 src/math/realclosure/realclosure.h                  | 1 +
 src/math/subpaving/subpaving_types.h                | 1 +
 src/muz/base/dl_engine_base.h                       | 1 +
 src/nlsat/nlsat_solver.h                            | 1 +
 src/opt/opt_context.h                               | 1 +
 src/opt/opt_pareto.h                                | 1 +
 src/qe/nlarith_util.cpp                             | 1 +
 src/qe/qe.h                                         | 1 +
 src/sat/sat_extension.h                             | 1 +
 src/sat/smt/pb_constraint.h                         | 3 +++
 src/sat/smt/pb_solver_interface.h                   | 1 +
 src/smt/smt_model_finder.cpp                        | 1 +
 src/smt/theory_opt.h                                | 1 +
 src/solver/assertions/asserted_formulas.h           | 1 +
 src/solver/solver.h                                 | 1 +
 src/tactic/fd_solver/smtfd_solver.cpp               | 2 ++
 31 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 0fafc2a76e5..739f63dc833 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1399,6 +1399,7 @@ inline bool has_labels(expr const * n) {
 class some_value_proc {
 public:
     virtual expr * operator()(sort * s) = 0;
+    virtual ~some_value_proc() = default;
 };
 
 // -----------------------------------
diff --git a/src/ast/ast_smt_pp.h b/src/ast/ast_smt_pp.h
index 23b656c12c4..ff25f123539 100644
--- a/src/ast/ast_smt_pp.h
+++ b/src/ast/ast_smt_pp.h
@@ -46,6 +46,7 @@ class ast_smt_pp {
     public:
         virtual bool operator()(func_decl* d) const { return false; }
         virtual bool operator()(sort* s) const { return false; }
+        virtual ~is_declared() = default;
     };
 private:
     ast_manager& m_manager;
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 3a1f2ec50f9..471a7c6fccd 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -61,7 +61,7 @@ class fpa2bv_converter {
 public:
 
     fpa2bv_converter(ast_manager & m);
-    ~fpa2bv_converter();
+    virtual ~fpa2bv_converter();
 
     fpa_util & fu() { return m_util; }
     bv_util & bu() { return m_bv_util; }
diff --git a/src/ast/is_variable_test.h b/src/ast/is_variable_test.h
index 461fca59d9d..6bf200b302d 100644
--- a/src/ast/is_variable_test.h
+++ b/src/ast/is_variable_test.h
@@ -23,6 +23,7 @@ Revision History:
 
 class is_variable_proc {
 public:
+    virtual ~is_variable_proc() = default;
     virtual bool operator()(const expr* e) const = 0;
 };
 
diff --git a/src/ast/normal_forms/name_exprs.h b/src/ast/normal_forms/name_exprs.h
index e744dfb0224..268df88211f 100644
--- a/src/ast/normal_forms/name_exprs.h
+++ b/src/ast/normal_forms/name_exprs.h
@@ -23,6 +23,7 @@ Module Name:
 
 class expr_predicate {
 public:
+    virtual ~expr_predicate() = default;
     virtual bool operator()(expr * t) = 0;
 };
 
diff --git a/src/ast/num_occurs.h b/src/ast/num_occurs.h
index cff4ef9ff38..d8c6e63198d 100644
--- a/src/ast/num_occurs.h
+++ b/src/ast/num_occurs.h
@@ -37,6 +37,8 @@ class num_occurs {
         m_ignore_quantifiers(ignore_quantifiers) {
     }
 
+    virtual ~num_occurs() = default;
+
     void validate();
     virtual void reset() { m_num_occurs.reset(); }
     
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index dd6f5181af6..1146b7aaffd 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -93,6 +93,7 @@ namespace recfun {
     // closure for computing whether a `rhs` expression is immediate
     struct is_immediate_pred {
         virtual bool operator()(expr * rhs) = 0;
+        virtual ~is_immediate_pred() = default;
     };
 
     class def {
diff --git a/src/ast/rewriter/push_app_ite.h b/src/ast/rewriter/push_app_ite.h
index ae3af12222e..a2e18dd257e 100644
--- a/src/ast/rewriter/push_app_ite.h
+++ b/src/ast/rewriter/push_app_ite.h
@@ -33,6 +33,7 @@ struct push_app_ite_cfg : public default_rewriter_cfg {
     virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args);
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
     push_app_ite_cfg(ast_manager& m): m(m), m_conservative(true) {}
+    virtual ~push_app_ite_cfg() = default;
     void set_conservative(bool c) { m_conservative = c; }
     bool rewrite_patterns() const { return false; }
 };
diff --git a/src/ast/rewriter/seq_eq_solver.h b/src/ast/rewriter/seq_eq_solver.h
index 6be2531b23e..c6c5437b79b 100644
--- a/src/ast/rewriter/seq_eq_solver.h
+++ b/src/ast/rewriter/seq_eq_solver.h
@@ -39,6 +39,7 @@ namespace seq {
 
     class eq_solver_context {
     public:
+        virtual ~eq_solver_context() = default;
         virtual void  add_consequence(bool uses_dep, expr_ref_vector const& clause) = 0;
         virtual void  add_solution(expr* var, expr* term) = 0;
         virtual expr* expr2rep(expr* e) = 0;
diff --git a/src/math/hilbert/heap_trie.h b/src/math/hilbert/heap_trie.h
index 8b9f60f7304..7d4179de8fe 100644
--- a/src/math/hilbert/heap_trie.h
+++ b/src/math/hilbert/heap_trie.h
@@ -270,6 +270,7 @@ class heap_trie {
     class check_value {
     public:
         virtual bool operator()(Value const& v) = 0;
+        virtual ~check_value() = default;
     };
 
     bool find_le(Key const* keys, check_value& check) {
diff --git a/src/math/lp/column_namer.h b/src/math/lp/column_namer.h
index cffae412c96..cef58ed21a0 100644
--- a/src/math/lp/column_namer.h
+++ b/src/math/lp/column_namer.h
@@ -23,6 +23,7 @@ Revision History:
 namespace lp {
 class column_namer {
 public:
+    virtual ~column_namer() = default;
     virtual std::string get_variable_name(unsigned j) const = 0;
     template <typename T>
     std::ostream & print_row(const row_strip<T> & row, std::ostream & out) const {
diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h
index a021a2a368b..b233894ad9c 100644
--- a/src/math/lp/factorization.h
+++ b/src/math/lp/factorization.h
@@ -120,6 +120,8 @@ struct factorization_factory {
         m_vars(vars), m_monic(m) {
     }
 
+    virtual ~factorization_factory() = default;
+
     bool_vector get_mask() const {
         // we keep the last element always in the first factor to avoid
         // repeating a pair twice, that is why m_mask is shorter by one then m_vars
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 594e9b6f450..442d10b1675 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -99,6 +99,7 @@ template <typename X> bool is_epsilon_small(const X & v, const double& eps);
 
 class lp_resource_limit {
 public:
+    virtual ~lp_resource_limit() = default;
     virtual bool get_cancel_flag() = 0;
 };
 
diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h
index 20c9b6b4044..416422f6435 100644
--- a/src/math/polynomial/polynomial.h
+++ b/src/math/polynomial/polynomial.h
@@ -71,6 +71,7 @@ namespace polynomial {
     template<typename ValManager, typename Value = typename ValManager::numeral>
     class var2value {
     public:
+        virtual ~var2value() = default;
         virtual ValManager & m() const = 0;
         virtual bool contains(var x) const = 0;
         virtual Value const & operator()(var x) const = 0;
@@ -100,6 +101,7 @@ namespace polynomial {
 
     struct display_var_proc {
         virtual std::ostream& operator()(std::ostream & out, var x) const { return out << "x" << x; }
+        virtual ~display_var_proc() = default;
     };
 
     class polynomial;
@@ -228,6 +230,7 @@ namespace polynomial {
             del_eh * m_next;
         public:
             del_eh():m_next(nullptr) {}
+            virtual ~del_eh() = default;
             virtual void operator()(polynomial * p) = 0;
         };
 
diff --git a/src/math/polynomial/upolynomial_factorization_int.h b/src/math/polynomial/upolynomial_factorization_int.h
index e3e4793a594..e66fd2f1ba1 100644
--- a/src/math/polynomial/upolynomial_factorization_int.h
+++ b/src/math/polynomial/upolynomial_factorization_int.h
@@ -175,6 +175,8 @@ namespace upolynomial {
             m_current_size = 0;
         }
 
+        virtual ~factorization_combination_iterator_base() = default;
+
         /**
            \brief Returns the factors we are enumerating through.
         */
diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h
index 8154c43d351..788db4bbff6 100644
--- a/src/math/realclosure/realclosure.h
+++ b/src/math/realclosure/realclosure.h
@@ -37,6 +37,7 @@ namespace realclosure {
 
     class mk_interval {
     public:
+        virtual ~mk_interval() = default;
         virtual void operator()(unsigned k, mpqi_manager & im, mpqi_manager::interval & r) = 0;
     };
 
diff --git a/src/math/subpaving/subpaving_types.h b/src/math/subpaving/subpaving_types.h
index b914901a8f1..8740135332d 100644
--- a/src/math/subpaving/subpaving_types.h
+++ b/src/math/subpaving/subpaving_types.h
@@ -42,6 +42,7 @@ class power : public std::pair<var, unsigned> {
 };
 
 struct display_var_proc {
+    virtual ~display_var_proc() = default;
     virtual void operator()(std::ostream & out, var x) const { out << "x" << x; }
 };
 
diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h
index 05872c06b7d..fcf45abf93a 100644
--- a/src/muz/base/dl_engine_base.h
+++ b/src/muz/base/dl_engine_base.h
@@ -122,6 +122,7 @@ namespace datalog {
 
     class register_engine_base {
     public:
+        virtual ~register_engine_base() = default;
         virtual engine_base* mk_engine(DL_ENGINE engine_type) = 0;
         virtual void set_context(context* ctx) = 0;
     };
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index 1e3e5cdfde1..c65a2b4ff79 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -32,6 +32,7 @@ namespace nlsat {
 
     class display_assumption_proc {
     public:
+        virtual ~display_assumption_proc() = default;
         virtual std::ostream& operator()(std::ostream& out, assumption a) const = 0;
     };
 
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 43f776a68f5..dd717c3922d 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -45,6 +45,7 @@ namespace opt {
 
     class maxsat_context {
     public:        
+        virtual ~maxsat_context() = default;
         virtual generic_model_converter& fm() = 0;   // converter that removes fresh names introduced by simplification.
         virtual bool sat_enabled() const = 0;       // is using th SAT solver core enabled?
         virtual solver& get_solver() = 0;           // retrieve solver object (SAT or SMT solver)
diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h
index f9c6fd912f4..a814ac0f8d9 100644
--- a/src/opt/opt_pareto.h
+++ b/src/opt/opt_pareto.h
@@ -26,6 +26,7 @@ namespace opt {
    
     class pareto_callback {
     public:
+        virtual ~pareto_callback() = default;
         virtual unsigned num_objectives() = 0;
         virtual expr_ref mk_gt(unsigned i, model_ref& model) = 0;
         virtual expr_ref mk_ge(unsigned i, model_ref& model) = 0;
diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp
index e5c4300a559..4a4997de6ef 100644
--- a/src/qe/nlarith_util.cpp
+++ b/src/qe/nlarith_util.cpp
@@ -989,6 +989,7 @@ namespace nlarith {
             imp& m_imp;
         public:
             isubst(imp& i) : m_imp(i) {}
+            virtual ~isubst() = default;
             virtual void mk_lt(poly const& p, app_ref& r) = 0;
             virtual void mk_eq(poly const& p, app_ref& r) = 0;
             virtual void mk_le(poly const& p, app_ref& r) { 
diff --git a/src/qe/qe.h b/src/qe/qe.h
index 6a50c0a7133..a5152522f37 100644
--- a/src/qe/qe.h
+++ b/src/qe/qe.h
@@ -34,6 +34,7 @@ namespace qe {
 
     class i_nnf_atom {
     public:
+        virtual ~i_nnf_atom() = default;
         virtual void operator()(expr* e, bool pol, expr_ref& result) = 0;
     };
 
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index b185ebdc5f9..147bc90cc21 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -40,6 +40,7 @@ namespace sat {
     class literal_occs_fun {
     public:
         virtual double operator()(literal l) = 0;        
+        virtual ~literal_occs_fun() = default;
     };
 
 
diff --git a/src/sat/smt/pb_constraint.h b/src/sat/smt/pb_constraint.h
index 076151395d7..d8cec6de9d7 100644
--- a/src/sat/smt/pb_constraint.h
+++ b/src/sat/smt/pb_constraint.h
@@ -52,6 +52,9 @@ namespace pb {
         constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k): 
             m_tag(t), m_lit(l), m_size(sz), m_obj_size(osz), m_id(id), m_k(k) {
         }
+
+        virtual ~constraint() = default;
+
         sat::ext_constraint_idx cindex() const { return sat::constraint_base::mem2base(this); }
         void deallocate(small_object_allocator& a) { a.deallocate(obj_size(), sat::constraint_base::mem2base_ptr(this)); }
         unsigned id() const { return m_id; }
diff --git a/src/sat/smt/pb_solver_interface.h b/src/sat/smt/pb_solver_interface.h
index 30914fc3f90..87d6c1b7598 100644
--- a/src/sat/smt/pb_solver_interface.h
+++ b/src/sat/smt/pb_solver_interface.h
@@ -35,6 +35,7 @@ namespace pb {
 
     class solver_interface {
     public:
+        virtual ~solver_interface() = default;
         virtual lbool value(bool_var v) const = 0;
         virtual lbool value(literal lit) const = 0;
         virtual bool is_false(literal lit) const = 0;
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 0b973f4eda0..34f32369545 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -50,6 +50,7 @@ namespace smt {
 
         class evaluator {
         public:
+            virtual ~evaluator() = default;
             virtual expr* eval(expr* n, bool model_completion) = 0;
         };
 
diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h
index a9eb2321b10..9e2fa92958e 100644
--- a/src/smt/theory_opt.h
+++ b/src/smt/theory_opt.h
@@ -29,6 +29,7 @@ namespace smt {
     class theory_opt {
     public:
         typedef inf_eps_rational<inf_rational> inf_eps;
+        virtual ~theory_opt() = default;
         virtual inf_eps value(theory_var) = 0;
         virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) = 0; 
         virtual theory_var add_objective(app* term) = 0;
diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h
index 59f83a34fea..95848133ca6 100644
--- a/src/solver/assertions/asserted_formulas.h
+++ b/src/solver/assertions/asserted_formulas.h
@@ -71,6 +71,7 @@ class asserted_formulas {
         char const*            m_id;
     public:
         simplify_fmls(asserted_formulas& af, char const* id): af(af), m(af.m), m_id(id) {}
+        virtual ~simplify_fmls() = default;
         char const* id() const { return m_id; }
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) = 0;
         virtual bool should_apply() const { return true;}
diff --git a/src/solver/solver.h b/src/solver/solver.h
index a6d6f8169c4..550105167d9 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -241,6 +241,7 @@ class solver : public check_sat_result {
 
     class propagate_callback {
     public:
+         virtual ~propagate_callback() = default;
         virtual void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) = 0;
     };
     class context_obj {
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 3e23175ffd0..c5d67506eba 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -509,6 +509,8 @@ namespace smtfd {
             m_context.add_plugin(this);
         }
 
+        virtual ~theory_plugin() = default;
+
         table& ast2table(ast* f, sort* s) {
             unsigned idx = 0;
             if (!m_ast2table.find(f, s, idx)) {

From b3982ccf12a156ac7128795ded71b43f70d4f7ed Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 14:52:18 +0200
Subject: [PATCH 04/10] cmake: add a few more checks

---
 cmake/compiler_warnings.cmake | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake
index 403acdc3bc3..339c2e6f58c 100644
--- a/cmake/compiler_warnings.cmake
+++ b/cmake/compiler_warnings.cmake
@@ -43,6 +43,23 @@ set(CLANG_WARNINGS_AS_ERRORS
   # non-virtual destructor. This helps catch hard to
   # track down memory errors
   "-Werror=non-virtual-dtor"
+  # warn if a null dereference is detected
+  "-Werror=null-dereference"
+  # warn for potential performance problem casts
+  # "-Werror=cast-align"
+  # warn if float is implicit promoted to double
+  # "-Werror=double-promotion"
+  "-Werror=no-unreachable-code-return"
+  # warn the user if a variable declaration shadows one from a parent context
+  # "-Werror=shadow"
+  # warn for c-style casts
+  # "-Werror=old-style-cast"
+  # warn on sign conversions
+  # "-Werror=sign-conversion"
+  # warn on type conversions that may lose data
+  # "-Werror=conversion"
+  # warn on anything being unused
+  # "-Werror=unused"
 )
 
 ################################################################################

From 9fc1004ab30156be70eb4187c101ba38856f099a Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 15:16:29 +0200
Subject: [PATCH 05/10] api: add missing virtual destructor to
 user_propagator_base

---
 src/api/c++/z3++.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 4847eeed52e..1bdcb7c30e8 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -3940,6 +3940,8 @@ namespace z3 {
         virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;
 
+        virtual ~user_propagator_base() = default;
+
         /**
            \brief user_propagators created using \c fresh() are created during 
            search and their lifetimes are restricted to search time. They should

From 1a46a78c519df8a841b3def39c742d81c661cb40 Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 15:22:45 +0200
Subject: [PATCH 06/10] examples: compile cpp example with compiler warnings

---
 examples/c++/CMakeLists.txt | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt
index 6223ea7c73e..0b152f6acc7 100644
--- a/examples/c++/CMakeLists.txt
+++ b/examples/c++/CMakeLists.txt
@@ -28,6 +28,8 @@ add_executable(cpp_example example.cpp)
 target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
 target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES})
 
+target_compile_options(cpp_example PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+
 if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
   # On Windows we need to copy the Z3 libraries
   # into the same directory as the executable

From cc6a91f595e88d18317c07b27095516fd7e93b7b Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 15:29:58 +0200
Subject: [PATCH 07/10] model: fix unused variable warnings

---
 src/model/model_evaluator.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 617cfe85f13..5c6d0f31197 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -162,7 +162,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
         result_pr = nullptr;
         family_id fid = f->get_family_id();
         bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
-        func_decl* g = nullptr;
         br_status st = BR_FAILED;
 #if 0
         struct pp {

From 8f8476990cf8b54957753c075d9679d4d55e751d Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 15:33:53 +0200
Subject: [PATCH 08/10] rewriter: fix logical-op-parentheses warnings

---
 src/ast/rewriter/seq_rewriter.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 9eebc26b97a..588979534b1 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3181,7 +3181,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
     else if (re().is_loop(r, r1, lo))
         result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, lo - 1));
     else if (re().is_loop(r, r1, lo, hi)) {
-        if (lo == 0 && hi == 0 || hi < lo)
+        if ((lo == 0 && hi == 0) || hi < lo)
             result = nothing();
         else
             result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, (lo == 0 ? 0 : lo - 1), hi - 1));
@@ -3403,7 +3403,7 @@ expr_ref  seq_rewriter::simplify_path(expr* path) {
             result = simplify_path(t);
         else if (m().is_true(t))
             result = simplify_path(h);
-        else if (m().is_eq(h, lhs, rhs) || m().is_not(h, h1) && m().is_eq(h1, lhs, rhs))
+        else if (m().is_eq(h, lhs, rhs) || (m().is_not(h, h1) && m().is_eq(h1, lhs, rhs)))
             elim_condition(lhs, result);
     }
     return result;

From b4a1e1be3cd2e1fb5246904ebcc7065104408968 Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 15:40:49 +0200
Subject: [PATCH 09/10] sat: fix unused variable warnings

---
 src/sat/sat_solver.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index cdf3a4c6813..e5fd2ef70a9 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1893,7 +1893,6 @@ namespace sat {
     void solver::init_ext_assumptions() {
         if (m_ext && m_ext->tracking_assumptions()) {
             m_ext_assumption_set.reset();
-            unsigned trail_size = m_trail.size();
             if (!inconsistent())
                 m_ext->add_assumptions(m_ext_assumption_set);
         }

From 85e331ebe42b5e5651568bb036c1c01af0e2a629 Mon Sep 17 00:00:00 2001
From: Henrich Lauko <henrich.lauko@trailofbits.com>
Date: Thu, 28 Oct 2021 15:43:58 +0200
Subject: [PATCH 10/10] smt: fix unused variable warnings

---
 src/sat/smt/array_model.cpp | 2 +-
 src/smt/mam.cpp             | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index 33ad8e48405..92a3680954b 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -119,7 +119,7 @@ namespace array {
 
     bool solver::must_have_different_model_values(theory_var v1, theory_var v2) {
         euf::enode* else1 = nullptr, * else2 = nullptr;
-        euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2);
+        euf::enode* n1 = var2enode(v1);
         expr* e1 = n1->get_expr();
         if (!a.is_array(e1))
             return true;
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index bc97daed2c5..a90403626e2 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2091,7 +2091,6 @@ namespace {
         enode * n = m_registers[j2->m_reg]->get_root();
         if (n->get_num_parents() == 0)
             return nullptr;
-        unsigned num_args = n->get_num_args();
         enode_vector * v  = mk_enode_vector();
         enode_vector::const_iterator it1  = n->begin_parents();
         enode_vector::const_iterator end1 = n->end_parents();