mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

#5777

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-16 10:52:25 -08:00
parent cd56d55e34
commit ea93345b75
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/sat_solver.cpp
View file

@ -3657,15 +3657,15 @@ namespace sat {
if (cw.is_binary()) { 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; 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; m_clauses_to_reinit[j++] = cw;
} }
else { else {
clause & c = *(cw.get_clause()); clause & c = *(cw.get_clause());
if (ENABLE_TERNARY && c.size() == 3) { 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; 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; m_clauses_to_reinit[j++] = cw;
else else
c.set_reinit_stack(false); c.set_reinit_stack(false);
@ -3673,10 +3673,10 @@ namespace sat {
} }
detach_clause(c); detach_clause(c);
attach_clause(c, reinit); attach_clause(c, reinit);
if (!at_base_lvl() && reinit) if (reinit && !at_base_lvl())
// clause propagated literal, must keep it in the reinit stack. // clause propagated literal, must keep it in the reinit stack.
m_clauses_to_reinit[j++] = cw; 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; m_clauses_to_reinit[j++] = cw;
else else
c.set_reinit_stack(false); c.set_reinit_stack(false);