From ea93345b755c739c75265289016c19260f1ff2db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Jan 2022 10:52:25 -0800 Subject: [PATCH] #5777 --- src/sat/sat_solver.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0e72de37f..c6d3ad3ae 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3655,17 +3655,17 @@ namespace sat { clause_wrapper cw = m_clauses_to_reinit[i]; bool reinit = false; if (cw.is_binary()) { - if (propagate_bin_clause(cw[0], cw[1]) && !at_base_lvl()) + if (propagate_bin_clause(cw[0], cw[1]) && !at_base_lvl()) m_clauses_to_reinit[j++] = cw; - else if (has_variables_to_reinit(cw[0], cw[1])) + else if (has_variables_to_reinit(cw[0], cw[1]) && !at_base_lvl()) m_clauses_to_reinit[j++] = cw; } else { clause & c = *(cw.get_clause()); if (ENABLE_TERNARY && c.size() == 3) { - if (!at_base_lvl() && propagate_ter_clause(c)) + if (propagate_ter_clause(c) && !at_base_lvl()) m_clauses_to_reinit[j++] = cw; - else if (has_variables_to_reinit(c)) + else if (has_variables_to_reinit(c) && !at_base_lvl()) m_clauses_to_reinit[j++] = cw; else c.set_reinit_stack(false); @@ -3673,13 +3673,13 @@ namespace sat { } detach_clause(c); attach_clause(c, reinit); - if (!at_base_lvl() && reinit) + if (reinit && !at_base_lvl()) // clause propagated literal, must keep it in the reinit stack. m_clauses_to_reinit[j++] = cw; - else if (has_variables_to_reinit(c)) + else if (has_variables_to_reinit(c) && !at_base_lvl()) m_clauses_to_reinit[j++] = cw; else - c.set_reinit_stack(false); + c.set_reinit_stack(false); } } m_clauses_to_reinit.shrink(j);