diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp
index 49a8da09c..0965439ae 100644
--- a/src/cmd_context/extra_cmds/proof_cmds.cpp
+++ b/src/cmd_context/extra_cmds/proof_cmds.cpp
@@ -63,6 +63,7 @@ class proof_trim {
     vector<expr_ref_vector> m_clauses;
     bool_vector             m_is_infer;
     symbol                  m_rup;
+    bool                    m_empty = false;
     
     void mk_clause(expr_ref_vector const& clause) {
         trim.init_clause();
@@ -121,25 +122,32 @@ public:
      */
     
     void infer(expr_ref_vector const& clause, app* hint) {
+        if (m_empty)
+            return;
+
         if (hint && !is_rup(hint) && m_checker.check(hint)) {
             auto clause1 = m_checker.clause(hint);
             if (clause1.size() != clause.size()) {
                 mk_clause(clause1);
-                trim.assume(m_clauses.size());
                 clause1.push_back(hint);
+                trim.assume(m_clauses.size());
                 m_clauses.push_back(clause1);                
-                m_is_infer.push_back(true);
-                mk_clause(clause);
-                trim.infer(m_clauses.size());
-                m_clauses.push_back(clause);
-                m_clauses.back().push_back(hint);
-                m_is_infer.push_back(true);
-                if (clause.empty()) 
+                m_is_infer.push_back(false);
+                
+                if (clause.empty()) {
+                    mk_clause(clause);
+                    trim.infer(m_clauses.size());                    
+                    m_clauses.push_back(clause);
+                    m_clauses.back().push_back(hint);
+                    m_is_infer.push_back(true);
+                    m_empty = true;
                     do_trim(std::cout);
+                }
                 return;
             }
         }
 
+
         mk_clause(clause);
         if (is_rup(hint))
             trim.infer(m_clauses.size());
@@ -149,8 +157,10 @@ public:
         if (hint)
             m_clauses.back().push_back(hint);
         m_is_infer.push_back(true);
-        if (clause.empty()) 
+        if (clause.empty()) {
+            m_empty = true;
             do_trim(std::cout);
+        }
     }
     
     void updt_params(params_ref const& p) {
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index 031ce9202..a8de05e0f 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -28,7 +28,7 @@ namespace sat {
     }
     
     // for nary clauses
-    static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) {
+    bool integrity_checker::contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) const {
         for (watched const& w : wlist) {
             if (w.is_clause()) {
                 if (w.get_clause_offset() == cls_off) {
@@ -38,6 +38,8 @@ namespace sat {
                 }
             }
         }
+        TRACE("sat", tout << "clause " << c << " not found in watch-list\n");
+        TRACE("sat", s.display_watches(tout));
         UNREACHABLE();
         return false;
     }
diff --git a/src/sat/sat_integrity_checker.h b/src/sat/sat_integrity_checker.h
index 22c8d0f5e..bc7fecf68 100644
--- a/src/sat/sat_integrity_checker.h
+++ b/src/sat/sat_integrity_checker.h
@@ -25,6 +25,7 @@ Revision History:
 namespace sat {
     class integrity_checker {
         solver const & s;
+        bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) const;
     public:
         integrity_checker(solver const & s);
         
diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp
index df55aecd7..ee35efe09 100644
--- a/src/sat/sat_proof_trim.cpp
+++ b/src/sat/sat_proof_trim.cpp
@@ -32,21 +32,33 @@ namespace sat {
     unsigned_vector proof_trim::trim() {
         unsigned_vector result;
         m_core_literals.reset();
+        m_propagated.resize(num_vars(), false);  
         m_core_literals.insert(literal_vector());
-        m_propagated.resize(num_vars(), false);
-        for (unsigned i = m_trail.size(); i-- > 0; ) {
+        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_trail.pop_back();
+        
+
+        for (unsigned i = m_trail.size(); i-- > 0; ) {            
             auto const& [id, cl, clp, is_add, is_initial] = m_trail[i];
             if (!is_add) {
                 revive(cl, clp);
                 continue;
-            }
+            }            
             IF_VERBOSE(10, s.display(verbose_stream()));
             prune_trail(cl, clp);
-            IF_VERBOSE(10, verbose_stream() << cl << " " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} ");
             IF_VERBOSE(10, s.display(verbose_stream() << "\n"));
             del(cl, clp);
-            if (!in_core(cl, clp))
+            if (!in_core(cl, clp)) 
                 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");
+
             result.push_back(id);
             if (is_initial)
                 continue;
@@ -57,6 +69,7 @@ namespace sat {
     }
     
     void proof_trim::del(literal_vector const& cl, clause* cp) {
+        CTRACE("sat", cp, tout << "del " << *cp << "\n");
         if (cp) 
             s.detach_clause(*cp);
         else 
@@ -90,6 +103,8 @@ namespace sat {
     void proof_trim::prune_trail(literal_vector const& cl, clause* cp) {
         m_in_clause.reset();
         m_in_coi.reset();
+
+        // verbose_stream() << "prune trail " << cl << "\n";
         
         if (cl.empty())
             return;
@@ -120,13 +135,23 @@ namespace sat {
             
             auto js = s.get_justification(l);
             bool in_coi = false;
+            //verbose_stream() << l << " " << js << "\n";
             if (js.is_clause())
-                for (literal lit : s.get_clause(j))
+                for (literal lit : s.get_clause(js))
                     in_coi |= m_in_coi.contains(lit.index());                
             else if (js.is_binary_clause())
                 in_coi = m_in_coi.contains(js.get_literal().index());
-            else
+            else if (js.is_none()) {                
+                verbose_stream() << "none " << js << "\n";
+            }
+            else if (js.is_ext_justification()) {
+                verbose_stream() << js << "\n";
                 UNREACHABLE(); // approach does not work for external justifications
+            }
+            else {
+                verbose_stream() << js << "\n";
+                UNREACHABLE(); // approach does not work for external justifications
+            }
             
             if (in_coi) 
                 unassign_literal(l);
@@ -134,6 +159,7 @@ namespace sat {
                 s.m_trail[j++] = s.m_trail[i];
         }            
         s.m_trail.shrink(j);
+        // verbose_stream() << "trail after " << s.m_trail << "\n";
         s.m_inconsistent = false; 
         s.m_qhead = s.m_trail.size();
         s.propagate(false);
@@ -188,11 +214,14 @@ namespace sat {
                 m_propagated[s.m_trail[i].var()] = true;
         }
         SASSERT(s.inconsistent());
-        IF_VERBOSE(3, verbose_stream() << s.m_not_l << " " << s.m_conflict << "\n");
+        IF_VERBOSE(3, s.display_justification(verbose_stream() << "conflict " << s.m_not_l << " ", s.m_conflict) << "\n");
+        IF_VERBOSE(3, s.display(verbose_stream()));
+        sat::literal l = sat::null_literal;
         if (s.m_not_l != null_literal) {
-            add_core(~s.m_not_l, s.m_conflict);
             add_dependency(s.m_not_l);
+            l = ~s.m_not_l;
         }
+        add_core(l, s.m_conflict);
         add_dependency(s.m_conflict);
         
         for (unsigned i = s.m_trail.size(); i-- > trail_size0; ) {
@@ -201,7 +230,7 @@ namespace sat {
             if (!s.is_marked(v))
                 continue;
             add_core(v);
-            s.reset_mark(v);
+            s.reset_mark(v);            
             add_dependency(s.get_justification(v));
         }
         if (!cl.empty())
@@ -210,8 +239,10 @@ namespace sat {
 
     void proof_trim::add_dependency(literal lit) {
         bool_var v = lit.var();
-        if (m_propagated[v]) // literal was propagated after assuming ~C
-            s.mark(v);        
+        if (m_propagated[v]) { // literal was propagated after assuming ~C
+            if (!s.is_marked(v))
+                s.mark(v);
+        }
         else if (s.lvl(v) == 0)  // literal depends on level 0, it is not assumed by ~C
             // inefficient for repeated insertions ? 
             add_core(v);                       
@@ -253,17 +284,18 @@ namespace sat {
             m_clause.push_back(j.get_literal());
             break;
         case justification::CLAUSE:
-            s.get_clause(j).mark_used();
-            IF_VERBOSE(3, verbose_stream() << "add core " << s.get_clause(j) << "\n");
-            return;
+            for (auto lit : s.get_clause(j))
+                m_clause.push_back(lit);
+            break;
         default:
+            verbose_stream() << j << "\n";
             UNREACHABLE();
             break;
         }
         std::sort(m_clause.begin(), m_clause.end());
         IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n");
         m_core_literals.insert(m_clause);
-        if (s.lvl(l) == 0) {
+        if (l != null_literal && s.lvl(l) == 0) {
             m_clause.reset();
             m_clause.push_back(l);
             m_core_literals.insert(m_clause);
@@ -271,10 +303,7 @@ namespace sat {
     }
 
     bool proof_trim::in_core(literal_vector const& cl, clause* cp) const {
-        if (cp)
-            return cp->was_used();
-        else
-            return m_core_literals.contains(cl);
+        return m_core_literals.contains(cl);
     }
 
     void proof_trim::revive(literal_vector const& cl, clause* cp) {
@@ -286,7 +315,7 @@ namespace sat {
 
     clause* proof_trim::del(literal_vector const& cl) {
         clause* cp = nullptr;
-        IF_VERBOSE(3, verbose_stream() << "del: " << cl << "\n");
+        TRACE("sat", tout << "del: " << cl << "\n");
         if (cl.size() == 2) {
             s.detach_bin_clause(cl[0], cl[1], true);
             return cp;
@@ -297,7 +326,7 @@ namespace sat {
         auto& v = e->get_data().m_value;
         if (!v.empty()) {
             cp = v.back();
-            IF_VERBOSE(3, verbose_stream() << "del: " << *cp << "\n");
+            TRACE("sat", tout << "del: " << *cp << "\n");
             s.detach_clause(*cp);
             v.pop_back();
         }
@@ -317,14 +346,57 @@ 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())
             return;
+        if (!m_conflict.empty() && m_clause.empty())
+            m_trail.push_back({id , m_clause, nullptr, true, is_initial});
+        if (!m_conflict.empty())
+            return;        
+
         IF_VERBOSE(3, verbose_stream() << (is_initial?"assume ":"rup ") << m_clause << "\n");
         auto* cl = s.mk_clause(m_clause, status::redundant());
+
+        auto is_unit2 = [&]() {
+            if (s.value(m_clause[0]) == l_false) {
+                std::swap(m_clause[0], m_clause[1]);
+                return true;
+            }
+            return s.value(m_clause[1]) == l_false;
+        };
+
+        auto is_unit = [&]() {
+            unsigned undef_idx = m_clause.size();
+            for (unsigned i = 0; i < m_clause.size(); ++i) {
+                sat::literal lit = (*cl)[i];
+                if (s.value(lit) != l_undef)
+                    continue;
+                if (undef_idx < m_clause.size())
+                    return false;
+                undef_idx = i;
+            }
+            if (undef_idx < m_clause.size()) {
+                std::swap((*cl)[undef_idx], (*cl)[0]);
+                return true;
+            }
+            return false;
+        };
+
         m_trail.push_back({ id, m_clause, cl, true, is_initial });
+        if (m_clause.size() == 2 && is_unit2())
+            s.propagate_bin_clause(m_clause[0], m_clause[1]);
+        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);
+        
         save(m_clause, cl);
     }
 
diff --git a/src/sat/sat_proof_trim.h b/src/sat/sat_proof_trim.h
index 6d996ad6e..6508f5a18 100644
--- a/src/sat/sat_proof_trim.h
+++ b/src/sat/sat_proof_trim.h
@@ -30,9 +30,10 @@ namespace sat {
 
     class proof_trim {
         solver         s;
-        literal_vector m_clause;
+        literal_vector m_clause, m_conflict;        
         uint_set       m_in_clause;
         uint_set       m_in_coi;
+        clause*        m_conflict_clause = nullptr;
         vector<std::tuple<unsigned, literal_vector, clause*, bool, bool>> m_trail;
         
         
@@ -70,10 +71,12 @@ namespace sat {
 
         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;}
         
     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(); }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5c1ed6dae..549783c61 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -90,7 +90,7 @@ namespace sat {
 
     solver::~solver() {
         m_ext = nullptr;
-        SASSERT(m_config.m_num_threads > 1 || check_invariant());
+        SASSERT(m_config.m_num_threads > 1 || m_trim || check_invariant());
         CTRACE("sat", !m_clauses.empty(), tout << "Delete clauses\n";);
         del_clauses(m_clauses);
         CTRACE("sat", !m_learned.empty(), tout << "Delete learned\n";);
@@ -878,6 +878,7 @@ namespace sat {
         m_conflict = c;
         m_not_l    = not_l;
         TRACE("sat", display(display_justification(tout << "conflict " << not_l << " ", c) << "\n"));
+        TRACE("sat", display_watches(tout));
     }
 
     void solver::assign_core(literal l, justification j) {