mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

remove sources for unused variable warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-21 09:54:45 -08:00
parent d9227b95ea
commit 8d18fd075e
12 changed files with 20 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -312,11 +312,11 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
unsigned sbits = m_fpa_util.get_sbits(var->get_range());
app * a0 = to_app(val->get_arg(0));
app * a1 = to_app(val->get_arg(1));
app * a2 = to_app(val->get_arg(2));
expr_ref v0(m), v1(m), v2(m);
#ifdef Z3DEBUG
app * a1 = to_app(val->get_arg(1));
app * a2 = to_app(val->get_arg(2));
v0 = mc->get_const_interp(a0->get_decl());
v1 = mc->get_const_interp(a1->get_decl());
v2 = mc->get_const_interp(a2->get_decl());
@ -555,4 +555,4 @@ void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) {
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
});
}
}

5
src/ast/rewriter/bv_bounds.cpp
View file

@ -24,9 +24,8 @@ bv_bounds::~bv_bounds() {
bv_bounds::conv_res bv_bounds::record(app * v, numeral lo, numeral hi, bool negated, vector<ninterval>& nis) {
TRACE("bv_bounds", tout << "record0 " << mk_ismt2_pp(v, m_m) << ":" << (negated ? "~[" : "[") << lo << ";" << hi << "]" << std::endl;);
const unsigned bv_sz = m_bv_util.get_bv_size(v);
const numeral& zero = numeral::zero();
const numeral& one = numeral::one();
SASSERT(zero <= lo);
SASSERT(numerl::zero() <= lo);
SASSERT(lo <= hi);
SASSERT(hi < numeral::power_of_two(bv_sz));
numeral vmax, vmin;
@ -49,7 +48,7 @@ bv_bounds::conv_res bv_bounds::record(app * v, numeral lo, numeral hi, bool nega
hi_max = hi >= vmax;
lo_min = true;
}
SASSERT(zero <= lo);
SASSERT(lo.is_nonneg());
SASSERT(lo <= hi);
SASSERT(hi < numeral::power_of_two(bv_sz));
}

2
src/ast/simplifier/simplifier.cpp
View file

@ -650,10 +650,12 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
#define Grey 1
#define Black 2
#ifdef Z3DEBUG
static int get_color(obj_map<expr, int> & colors, expr * n) {
obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(n, White);
return entry->get_data().m_value;
}
#endif
static bool visit_ac_children(func_decl * f, expr * n, obj_map<expr, int> & colors, ptr_buffer<expr> & todo, ptr_buffer<expr> & result) {
if (is_app_of(n, f)) {