From cf6486f990dfa638977bfcd17d6cffd2c735ad34 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Dec 2021 07:43:37 -0800 Subject: [PATCH] bug in flatten/and/or introduced when skipping sub-expressions Signed-off-by: Nikolaj Bjorner --- src/ast/ast_util.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 69b63af0f..090a2ff9d 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -264,8 +264,12 @@ void flatten_and(expr_ref_vector& result) { expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++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; + } seen.mark(e); pin.push_back(e); if (m.is_and(e)) { @@ -330,8 +334,12 @@ void flatten_or(expr_ref_vector& result) { expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++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; + } seen.mark(e); pin.push_back(e); if (m.is_or(e)) {