3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

fix unused-but-set-variable warnings reported in #579

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-18 11:02:10 -07:00
parent 9aaee8616a
commit 3a6e6df4f5
11 changed files with 19 additions and 8 deletions

View file

@ -342,6 +342,7 @@ public:
else
cls1.push_back(cls2[j]);
}
(void)found_pivot2;
assert(found_pivot2);
return;
}

View file

@ -362,6 +362,7 @@ public:
else
cls1.push_back(cls2[j]);
}
(void)found_pivot2;
assert(found_pivot2);
return;
}

View file

@ -300,6 +300,7 @@ public:
break;
case datalog::OK:
(void)query_exn;
SASSERT(query_exn);
break;

View file

@ -173,6 +173,7 @@ namespace datalog {
else {
processed = false;
}
(void)processed;
TRACE("dl", tout << (processed?"+ ":"- ") << mk_pp(e, m) << "\n";
if (processed) matrix::display_ineq(tout, row, M.b.back(), M.eq.back());
);

View file

@ -52,6 +52,7 @@ namespace sat {
bool clause::check_approx() const {
var_approx_set curr = m_approx;
(void)curr;
const_cast<clause*>(this)->update_approx();
SASSERT(may_eq(curr, m_approx));
return true;

View file

@ -159,7 +159,8 @@ namespace sat {
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
literal l = ~to_literal(l_idx);
watch_list const & wlist = *it;
CTRACE("sat_bug", s.was_eliminated(l.var()) && !wlist.empty(),
CTRACE("sat_bug",
s.was_eliminated(l.var()) && !wlist.empty(),
tout << "l: " << l << "\n";
s.display_watches(tout);
s.display(tout););
@ -179,7 +180,7 @@ namespace sat {
tout << "\n";
sat::display(tout, s.m_cls_allocator, s.get_wlist(~(it2->get_literal())));
tout << "\n";);
SASSERT(s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())));
SASSERT(s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())));
break;
case watched::TERNARY:
SASSERT(!s.was_eliminated(it2->get_literal1().var()));

View file

@ -739,6 +739,7 @@ public:
if (idx2 < idx1) {
std::swap(idx1,idx2);
}
(void) max_idx;
SASSERT(idx1 < idx2 && idx2 < edges.size());
SASSERT(max_idx < edges.size());
dst = get_source(edges[idx2]);

View file

@ -1342,6 +1342,7 @@ namespace smt {
tout << "v" << x_i << " ";
tout << (has_shared?"shared":"not shared") << "\n";);
(void) empty_column;
SASSERT(!safe_gain(min_gain, max_gain) ||
empty_column ||
(unbounded_gain(max_gain) == (x_i == null_theory_var)));

View file

@ -276,6 +276,7 @@ namespace smt {
SASSERT(r && bv_sz == m_ebits);
r = m_bu.is_numeral(values[2], sig_r, bv_sz);
SASSERT(r && bv_sz == m_sbits - 1);
(void)r;
SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator()));
SASSERT(mpzm.is_one(exp_r.to_mpq().denominator()));

View file

@ -156,6 +156,7 @@ class fm_tactic : public tactic {
r = c;
}
}
(void)found;
SASSERT(found);
return is_lower ? LOWER : UPPER;
}

View file

@ -280,7 +280,6 @@ bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
for (size_t j = numer.size()-1; j > 0; j--) {
temp = (((mpn_double_digit)numer[j]) << DIGIT_BITS) | ((mpn_double_digit)numer[j-1]);
q_hat = temp / (mpn_double_digit) denom;
r_hat = temp % (mpn_double_digit) denom;
if (q_hat >= BASE) {
UNREACHABLE(); // is this reachable with normalized v?
}
@ -294,11 +293,13 @@ bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
quot[j-1]--;
numer[j] = numer[j-1] + denom;
}
TRACE("mpn_div1", tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat;
tout << " ms=" << ms;
tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size());
tout << " borrow=" << borrow;
tout << std::endl; );
TRACE("mpn_div1",
r_hat = temp % (mpn_double_digit) denom;
tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat;
tout << " ms=" << ms;
tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size());
tout << " borrow=" << borrow;
tout << std::endl; );
}
return true; // return rem != 0?