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

minor formatting update

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-23 11:05:09 -07:00
parent 4a1d76cf49
commit ddbca68270
1 changed files with 6 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/sat/sat_solver.cpp
View file

@ -601,18 +601,17 @@ namespace sat {
clause * r = alloc_clause(num_lits, lits, st.is_redundant()); clause * r = alloc_clause(num_lits, lits, st.is_redundant());
SASSERT(!st.is_redundant() || r->is_learned()); SASSERT(!st.is_redundant() || r->is_learned());
bool reinit = attach_nary_clause(*r, st.is_sat() && st.is_redundant()); 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); m_learned.push_back(r);
} else
else {
m_clauses.push_back(r); m_clauses.push_back(r);
}
if (m_config.m_drat) if (m_config.m_drat)
m_drat.add(*r, st); m_drat.add(*r, st);
for (literal l : *r) { for (literal l : *r)
m_touched[l.var()] = m_touch_index; m_touched[l.var()] = m_touch_index;
}
return r; return r;
} }