From a15a7cee7bd7528e1e5b8e29f77083a03daa4ad8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 Dec 2023 14:13:05 -0800 Subject: [PATCH] touch Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/hoist_rewriter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp index 7b217fc2421..1b99469a190 100644 --- a/src/ast/rewriter/hoist_rewriter.cpp +++ b/src/ast/rewriter/hoist_rewriter.cpp @@ -137,6 +137,7 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & m_subst.insert(p, m.mk_true()); fmls.push_back(p); } + bool new_eq = false; for (auto& [a, b] : m_eqs) { if (m.is_value(a)) std::swap(a, b); @@ -146,6 +147,7 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result = m.mk_false(); return BR_DONE; } + new_eq = true; m_subst.insert(a, b); fmls.push_back(m.mk_eq(a, b)); } @@ -154,7 +156,7 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & fmls.push_back(ors); result = mk_and(fmls); TRACE("hoist", tout << ors << " => " << result << "\n";); - return BR_DONE; + return new_eq ? BR_REWRITE3 : BR_DONE; } unsigned hoist_rewriter::mk_var(expr* e) {