mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
removing warnings for unused variables, #579
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
96e157e201
commit
40f8e16273
|
@ -542,10 +542,11 @@ namespace simplex {
|
|||
continue;
|
||||
}
|
||||
SASSERT(!rows.contains(c.m_row_id));
|
||||
_row const& row = m_rows[c.m_row_id];
|
||||
_row_entry const& r = row.m_entries[c.m_row_idx];
|
||||
SASSERT(r.m_var == v);
|
||||
SASSERT((unsigned)r.m_col_idx == i);
|
||||
DEBUG_CODE(
|
||||
_row const& row = m_rows[c.m_row_id];
|
||||
_row_entry const& r = row.m_entries[c.m_row_idx];
|
||||
SASSERT(r.m_var == v);
|
||||
SASSERT((unsigned)r.m_col_idx == i););
|
||||
rows.insert(c.m_row_id);
|
||||
}
|
||||
int idx = col.m_first_free_idx;
|
||||
|
|
|
@ -861,11 +861,12 @@ namespace qe {
|
|||
|
||||
void operator()(expr_ref& fml, atom_set& pos, atom_set& neg) {
|
||||
expr_ref orig(fml);
|
||||
ast_manager& m = fml.get_manager();
|
||||
m_nnf_core(fml);
|
||||
m_normalize_literals(fml);
|
||||
m_collect_atoms(fml, pos, neg);
|
||||
TRACE("qe", tout << mk_ismt2_pp(orig, m) << "\n-->\n" << mk_ismt2_pp(fml, m) << "\n";);
|
||||
TRACE("qe",
|
||||
ast_manager& m = fml.get_manager();
|
||||
tout << mk_ismt2_pp(orig, m) << "\n-->\n" << mk_ismt2_pp(fml, m) << "\n";);
|
||||
}
|
||||
|
||||
void reset() {
|
||||
|
|
|
@ -306,9 +306,10 @@ namespace smt {
|
|||
|
||||
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
|
||||
SASSERT(values.size() == 1);
|
||||
ast_manager & m = m_th.get_manager();
|
||||
|
||||
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
|
||||
TRACE("t_fpa_detail",
|
||||
ast_manager & m = m_th.get_manager();
|
||||
for (unsigned i = 0; i < values.size(); i++)
|
||||
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
|
||||
|
||||
app * result = 0;
|
||||
|
|
|
@ -787,8 +787,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
for (unsigned i = 0; i < ineqs->size(); ++i) {
|
||||
ineq* c = (*ineqs)[i];
|
||||
SASSERT(c->is_ge());
|
||||
SASSERT((*ineqs)[i]->is_ge());
|
||||
if (assign_watch_ge(v, is_true, *ineqs, i)) {
|
||||
// i was removed from watch list.
|
||||
--i;
|
||||
|
@ -1834,13 +1833,12 @@ namespace smt {
|
|||
|
||||
void theory_pb::validate_assign(ineq const& c, literal_vector const& lits, literal l) const {
|
||||
uint_set nlits;
|
||||
context& ctx = get_context();
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
SASSERT(ctx.get_assignment(lits[i]) == l_true);
|
||||
SASSERT(get_context().get_assignment(lits[i]) == l_true);
|
||||
nlits.insert((~lits[i]).index());
|
||||
}
|
||||
SASSERT(ctx.get_assignment(l) == l_undef);
|
||||
SASSERT(ctx.get_assignment(c.lit()) == l_true);
|
||||
SASSERT(get_context().get_assignment(l) == l_undef);
|
||||
SASSERT(get_context().get_assignment(c.lit()) == l_true);
|
||||
nlits.insert(l.index());
|
||||
numeral sum = numeral::zero();
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
|
|
Loading…
Reference in a new issue