From cc3bfe8da22e53ba74dbec25f04c2fb32db10ea4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 May 2016 16:02:08 -0700 Subject: [PATCH] removing warnings for unused variables, #579 Signed-off-by: Nikolaj Bjorner --- src/smt/qi_queue.cpp | 10 ++++------ src/smt/smt_model_finder.cpp | 3 +-- src/smt/theory_seq.cpp | 3 +-- 3 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index f9413be72..711cdc336 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -377,11 +377,10 @@ namespace smt { bool result = true; for (unsigned i = 0; i < sz; i++) { entry & e = m_delayed_entries[i]; - fingerprint * f = e.m_qb; - TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); + TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= min_cost) { TRACE("qi_queue", - tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(f->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); + tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); m_stats.m_num_lazy_instances++; @@ -394,11 +393,10 @@ namespace smt { bool result = true; for (unsigned i = 0; i < m_delayed_entries.size(); i++) { entry & e = m_delayed_entries[i]; - fingerprint * f = e.m_qb; - TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); + TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { TRACE("qi_queue", - tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(f->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); + tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); m_stats.m_num_lazy_instances++; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 1f4f26b06..5dc0dd8ec 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -3545,10 +3545,9 @@ namespace smt { // // Since we only care about q (and its bindings), it only makes sense to restrict the variables of q. bool asserted_something = false; - quantifier * flat_q = get_flat_quantifier(q); unsigned num_decls = q->get_num_decls(); // Remark: sks were created for the flat version of q. - SASSERT(flat_q->get_num_decls() == sks.size()); + SASSERT(get_flat_quantifier(q)->get_num_decls() == sks.size()); SASSERT(sks.size() >= num_decls); for (unsigned i = 0; i < num_decls; i++) { expr * sk = sks.get(num_decls - i - 1); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index f2bd8be84..97189ce4c 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3741,7 +3741,6 @@ expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned rej(s, idx, re, i) -> len(s) > idx if i is final */ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) { - context& ctx = get_context(); expr *s, * idx, *re; unsigned src; eautomaton* aut = 0; @@ -3752,7 +3751,7 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) { } if (m_util.str.is_length(idx)) return; SASSERT(m_autil.is_numeral(idx)); - SASSERT(ctx.get_assignment(lit) == l_true); + SASSERT(get_context().get_assignment(lit) == l_true); bool is_final = aut->is_final_state(src); if (is_final == is_acc) { propagate_lit(0, 1, &lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), idx)));