From 96671cfc73766568988ec876894c8f6f3bf5bebf Mon Sep 17 00:00:00 2001 From: Henrich Lauko Date: Fri, 29 Oct 2021 15:42:32 +0200 Subject: [PATCH] Add and fix a few general compiler warnings. (#5628) * rewriter: fix unused variable warnings * cmake: make missing non-virtual dtors error * treewide: add missing virtual destructors * cmake: add a few more checks * api: add missing virtual destructor to user_propagator_base * examples: compile cpp example with compiler warnings * model: fix unused variable warnings * rewriter: fix logical-op-parentheses warnings * sat: fix unused variable warnings * smt: fix unused variable warnings --- cmake/compiler_warnings.cmake | 21 +++++++++++++++++++ examples/c++/CMakeLists.txt | 2 ++ src/api/c++/z3++.h | 2 ++ 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/ast/rewriter/seq_rewriter.cpp | 7 +++---- 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 +++ .../upolynomial_factorization_int.h | 2 ++ src/math/realclosure/realclosure.h | 1 + src/math/subpaving/subpaving_types.h | 1 + src/model/model_evaluator.cpp | 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/sat_solver.cpp | 1 - src/sat/smt/array_model.cpp | 2 +- src/sat/smt/pb_constraint.h | 3 +++ src/sat/smt/pb_solver_interface.h | 1 + src/smt/mam.cpp | 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 ++ 39 files changed, 68 insertions(+), 9 deletions(-) diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index 4a5819fe0..339c2e6f5 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -39,6 +39,27 @@ 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" + # 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" ) ################################################################################ diff --git a/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt index 6223ea7c7..0b152f6ac 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 diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4847eeed5..1bdcb7c30 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 diff --git a/src/ast/ast.h b/src/ast/ast.h index 0fafc2a76..739f63dc8 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 23b656c12..ff25f1235 100644 --- a/src/ast/ast_smt_pp.h +++ b/src/ast/ast_smt_pp.h @@ -46,6 +46,7 @@ public: 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 3a1f2ec50..471a7c6fc 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -61,7 +61,7 @@ protected: 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 461fca59d..6bf200b30 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 e744dfb02..268df8821 100644 --- a/src/ast/normal_forms/name_exprs.h +++ b/src/ast/normal_forms/name_exprs.h @@ -23,6 +23,7 @@ Notes: 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 cff4ef9ff..d8c6e6319 100644 --- a/src/ast/num_occurs.h +++ b/src/ast/num_occurs.h @@ -37,6 +37,8 @@ public: 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 dd6f5181a..1146b7aaf 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 ae3af1222..a2e18dd25 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 6be2531b2..c6c5437b7 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/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index f75ccb255..588979534 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,()) = [] @@ -3182,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)); @@ -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()); }; @@ -3404,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; diff --git a/src/math/hilbert/heap_trie.h b/src/math/hilbert/heap_trie.h index 8b9f60f73..7d4179de8 100644 --- a/src/math/hilbert/heap_trie.h +++ b/src/math/hilbert/heap_trie.h @@ -270,6 +270,7 @@ public: 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 cffae412c..cef58ed21 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 std::ostream & print_row(const row_strip & row, std::ostream & out) const { diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h index a021a2a36..b233894ad 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 594e9b6f4..442d10b16 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -99,6 +99,7 @@ template 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 20c9b6b40..416422f64 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -71,6 +71,7 @@ namespace polynomial { template 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 e3e4793a5..e66fd2f1b 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 8154c43d3..788db4bbf 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 b914901a8..874013533 100644 --- a/src/math/subpaving/subpaving_types.h +++ b/src/math/subpaving/subpaving_types.h @@ -42,6 +42,7 @@ public: }; 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/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 617cfe85f..5c6d0f311 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 { diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index 05872c06b..fcf45abf9 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 1e3e5cdfd..c65a2b4ff 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 43f776a68..dd717c392 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 f9c6fd912..a814ac0f8 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 e5c4300a5..4a4997de6 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 6a50c0a71..a5152522f 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 b185ebdc5..147bc90cc 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/sat_solver.cpp b/src/sat/sat_solver.cpp index cdf3a4c68..e5fd2ef70 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); } diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index 33ad8e484..92a368095 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/sat/smt/pb_constraint.h b/src/sat/smt/pb_constraint.h index 076151395..d8cec6de9 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 30914fc3f..87d6c1b75 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/mam.cpp b/src/smt/mam.cpp index bc97daed2..a90403626 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(); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 0b973f4ed..34f323695 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 a9eb2321b..9e2fa9295 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_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 59f83a34f..95848133c 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 a6d6f8169..550105167 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -241,6 +241,7 @@ public: 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 3e23175ff..c5d67506e 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)) {