diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp
index 0965439ae..e2a19446d 100644
--- a/src/cmd_context/extra_cmds/proof_cmds.cpp
+++ b/src/cmd_context/extra_cmds/proof_cmds.cpp
@@ -43,6 +43,7 @@ Proof checker for clauses created during search.
 #include "util/small_object_allocator.h"
 #include "ast/ast_util.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/arith_decl_plugin.h"
 #include "smt/smt_solver.h"
 #include "sat/sat_solver.h"
 #include "sat/sat_drat.h"
@@ -132,7 +133,7 @@ public:
                 clause1.push_back(hint);
                 trim.assume(m_clauses.size());
                 m_clauses.push_back(clause1);                
-                m_is_infer.push_back(false);
+                m_is_infer.push_back(true);
                 
                 if (clause.empty()) {
                     mk_clause(clause);
@@ -167,12 +168,22 @@ public:
         trim.updt_params(p);
     }
 
+    expr_ref mk_dep(unsigned id, unsigned_vector const& deps) {
+        arith_util a(m);
+        expr_ref_vector args(m);
+        args.push_back(a.mk_int(id));
+        for (auto d : deps)
+            args.push_back(a.mk_int(d));
+        return expr_ref(m.mk_app(symbol("deps"), args.size(), args.data(), m.mk_proof_sort()), m);
+    }
+
     void do_trim(std::ostream& out) {
         ast_pp_util pp(m);
         auto ids = trim.trim();
-        for (unsigned id : ids) {
-            auto const& clause = m_clauses[id];
+        for (auto const& [id, deps] : ids) {
+            auto& clause = m_clauses[id];
             bool is_infer = m_is_infer[id];
+            clause.push_back(mk_dep(id, deps));            
             for (expr* e : clause) 
                 pp.collect(e);
             
@@ -268,8 +279,10 @@ public:
     }
 
     void add_literal(expr* e) override {
-        if (m.is_proof(e))
-            m_proof_hint = to_app(e);
+        if (m.is_proof(e)) {
+            if (!m_proof_hint)
+                m_proof_hint = to_app(e);
+        }
         else if (!m.is_bool(e))
             throw default_exception("literal should be either a Proof or Bool");
         else
diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp
index ee35efe09..b4171f51d 100644
--- a/src/sat/sat_proof_trim.cpp
+++ b/src/sat/sat_proof_trim.cpp
@@ -29,19 +29,20 @@ namespace sat {
        Output: reduced trail - result                                                                           
     */        
 
-    unsigned_vector proof_trim::trim() {
-        unsigned_vector result;
+    vector<std::pair<unsigned, unsigned_vector>> proof_trim::trim() {
+        m_result.reset();
         m_core_literals.reset();
         m_propagated.resize(num_vars(), false);  
         m_core_literals.insert(literal_vector());
         m_core_literals.insert(m_conflict);
-        conflict_analysis_core(m_conflict, m_conflict_clause);
+
 
         IF_VERBOSE(10, s.display(verbose_stream() << "trim\n"));
 
         auto const& [id, cl, clp, is_add, is_initial] = m_trail.back();
         SASSERT(cl.empty());
-        result.push_back(id);
+        m_result.push_back({id, unsigned_vector()});
+        conflict_analysis_core(m_conflict, m_conflict_clause);
         m_trail.pop_back();
         
 
@@ -55,17 +56,17 @@ namespace sat {
             prune_trail(cl, clp);
             IF_VERBOSE(10, s.display(verbose_stream() << "\n"));
             del(cl, clp);
-            if (!in_core(cl, clp)) 
+            if (!in_core(cl)) 
                 continue;
-            IF_VERBOSE(4, verbose_stream() << cl << " in-core " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} "; verbose_stream() << "\n");
+            IF_VERBOSE(4, verbose_stream() << cl << " in-core " << in_core(cl) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} "; verbose_stream() << "\n");
 
-            result.push_back(id);
+            m_result.push_back({id, unsigned_vector()});
             if (is_initial)
                 continue;
             conflict_analysis_core(cl, clp);            
         }
-        result.reverse();
-        return result;
+        m_result.reverse();
+        return m_result;
     }
     
     void proof_trim::del(literal_vector const& cl, clause* cp) {
@@ -75,20 +76,6 @@ namespace sat {
         else 
             del(cl);
     }
-    
-    bool proof_trim::match_clause(literal_vector const& cl, literal l1, literal l2) const {
-        return cl.size() == 2 && ((l1 == cl[0] && l2 == cl[1]) || (l1 == cl[1] && l2 == cl[0]));
-    }
-    
-    bool proof_trim::match_clause(literal_vector const& cl, literal l1, literal l2, literal l3) const {
-        return cl.size() == 3 &&
-            ((l1 == cl[0] && l2 == cl[1] && l3 == cl[2]) ||
-             (l1 == cl[0] && l2 == cl[2] && l3 == cl[1]) ||
-             (l1 == cl[1] && l2 == cl[0] && l3 == cl[2]) ||
-             (l1 == cl[1] && l2 == cl[2] && l3 == cl[0]) ||
-             (l1 == cl[2] && l2 == cl[1] && l3 == cl[0]) ||
-             (l1 == cl[2] && l2 == cl[0] && l3 == cl[1]));
-    }
 
     /**
      * cl is on the trail if there is some literal l that is implied by cl
@@ -294,6 +281,9 @@ namespace sat {
         }
         std::sort(m_clause.begin(), m_clause.end());
         IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n");
+        unsigned id;
+        VERIFY(m_clause2id.find(m_clause, id));
+        m_result.back().second.push_back(id);
         m_core_literals.insert(m_clause);
         if (l != null_literal && s.lvl(l) == 0) {
             m_clause.reset();
@@ -302,7 +292,7 @@ namespace sat {
         }
     }
 
-    bool proof_trim::in_core(literal_vector const& cl, clause* cp) const {
+    bool proof_trim::in_core(literal_vector const& cl) const {
         return m_core_literals.contains(cl);
     }
 
@@ -346,10 +336,6 @@ namespace sat {
         s.set_trim();
     }
 
-    proof_trim::~proof_trim() {
-    }
-
-
     void proof_trim::assume(unsigned id, bool is_initial) {
         std::sort(m_clause.begin(), m_clause.end());
         if (unit_or_binary_occurs())
@@ -360,6 +346,8 @@ namespace sat {
             return;        
 
         IF_VERBOSE(3, verbose_stream() << (is_initial?"assume ":"rup ") << m_clause << "\n");
+        std::sort(m_clause.begin(), m_clause.end());
+        m_clause2id.insert(m_clause, id);
         auto* cl = s.mk_clause(m_clause, status::redundant());
 
         auto is_unit2 = [&]() {
@@ -393,7 +381,6 @@ namespace sat {
         else if (m_clause.size() > 2 && is_unit())
             s.propagate_clause(*cl, true, 0, s.cls_allocator().get_offset(cl));
         s.propagate(false);
-        // verbose_stream() << m_clause << " - " << s.inconsistent() << "\n";
         if (s.inconsistent() ||  all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; }))
             set_conflict(m_clause, cl);
         
diff --git a/src/sat/sat_proof_trim.h b/src/sat/sat_proof_trim.h
index 6508f5a18..9a43315f3 100644
--- a/src/sat/sat_proof_trim.h
+++ b/src/sat/sat_proof_trim.h
@@ -35,7 +35,7 @@ namespace sat {
         uint_set       m_in_coi;
         clause*        m_conflict_clause = nullptr;
         vector<std::tuple<unsigned, literal_vector, clause*, bool, bool>> m_trail;
-        
+        vector<std::pair<unsigned, unsigned_vector>> m_result;
         
         struct hash {
             unsigned operator()(literal_vector const& v) const {
@@ -48,15 +48,13 @@ namespace sat {
             }
         };
         map<literal_vector, clause_vector, hash, eq> m_clauses;
+        map<literal_vector, unsigned, hash, eq>      m_clause2id;
 
         hashtable<literal_vector, hash, eq> m_core_literals;
         bool_vector                         m_propagated;
 
         void del(literal_vector const& cl, clause* cp);
 
-        bool match_clause(literal_vector const& cl, literal l1, literal l2) const;
-        bool match_clause(literal_vector const& cl, literal l1, literal l2, literal l3) const;
-
         void prune_trail(literal_vector const& cl, clause* cp);
         void conflict_analysis_core(literal_vector const& cl, clause* cp);
 
@@ -64,7 +62,7 @@ namespace sat {
         void add_dependency(justification j);
         void add_core(bool_var v);
         void add_core(literal l, justification j);
-        bool in_core(literal_vector const& cl, clause* cp) const;
+        bool in_core(literal_vector const& cl) const;
         void revive(literal_vector const& cl, clause* cp);        
         clause* del(literal_vector const& cl);
         void save(literal_vector const& lits, clause* cl);
@@ -76,7 +74,6 @@ namespace sat {
     public:
 
         proof_trim(params_ref const& p, reslimit& lim);
-        ~proof_trim();
 
         bool_var mk_var() { return s.mk_var(true, true); }
         void init_clause() { m_clause.reset(); }
@@ -88,7 +85,7 @@ namespace sat {
         void infer(unsigned id);
         void updt_params(params_ref const& p) { s.updt_params(p); }
 
-        unsigned_vector trim();
+        vector<std::pair<unsigned, unsigned_vector>> trim();
 
     };
 }