mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

(mev) renamed variable to clarify that it is unused

Browse source
This commit is contained in:
Arie Gurfinkel 2017-06-21 20:53:30 -04:00
parent 1fee5fd94e
commit e62e563e2d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/model/model_evaluator.cpp
View file

@ -202,8 +202,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
void expand_value(expr_ref& val) {
vector<expr_ref_vector> stores;
expr_ref else_case(m());
bool args_are_unique;
if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, args_are_unique)) {
bool _unused;
if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) {
sort* srt = m().get_sort(val);
val = m_ar.mk_const_array(srt, else_case);
for (unsigned i = stores.size(); i > 0; ) {