From 97115e5ebdcad46bd8cd9ce5fa208cfa645e4b04 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Apr 2022 00:14:59 -0700
Subject: [PATCH] #5778

add new clauses created during propagation to use-list
---
 src/sat/sat_simplifier.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 5cb300725..b3521452b 100644
--- 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) {