From ddbca68270f68839553790f9cc4ba933e606ec6e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Oct 2022 11:05:09 -0700 Subject: [PATCH] minor formatting update --- src/sat/sat_solver.cpp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 15bc20a58..3012a840e 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -601,18 +601,17 @@ namespace sat { clause * r = alloc_clause(num_lits, lits, st.is_redundant()); SASSERT(!st.is_redundant() || r->is_learned()); bool reinit = attach_nary_clause(*r, st.is_sat() && st.is_redundant()); - if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r); - if (st.is_redundant()) { + + if (reinit || has_variables_to_reinit(*r)) + push_reinit_stack(*r); + if (st.is_redundant()) m_learned.push_back(r); - } - else { + else m_clauses.push_back(r); - } if (m_config.m_drat) m_drat.add(*r, st); - for (literal l : *r) { + for (literal l : *r) m_touched[l.var()] = m_touch_index; - } return r; }