From ba8d8f0af746040f9c39f9da35c6acf30d3c0409 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Dec 2023 15:40:47 -0800 Subject: [PATCH] Disable hoist entirely, it is bad on QF_LIA and does not help on other observed cases --- src/ast/rewriter/bool_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index a92799c4c..7728716fd 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -270,7 +270,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args return BR_DONE; } -#if 1 +#if 0 br_status st; expr_ref r(m()); st = m_hoist.mk_or(buffer.size(), buffer.data(), r); @@ -282,7 +282,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args get_num_internal_exprs(m_counts2, m_todo2, args[i]); unsigned count1 = count_internal_nodes(m_counts1, m_todo1); unsigned count2 = count_internal_nodes(m_counts2, m_todo2); - if (count1 > count2 + num_args) + if (count1 > count2) st = BR_FAILED; } if (st != BR_FAILED)