From ab2c992aa103a7e2e64563131971c30fff651f8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Oct 2024 01:31:41 -0700 Subject: [PATCH] build warnings Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_context.cpp | 4 ++-- src/ast/sls/sls_datatype_plugin.cpp | 1 - src/ast/sls/sls_datatype_plugin.h | 2 +- src/ast/sls/sls_smt_solver.cpp | 2 +- 4 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index 626348ee8..051ae98a7 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -39,8 +39,8 @@ namespace sls { m_ld(*this), m_repair_down(m.get_num_asts(), m_gd), m_repair_up(m.get_num_asts(), m_ld), - m_todo(m), - m_constraint_trail(m) { + m_constraint_trail(m), + m_todo(m) { } void context::updt_params(params_ref const& p) { diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp index aea9e55ac..f5aba0083 100644 --- a/src/ast/sls/sls_datatype_plugin.cpp +++ b/src/ast/sls/sls_datatype_plugin.cpp @@ -182,7 +182,6 @@ namespace sls { void datatype_plugin::add_axioms() { expr_ref_vector axioms(m); - expr* u = nullptr; for (auto t : ctx.subterms()) { auto s = t->get_sort(); if (dt.is_datatype(s)) diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h index a28dd65c0..f06e24963 100644 --- a/src/ast/sls/sls_datatype_plugin.h +++ b/src/ast/sls/sls_datatype_plugin.h @@ -82,7 +82,7 @@ namespace sls { public: datatype_plugin(context& c); ~datatype_plugin() override; - family_id fid() { return m_fid; } + family_id fid() override { return m_fid; } expr_ref get_value(expr* e) override; void initialize() override; void start_propagation() override; diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp index e4e9f1200..09efea199 100644 --- a/src/ast/sls/sls_smt_solver.cpp +++ b/src/ast/sls/sls_smt_solver.cpp @@ -78,7 +78,7 @@ namespace sls { m_context.register_atom(v, e); } - std::ostream& display(std::ostream& out) { + std::ostream& display(std::ostream& out) override { m_ddfw.display(out); m_context.display(out); return out;