mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

#5778

Browse source 
add new clauses created during propagation to use-list
This commit is contained in:
Nikolaj Bjorner 2022-04-02 00:14:59 -07:00
parent 4cc33277fa
commit 97115e5ebd
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_simplifier.cpp
View file

@ -652,6 +652,7 @@ namespace sat {
inline void simplifier::propagate_unit(literal l) { inline void simplifier::propagate_unit(literal l) {
unsigned old_trail_sz = s.m_trail.size(); unsigned old_trail_sz = s.m_trail.size();
unsigned num_clauses = s.m_clauses.size();
s.assign_scoped(l); s.assign_scoped(l);
s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state. s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state.
if (s.inconsistent()) if (s.inconsistent())
@ -672,6 +673,8 @@ namespace sat {
} }
cs.reset(); cs.reset();
} }
for (unsigned i = num_clauses; i < s.m_clauses.size(); ++i)
m_use_list.insert(*s.m_clauses[i]);
} }
void simplifier::elim_lit(clause & c, literal l) { void simplifier::elim_lit(clause & c, literal l) {