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

bug in qe_lite

Browse source
This commit is contained in:
Arie Gurfinkel 2019-08-08 15:06:26 -04:00 • committed by Nikolaj Bjorner
parent e2d91ce1fc
commit 52acbf1f14
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/qe/qe_lite.cpp
View file

@ -145,6 +145,7 @@ namespace eq {
continue; continue;
if (is_sub_extract(vars[i]->get_idx(), definitions[i])) { if (is_sub_extract(vars[i]->get_idx(), definitions[i])) {
order.push_back(i); order.push_back(i);
done.mark(definitions[i]);
continue; continue;
} }
var * v = vars[i]; var * v = vars[i];