mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

qe_lite: simplify definitions before deciding on elimination order

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-30 11:59:57 -07:00
parent b120923dd5
commit 0452bc3d43
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/qe/qe_lite.cpp
View file

@ -142,10 +142,10 @@ namespace eq {
} }
else { else {
SASSERT(fr.second == 1); SASSERT(fr.second == 1);
visiting.reset_mark(t); visiting.reset_mark(t);
if (!done.is_marked(t)) { if (!done.is_marked(t)) {
if (definitions.get(vidx, nullptr) != nullptr) if (definitions.get(vidx, nullptr) != nullptr)
order.push_back(vidx); order.push_back(vidx);
done.mark(t); done.mark(t);
} }
} }