From 960b8566f51a97180373ca25096e1ba3aaa0a157 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 1 Jun 2019 15:45:17 +0700 Subject: [PATCH] Fix some unused variable warnings. --- src/smt/theory_array_bapa.cpp | 1 - src/tactic/tactic.cpp | 1 - 2 files changed, 2 deletions(-) diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index e79c64755..6d790b68d 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -348,7 +348,6 @@ namespace smt { expr_ref le(m_arith.mk_le(set_sz->get_arg(1), m_arith.mk_int(0)), m); literal le_lit = mk_literal(le); literal sz_lit = mk_literal(set_sz); - unsigned k = i.m_selects.size(); for (unsigned k = i.m_selects.size(); rational(k) < i.m_size; ++k) { expr_ref idx = mk_index_skolem(set_sz, set, k); app_ref sel(mk_select(set, idx), m); diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index bad35fa3e..53a3c4a24 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -154,7 +154,6 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result) { lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { bool models_enabled = g->models_enabled(); - bool proofs_enabled = g->proofs_enabled(); bool cores_enabled = g->unsat_core_enabled(); md = nullptr; pr = nullptr;