From 25f53c046755eac118bf3ed715a1a82e8582bd96 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Feb 2021 13:49:47 -0800 Subject: [PATCH] deal with warnings reported in https://launchpadlibrarian.net/522361319/buildlog_ubuntu-groovy-s390x.z3_4.8.10-1ubuntu4ppa1_BUILDING.txt.gz Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/expr_safe_replace.cpp | 1 - src/nlsat/nlsat_interval_set.cpp | 2 +- src/qe/qe.cpp | 3 --- src/sat/sat_solver.cpp | 1 - src/sat/smt/q_ematch.cpp | 1 - src/sat/smt/q_mbi.cpp | 2 +- src/smt/dyn_ack.cpp | 1 - src/smt/theory_arith_eq.h | 1 + src/smt/theory_seq.cpp | 2 +- src/smt/theory_str.cpp | 6 ------ src/tactic/bv/bv_bounds_tactic.cpp | 4 ++-- 11 files changed, 6 insertions(+), 18 deletions(-) diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index a7f3ecd99..26d5ec9c4 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -64,7 +64,6 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { } else if (is_app(a)) { app* c = to_app(a); - unsigned n = c->get_num_args(); m_args.reset(); bool arg_differs = false, has_all_args = true; for (expr* arg : *c) { diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index 226b5b381..aa5053966 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -76,9 +76,9 @@ namespace nlsat { if (!i.m_lower_inf && !i.m_upper_inf) { auto s = am.compare(i.m_lower, i.m_upper); + (void)s; TRACE("nlsat_interval", tout << "lower: "; am.display_decimal(tout, i.m_lower); tout << ", upper: "; am.display_decimal(tout, i.m_upper); tout << "\ns: " << s << "\n";); - (void)s; SASSERT(s <= 0); SASSERT(!is_zero(s) || !i.m_lower_open && !i.m_upper_open); } diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index d9f036ffd..b4e7ded1b 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -550,7 +550,6 @@ namespace qe { void nnf_and_or(bool is_and, app* a, bool p) { m_args.reset(); - unsigned num_args = a->get_num_args(); expr_ref tmp(m); bool visited = true; for (expr* arg : *a) { @@ -1272,7 +1271,6 @@ namespace qe { } bool i_solver_context::has_plugin(app* x) { - ast_manager& m = get_manager(); family_id fid = x->get_sort()->get_family_id(); return 0 <= fid && @@ -1281,7 +1279,6 @@ namespace qe { } qe_solver_plugin& i_solver_context::plugin(app* x) { - ast_manager& m = get_manager(); SASSERT(has_plugin(x)); return *(m_plugins[x->get_sort()->get_family_id()]); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index ec2b473d1..69db141b8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3588,7 +3588,6 @@ namespace sat { void solver::unassign_vars(unsigned old_sz, unsigned new_lvl) { SASSERT(old_sz <= m_trail.size()); SASSERT(m_replay_assign.empty()); - unsigned i = m_trail.size(); for (unsigned i = m_trail.size(); i-- > old_sz; ) { literal l = m_trail[i]; bool_var v = l.var(); diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index e69eb3cf2..820d2a532 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -264,7 +264,6 @@ namespace q { } void ematch::instantiate(binding& b, clause& c) { - quantifier* q = c.q(); if (m_stats.m_num_instantiations > ctx.get_config().m_qi_max_instances) return; unsigned max_generation = b.m_max_generation; diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 32420a7bf..90c74089c 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -513,7 +513,7 @@ namespace q { bool mbqi::first_offset(unsigned_vector& offsets, app_ref_vector const& vars) { offsets.reset(); - for (app* v : vars) + for (app* _ : vars) offsets.push_back(0); for (unsigned i = 0; i < vars.size(); ++i) if (!next_offset(offsets, vars, i, 0)) diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index fcd26ed53..7d35784db 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -71,7 +71,6 @@ namespace smt { proof * mk_proof(conflict_resolution & cr) override { ast_manager & m = cr.get_manager(); - context & ctx = cr.get_context(); unsigned num_args = m_app1->get_num_args(); proof_ref_vector prs(m); expr_ref_vector lits(m); diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index fb909100c..d167a5c57 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -319,6 +319,7 @@ namespace smt { void theory_arith::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) { // Ignore equality if variables are already known to be equal. ast_manager& m = get_manager(); + (void)m; if (is_equal(x, y)) return; // I doesn't make sense to propagate an equality (to the core) of variables of different sort. diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ca3efa157..d925c0b57 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1494,7 +1494,7 @@ bool theory_seq::internalize_term(app* term) { else { e = ctx.mk_enode(term, false, m.is_bool(term), true); } - theory_var v = mk_var(e); + mk_var(e); if (!ctx.relevancy()) { relevant_eh(term); } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index d7f6f2757..427aa48ac 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -307,7 +307,6 @@ namespace smt { } void theory_str::refresh_theory_var(expr * e) { - ast_manager & m = get_manager(); enode * en = ensure_enode(e); theory_var v = mk_var(en); (void)v; TRACE("str", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;); @@ -318,7 +317,6 @@ namespace smt { theory_var theory_str::mk_var(enode* n) { TRACE("str", tout << "mk_var for " << mk_pp(n->get_owner(), get_manager()) << std::endl;); - ast_manager & m = get_manager(); if (!(n->get_owner()->get_sort() == u.str.mk_string_sort())) { return null_theory_var; } @@ -6543,7 +6541,6 @@ namespace smt { } void theory_str::handle_equality(expr * lhs, expr * rhs) { - ast_manager & m = get_manager(); // both terms must be of sort String sort * lhs_sort = lhs->get_sort(); sort * rhs_sort = rhs->get_sort(); @@ -7117,7 +7114,6 @@ namespace smt { } void theory_str::recursive_check_variable_scope(expr * ex) { - ast_manager & m = get_manager(); if (is_app(ex)) { app * a = to_app(ex); @@ -9205,8 +9201,6 @@ namespace smt { } bool theory_str::flatten(expr* ex, expr_ref_vector & flat) { - ast_manager & m = get_manager(); - // TRACE("str", tout << "ex " << mk_pp(ex, m) << " target " << target << " length " << length << " sublen " << mk_pp(sublen, m) << " extra " << mk_pp(extra, m) << std::endl;); sort * ex_sort = ex->get_sort(); sort * str_sort = u.str.mk_string_sort(); diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index f4c06b818..72f0266c1 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -163,9 +163,9 @@ namespace { struct undo_bound { - expr* e; + expr* e { nullptr }; interval b; - bool fresh; + bool fresh { false }; undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} };