mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 18:30:24 +00:00
Code Activity

fix build warnings

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-14 10:33:14 -07:00
parent 5ad79f2864
commit 1510b3112e
7 changed files with 0 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -21,7 +21,6 @@ namespace sls {
bv_fixed::bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx) : bv_fixed::bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx) :
ev(ev), ev(ev),
terms(terms),
m(ev.m), m(ev.m),
bv(ev.bv), bv(ev.bv),
ctx(ctx) ctx(ctx)

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

@ -29,7 +29,6 @@ namespace sls {
class bv_fixed { class bv_fixed {
bv_eval& ev; bv_eval& ev;
bv_terms& terms;
ast_manager& m; ast_manager& m;
bv_util& bv; bv_util& bv;
sls::context& ctx; sls::context& ctx;

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

@ -24,7 +24,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 {
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_context.h
View file

@ -125,7 +125,6 @@ namespace sls {
random_gen m_rand; random_gen m_rand;
bool m_initialized = false; bool m_initialized = false;
bool m_new_constraint = false; bool m_new_constraint = false;
bool m_dirty = false;
expr_ref_vector m_input_assertions; expr_ref_vector m_input_assertions;
expr_ref_vector m_allterms; expr_ref_vector m_allterms;
ptr_vector<expr> m_subterms; ptr_vector<expr> m_subterms;

1
src/qe/mbp/mbp_arrays_tg.cpp
View file

@ -414,7 +414,6 @@ struct mbp_array_tg::impl {
expr* a1 = e1->get_arg(0); expr* a1 = e1->get_arg(0);
for (unsigned j = i + 1; j < rdTerms.size(); j++) { for (unsigned j = i + 1; j < rdTerms.size(); j++) {
app* e2 = rdTerms.get(j); app* e2 = rdTerms.get(j);
expr* a2 = e2->get_arg(0);
if (!is_seen(e1, e2) && a1 == e2) { if (!is_seen(e1, e2) && a1 == e2) {
mark_seen(e1, e2); mark_seen(e1, e2);
progress = true; progress = true;

1
src/tactic/arith/fix_dl_var_tactic.cpp
View file

@ -245,7 +245,6 @@ class fix_dl_var_tactic : public tactic {
void operator()(goal_ref const & g, void operator()(goal_ref const & g,
goal_ref_buffer & result) { goal_ref_buffer & result) {
tactic_report report("fix-dl-var", *g); tactic_report report("fix-dl-var", *g);
bool produce_proofs = g->proofs_enabled();
m_produce_models = g->models_enabled(); m_produce_models = g->models_enabled();
TRACE("fix_dl_var", g->display(tout);); TRACE("fix_dl_var", g->display(tout););