diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp
index 0965439ae..5b3cb4da0 100644
--- a/src/cmd_context/extra_cmds/proof_cmds.cpp
+++ b/src/cmd_context/extra_cmds/proof_cmds.cpp
@@ -132,7 +132,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);
diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp
index ee35efe09..01b078d18 100644
--- a/src/sat/sat_proof_trim.cpp
+++ b/src/sat/sat_proof_trim.cpp
@@ -75,20 +75,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
@@ -346,10 +332,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())
@@ -393,7 +375,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..aa75589ac 100644
--- a/src/sat/sat_proof_trim.h
+++ b/src/sat/sat_proof_trim.h
@@ -35,8 +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;
-        
-        
+                
         struct hash {
             unsigned operator()(literal_vector const& v) const {
                 return string_hash((char const*)v.begin(), v.size()*sizeof(literal), 3);
@@ -54,9 +53,6 @@ namespace sat {
 
         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);
 
@@ -76,7 +72,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(); }