From 706f7fbdc786509169abbb8483f055da9e1689e7 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 22 Aug 2022 02:39:30 +0700 Subject: [PATCH] Fix some warnings about unused stuff. (#6290) --- src/smt/theory_arith_eq.h | 1 - src/smt/theory_dense_diff_logic_def.h | 1 - src/tactic/bv/bv_size_reduction_tactic.cpp | 4 +++- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index fabdb6abd4a..fab67a80136 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -328,7 +328,6 @@ namespace smt { return; } context & ctx = get_context(); - region & r = ctx.get_region(); enode * _x = get_enode(x); enode * _y = get_enode(y); eq_vector const& eqs = antecedents.eqs(); diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 46d2b0119f0..8f69c948953 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -591,7 +591,6 @@ namespace smt { get_antecedents(target, source, antecedents); if (l != null_literal) antecedents.push_back(l); - region & r = ctx.get_region(); ctx.set_conflict(ctx.mk_justification(theory_conflict_justification(get_id(), ctx, antecedents.size(), antecedents.data()))); return; diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 18083452b97..788f562d316 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -112,6 +112,7 @@ class bv_size_reduction_tactic : public tactic { unsigned bv_sz; expr * f, * lhs, * rhs; +#if 0 auto match_bitmask = [&](expr* lhs, expr* rhs) { unsigned lo, hi; expr* arg; @@ -131,7 +132,8 @@ class bv_size_reduction_tactic : public tactic { update_unsigned_upper(to_app(arg), val); return true; }; - +#endif + for (unsigned i = 0; i < sz; i++) { bool negated = false; f = g.form(i);