mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity

build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-26 01:31:41 -07:00
parent d7b1a5e3be
commit ab2c992aa1
4 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/sls_context.cpp
View file

@ -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) {

1
src/ast/sls/sls_datatype_plugin.cpp
View file

@ -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))

2
src/ast/sls/sls_datatype_plugin.h
View file

@ -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;

2
src/ast/sls/sls_smt_solver.cpp
View file

@ -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;