From f01d096fb583bdc7fa46bc8f9db6dc5ffd706cab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Dec 2021 09:51:15 -0800 Subject: [PATCH] fix again --- src/ast/ast_util.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 85d7021c0..69b63af0f 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -260,8 +260,8 @@ expr_ref mk_distinct(expr_ref_vector const& args) { void flatten_and(expr_ref_vector& result) { ast_manager& m = result.get_manager(); expr* e1, *e2, *e3; - expr_fast_mark1 seen; expr_ref_vector pin(m); + expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++i) { expr* e = result.get(i); if (seen.is_marked(e)) @@ -326,8 +326,8 @@ void flatten_and(expr_ref& fml) { void flatten_or(expr_ref_vector& result) { ast_manager& m = result.get_manager(); expr* e1, *e2, *e3; - expr_fast_mark1 seen; expr_ref_vector pin(m); + expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++i) { expr* e = result.get(i); if (seen.is_marked(e))