mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

qe_lite: bug fix in der::der_sort_vars()

Browse source 
The case of

VAR 1 = (+ (:var 2) 10)
VAR 2 = (+ 0 foo)

was not properly handled whenever VAR2 has only one reference.
In that case, VAR2 is not marked as done when VAR1 is processed,
causing VAR2 to be duplicated in elimination order
This commit is contained in:
Arie Gurfinkel 2018-05-30 11:54:57 -07:00
parent fb52c36210
commit b120923dd5
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/qe/qe_lite.cpp
View file

@ -142,10 +142,10 @@ namespace eq {
}
else {
SASSERT(fr.second == 1);
visiting.reset_mark(t);
visiting.reset_mark(t);
if (!done.is_marked(t)) {
if (definitions.get(vidx, nullptr) != nullptr)
order.push_back(vidx);
order.push_back(vidx);
done.mark(t);
}
}
@ -444,7 +444,7 @@ namespace eq {
expr_ref r(m);
m_subst(cur, m_subst_map.size(), m_subst_map.c_ptr(), r);
unsigned inx = sz - m_order[i]- 1;
SASSERT(m_subst_map[inx]==0);
SASSERT(m_subst_map[inx]==nullptr);
m_subst_map[inx] = r;
}
}