mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

address unused variable warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-08-28 18:50:54 -07:00
parent 4d29925c3f
commit 6f2a6da600
4 changed files with 21 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/pp.cpp
View file

@ -66,7 +66,6 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
bool single_line = p.single_line();
unsigned pos = 0;
unsigned ribbon_pos = 0;
unsigned line = 0;
unsigned len;
unsigned i;
@ -92,7 +91,6 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
break;
}
pos += len;
ribbon_pos += len;
out << f->get_decl()->get_parameter(0).get_symbol();
break;
case OP_INDENT:
@ -121,7 +119,6 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
break;
}
pos = indent;
ribbon_pos = 0;
line++;
if (line < max_num_lines) {
out << "\n";

1
src/math/lp/emonics.cpp
View file

@ -546,6 +546,7 @@ bool emonics::invariant() const {
}
CTRACE("nla_solver_mons", !found, tout << "not found v" << v << ": " << m << "\n";);
SASSERT(found);
(void)found;
c = c->m_next;
}
while (c != ht.m_head);

8
src/model/model_evaluator.cpp
View file

@ -566,14 +566,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case, bool& are_unique) {
SASSERT(m_ar.is_array(a));
bool are_values = true;
are_unique = true;
TRACE("model_evaluator", tout << mk_pp(a, m) << "\n";);
while (m_ar.is_store(a)) {
expr_ref_vector store(m);
store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
are_values &= args_are_values(store, are_unique);
args_are_values(store, are_unique);
stores.push_back(store);
a = to_app(a)->get_arg(0);
}
@ -584,9 +583,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
if (m_ar_rw.has_index_set(a, else_case, stores)) {
for (auto const& store : stores) {
are_values &= args_are_values(store, are_unique);
}
for (auto const& store : stores)
args_are_values(store, are_unique);
return true;
}
if (!m_ar.is_as_array(a)) {

33
src/nlsat/nlsat_evaluator.cpp
View file

@ -286,22 +286,23 @@ namespace nlsat {
}
bool check_invariant() const {
SASSERT(m_sections.size() == m_sorted_sections.size());
for (unsigned i = 0; i < m_sorted_sections.size(); i++) {
SASSERT(m_sorted_sections[i] < m_sections.size());
SASSERT(m_sections[m_sorted_sections[i]].m_pos == i);
}
unsigned total_num_sections = 0;
unsigned total_num_signs = 0;
for (unsigned i = 0; i < m_info.size(); i++) {
SASSERT(m_info[i].m_first_section <= m_poly_sections.size());
SASSERT(m_info[i].m_num_roots == 0 || m_info[i].m_first_section < m_poly_sections.size());
SASSERT(m_info[i].m_first_sign < m_poly_signs.size());
total_num_sections += m_info[i].m_num_roots;
total_num_signs += m_info[i].m_num_roots + 1;
}
SASSERT(total_num_sections == m_poly_sections.size());
SASSERT(total_num_signs == m_poly_signs.size());
DEBUG_CODE(
SASSERT(m_sections.size() == m_sorted_sections.size());
for (unsigned i = 0; i < m_sorted_sections.size(); i++) {
SASSERT(m_sorted_sections[i] < m_sections.size());
SASSERT(m_sections[m_sorted_sections[i]].m_pos == i);
}
unsigned total_num_sections = 0;
unsigned total_num_signs = 0;
for (unsigned i = 0; i < m_info.size(); i++) {
SASSERT(m_info[i].m_first_section <= m_poly_sections.size());
SASSERT(m_info[i].m_num_roots == 0 || m_info[i].m_first_section < m_poly_sections.size());
SASSERT(m_info[i].m_first_sign < m_poly_signs.size());
total_num_sections += m_info[i].m_num_roots;
total_num_signs += m_info[i].m_num_roots + 1;
}
SASSERT(total_num_sections == m_poly_sections.size());
SASSERT(total_num_signs == m_poly_signs.size()););
return true;
}