mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

bug in flatten/and/or introduced when skipping sub-expressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-22 07:43:37 -08:00
parent 4b5ee91b44
commit cf6486f990
1 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/ast_util.cpp
View file

@ -264,8 +264,12 @@ void flatten_and(expr_ref_vector& result) {
expr_fast_mark1 seen; expr_fast_mark1 seen;
for (unsigned i = 0; i < result.size(); ++i) { for (unsigned i = 0; i < result.size(); ++i) {
expr* e = result.get(i); expr* e = result.get(i);
if (seen.is_marked(e)) if (seen.is_marked(e)) {
result[i] = result.back();
result.pop_back();
--i;
continue; continue;
}
seen.mark(e); seen.mark(e);
pin.push_back(e); pin.push_back(e);
if (m.is_and(e)) { if (m.is_and(e)) {
@ -330,8 +334,12 @@ void flatten_or(expr_ref_vector& result) {
expr_fast_mark1 seen; expr_fast_mark1 seen;
for (unsigned i = 0; i < result.size(); ++i) { for (unsigned i = 0; i < result.size(); ++i) {
expr* e = result.get(i); expr* e = result.get(i);
if (seen.is_marked(e)) if (seen.is_marked(e)) {
result[i] = result.back();
result.pop_back();
--i;
continue; continue;
}
seen.mark(e); seen.mark(e);
pin.push_back(e); pin.push_back(e);
if (m.is_or(e)) { if (m.is_or(e)) {