mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Fix some unused variable warnings.

Browse source
This commit is contained in:
Bruce Mitchener 2019-06-01 15:45:17 +07:00
parent 60e4cad7f1
commit 960b8566f5
2 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_array_bapa.cpp
View file

@ -348,7 +348,6 @@ namespace smt {
expr_ref le(m_arith.mk_le(set_sz->get_arg(1), m_arith.mk_int(0)), m);
literal le_lit = mk_literal(le);
literal sz_lit = mk_literal(set_sz);
unsigned k = i.m_selects.size();
for (unsigned k = i.m_selects.size(); rational(k) < i.m_size; ++k) {
expr_ref idx = mk_index_skolem(set_sz, set, k);
app_ref sel(mk_select(set, idx), m);