mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-12 02:04:43 +00:00
Code Activity

fix build warning

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-11-02 11:26:25 -07:00
parent 40b927ff2b
commit d702e68fb9
8 changed files with 4 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2240,12 +2240,12 @@ namespace sls {
return value(v) == abs(value(od.m_arg1)); return value(v) == abs(value(od.m_arg1));
} }
case arith_op_kind::OP_TO_INT: { case arith_op_kind::OP_TO_INT: {
auto od = m_ops[vi.m_def_idx]; // auto od = m_ops[vi.m_def_idx];
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
break; break;
} }
case arith_op_kind::OP_TO_REAL: { case arith_op_kind::OP_TO_REAL: {
auto od = m_ops[vi.m_def_idx]; // auto od = m_ops[vi.m_def_idx];
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
break; break;
} }

1
src/ast/sls/sls_basic_plugin.h
View file

@ -17,7 +17,6 @@ Author:
namespace sls { namespace sls {
class basic_plugin : public plugin { class basic_plugin : public plugin {
bool m_initialized = false;
expr_mark m_axiomatized; expr_mark m_axiomatized;
bool is_basic(expr* e) const; bool is_basic(expr* e) const;

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

@ -23,7 +23,6 @@ Author:
namespace sls { namespace sls {
bv_terms::bv_terms(sls::context& ctx): bv_terms::bv_terms(sls::context& ctx):
ctx(ctx),
m(ctx.get_manager()), m(ctx.get_manager()),
bv(m), bv(m),
m_axioms(m) {} m_axioms(m) {}

1
src/ast/sls/sls_bv_terms.h
View file

@ -29,7 +29,6 @@ Author:
namespace sls { namespace sls {
class bv_terms { class bv_terms {
sls::context& ctx;
ast_manager& m; ast_manager& m;
bv_util bv; bv_util bv;
expr_ref_vector m_axioms; expr_ref_vector m_axioms;

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

@ -430,7 +430,6 @@ namespace sls {
} }
euf::enode* datatype_plugin::get_constructor(euf::enode* n) const { euf::enode* datatype_plugin::get_constructor(euf::enode* n) const {
euf::enode* con = nullptr;
for (auto sib : euf::enode_class(n)) for (auto sib : euf::enode_class(n))
if (dt.is_constructor(sib->get_expr())) if (dt.is_constructor(sib->get_expr()))
return sib; return sib;

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

@ -101,7 +101,6 @@ namespace sls {
g.explain<size_t>(explain, nullptr); g.explain<size_t>(explain, nullptr);
g.end_explain(); g.end_explain();
double reward = -1; double reward = -1;
bool has_flipped = false;
TRACE("enf", TRACE("enf",
for (auto p : explain) { for (auto p : explain) {
sat::literal l = to_literal(p); sat::literal l = to_literal(p);

1
src/ast/sls/sls_euf_plugin.h
View file

@ -70,7 +70,6 @@ namespace sls {
public: public:
euf_plugin(context& c); euf_plugin(context& c);
~euf_plugin() override; ~euf_plugin() override;
family_id fid() { return m_fid; }
expr_ref get_value(expr* e) override; expr_ref get_value(expr* e) override;
void initialize() override; void initialize() override;
void start_propagation() override; void start_propagation() override;

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

@ -64,7 +64,7 @@ namespace sls {
continue; continue;
m_context.register_atom(v, m_smt2sls_tr(e)); m_context.register_atom(v, m_smt2sls_tr(e));
for (auto t : subterms::all(expr_ref(e, m))) for (auto t : subterms::all(expr_ref(e, m)))
add_shared_term(e); add_shared_term(t);
} }
for (auto fml : fmls) for (auto fml : fmls)
@ -82,7 +82,7 @@ namespace sls {
continue; continue;
add_shared_var(v, w); add_shared_var(v, w);
for (auto t : subterms::all(expr_ref(e, m))) for (auto t : subterms::all(expr_ref(e, m)))
add_shared_term(e); add_shared_term(t);
} }
m_thread = std::thread([this]() { run(); }); m_thread = std::thread([this]() { run(); });