mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Remove unused variables

Browse source
This commit is contained in:
Daniel Schemmel 2019-07-23 11:09:50 +02:00
parent 364fbda925
commit 5e5c231712
No known key found for this signature in database
GPG key ID: A176732062461ECC
2 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/seq_rewriter.cpp
View file

@ -704,7 +704,6 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
if (!get_lengths(b, lens, pos)) {
return BR_FAILED;
}
unsigned rsz = lens.size();
unsigned i = 0;
for (; i < m_lhs.size(); ++i) {
expr* lhs = m_lhs.get(i);

2
src/model/model_evaluator.cpp
View file

@ -238,8 +238,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
func_decl* g = nullptr;
VERIFY(m_ar.is_as_array(f, g));
expr* def = nullptr;
quantifier* q = nullptr;
proof* def_pr = nullptr;
if (m_def_cache.find(g, def)) {
result = def;
return BR_DONE;