From 476b06fa14c7bc5641150f8c359b5dbf14bac711 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Sep 2016 16:42:07 -0700 Subject: [PATCH] fix compiler warnings, gcc Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_bounds.cpp | 4 +--- src/ast/rewriter/bv_rewriter.cpp | 1 - src/smt/smt_consequences.cpp | 2 -- src/smt/smt_model_checker.cpp | 2 ++ 4 files changed, 3 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp index 9d3ca8c76..0f82a85c9 100644 --- a/src/ast/rewriter/bv_bounds.cpp +++ b/src/ast/rewriter/bv_bounds.cpp @@ -85,7 +85,7 @@ bool bv_bounds::is_uleq(expr * e, expr * & v, numeral & c) { if (!m_bv_util.is_extract(eql)) return false; expr * const eql0 = to_app(eql)->get_arg(0); const unsigned eql0_sz = m_bv_util.get_bv_size(eql0); - if (!m_bv_util.get_extract_high(eql) == (eql0_sz - 1)) return false; + if (m_bv_util.get_extract_high(eql) != (eql0_sz - 1)) return false; if (!m_bv_util.is_numeral(eqr, eqr_val, eqr_sz)) return false; if (!eqr_val.is_zero()) return false; if (!m_bv_util.is_extract(ulel)) return false; @@ -245,7 +245,6 @@ void bv_bounds::reset() { } br_status bv_bounds::rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result) { - const family_id fid = f->get_family_id(); if (!m_m.is_bool(f->get_range())) return BR_FAILED; const decl_kind k = f->get_decl_kind(); if ((k != OP_OR && k != OP_AND) || num > limit) return BR_FAILED; @@ -614,7 +613,6 @@ bool bv_bounds::is_sat(app * v) { bool bv_bounds::is_sat_core(app * v) { SASSERT(m_bv_util.is_bv(v)); if (!m_okay) return false; - func_decl * const d = v->get_decl(); unsigned const bv_sz = m_bv_util.get_bv_size(v); numeral lower, upper; const bool has_upper = m_unsigned_uppers.find(v, upper); diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index dcb5ba681..0246f2b16 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -622,7 +622,6 @@ unsigned bv_rewriter::propagate_extract(unsigned high, expr * arg, expr_ref & re } // perform removal SASSERT(removable <= to_remove); - const unsigned new_sz = sz - removable; ptr_buffer new_args; ptr_buffer new_concat_args; for (unsigned i = 0; i < num; i++) { diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 65dca4918..8619ff815 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -473,9 +473,7 @@ namespace smt { tout << "lits: " << num_units << "\n";); m_case_split_queue->init_search_eh(); unsigned num_iterations = 0; - unsigned model_threshold = 2; unsigned num_fixed_eqs = 0; - unsigned num_reiterations = 0; unsigned chunk_size = 100; while (!var2val.empty()) { diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 980270ded..c17211664 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -158,11 +158,13 @@ namespace smt { TRACE("model_checker", tout << "Could not get value for " << sk_d->get_name() << "\n";); return false; // get_some_value failed... giving up } + TRACE("model_checker", tout << "Got some value " << sk_value << "\n";); } if (use_inv) { unsigned sk_term_gen; expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen); if (sk_term != 0) { + TRACE("model_checker", tout << "Found inverse " << mk_pp(sk_term, m) << "\n";); SASSERT(!m.is_model_value(sk_term)); if (sk_term_gen > max_generation) max_generation = sk_term_gen;