#5778

add new clauses created during propagation to use-list
Z3Prover · Apr 2, 2022 · 97115e5 · 97115e5
1 parent 4cc3327
commit 97115e5
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
@@ -652,6 +652,7 @@ namespace sat {
 
     inline void simplifier::propagate_unit(literal l) {
         unsigned old_trail_sz = s.m_trail.size();
+        unsigned num_clauses = s.m_clauses.size();
         s.assign_scoped(l);
         s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state.
         if (s.inconsistent())
@@ -672,6 +673,8 @@ namespace sat {
             }
             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) {