diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp
index a9f36b818..56c4a1b7a 100644
--- a/src/sat/sat_proof_trim.cpp
+++ b/src/sat/sat_proof_trim.cpp
@@ -56,6 +56,7 @@ namespace sat {
             IF_VERBOSE(4, verbose_stream() << cl << " in-core " << in_core(cl) << ": "; for (auto const& [k,v] : m_clauses) verbose_stream() << "{" << v.m_clauses << "} "; verbose_stream() << "\n");
 
             m_result.push_back({id, unsigned_vector()});
+            m_in_deps.reset();
             if (is_initial)
                 continue;
             conflict_analysis_core(cl, clp);            
@@ -219,6 +220,7 @@ namespace sat {
     }
 
     void proof_trim::add_dependency(literal lit) {
+        IF_VERBOSE(3, verbose_stream() << "add dependency " << lit << "\n");
         bool_var v = lit.var();
         if (m_propagated[v]) { // literal was propagated after assuming ~C
             if (!s.is_marked(v))
@@ -253,6 +255,12 @@ namespace sat {
         add_core(lit, j);
     }
 
+    void proof_trim::insert_dep(unsigned dep) {
+        if (m_in_deps.contains(dep))
+            return;
+        m_in_deps.insert(dep);
+        m_result.back().second.push_back(dep);
+    }
 
     void proof_trim::add_core(literal l, justification j) {
         m_clause.reset();
@@ -277,14 +285,18 @@ namespace sat {
         IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n");
         auto& [clauses, id, in_core] = m_clauses.find(m_clause);
         in_core = true;
-        m_result.back().second.push_back(id);
-        if (l != null_literal && s.lvl(l) == 0 && m_clause.size() > 1) {
-            m_clause.reset();
-            m_clause.push_back(l);
-            auto& [clauses, id, in_core] = m_clauses.insert_if_not_there(m_clause, {{}, 0, true });
-            in_core = true;
-            if (id != 0)
-                m_result.back().second.push_back(id);
+        insert_dep(id);
+        if (m_clause.size() > 1 && l != null_literal && s.lvl(l) == 0) {
+            for (auto lit : m_clause) {
+                if (s.lvl(lit) != 0)
+                    continue;
+                m_clause2.reset();
+                m_clause2.push_back(s.value(lit) == l_false ? ~lit : lit);
+                auto& [clauses, id, in_core] = m_clauses.insert_if_not_there(m_clause2, {{}, UINT_MAX, true });
+                in_core = true;
+                if (id != UINT_MAX)
+                    insert_dep(id);
+            }
         }
     }
 
diff --git a/src/sat/sat_proof_trim.h b/src/sat/sat_proof_trim.h
index 24091e69c..11e460eb6 100644
--- a/src/sat/sat_proof_trim.h
+++ b/src/sat/sat_proof_trim.h
@@ -30,7 +30,8 @@ namespace sat {
 
     class proof_trim {
         solver         s;
-        literal_vector m_clause, m_conflict;        
+        literal_vector m_clause, m_clause2, m_conflict;
+        uint_set       m_in_deps;
         uint_set       m_in_clause;
         uint_set       m_in_coi;
         clause*        m_conflict_clause = nullptr;
@@ -72,6 +73,8 @@ namespace sat {
         void revive(literal_vector const& cl, clause* cp);        
         clause* del(literal_vector const& cl);
 
+        void insert_dep(unsigned dep);
+
         uint_set m_units;
         bool unit_or_binary_occurs();
         void set_conflict(literal_vector const& c, clause* cp) { m_conflict.reset(); m_conflict.append(c); m_conflict_clause = cp;}