diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp
index 31d708733..ea585bfae 100644
--- a/src/cmd_context/extra_cmds/proof_cmds.cpp
+++ b/src/cmd_context/extra_cmds/proof_cmds.cpp
@@ -350,9 +350,9 @@ public:
 
     void updt_params(params_ref const& p) override {
         solver_params sp(p);
-        m_check = sp.proof_check();
         m_save  = sp.proof_save();        
         m_trim  = sp.proof_trim();
+        m_check = sp.proof_check() && !m_trim && !m_save && !m_on_clause_eh;
         if (m_trim)
             trim().updt_params(p);
     }
@@ -360,6 +360,8 @@ public:
     void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause_eh) override {
         m_on_clause_ctx = ctx;
         m_on_clause_eh = on_clause_eh;
+        if (m_on_clause_eh)
+            m_check = false;
     }
 
 };
diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp
index d346fb015..51fc44cd7 100644
--- a/src/sat/sat_proof_trim.cpp
+++ b/src/sat/sat_proof_trim.cpp
@@ -383,14 +383,18 @@ namespace sat {
             return false;
         };
 
-        if (all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; }))
+        if (all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; })) {
+            IF_VERBOSE(3, verbose_stream() << "conflict " << m_clause << "\n");
+            set_conflict(m_clause, cl);
             return;
+        }
+
         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);
-        if (s.inconsistent() || all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; })) {
+        if (s.inconsistent()) {
             IF_VERBOSE(3, verbose_stream() << "conflict " << m_clause << "\n");
             set_conflict(m_clause, cl);
         }
diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index 9fafbcc80..bdcddc03d 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -192,6 +192,9 @@ namespace arith {
         case hint_type::farkas_h:
             name = "farkas";
             break;
+        case hint_type::cut_h:
+            name = "cut";
+            break;
         case hint_type::bound_h:
             name = "bound";
             break;
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 2803e6c06..89bccf76b 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1147,7 +1147,7 @@ namespace arith {
             app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
             IF_VERBOSE(4, verbose_stream() << "cut " << b << "\n");
             literal lit = expr2literal(b);
-            assign(lit, m_core, m_eqs, explain(hint_type::bound_h, lit));
+            assign(lit, m_core, m_eqs, explain(hint_type::cut_h, lit));
             lia_check = l_false;
             break;
         }
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 2364bb16e..8922673c0 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -51,6 +51,7 @@ namespace arith {
     enum class hint_type {
         farkas_h,
         bound_h,
+        cut_h,
         implied_eq_h
     };
 
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index 39c9879a6..55b5eff72 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -255,6 +255,7 @@ namespace euf {
     smt_proof_hint* solver::mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, expr_pair const* eqs, unsigned nd, expr_pair const* deqs) {
         if (!use_drat())
             return nullptr;
+        TRACE("euf", tout << "SMT hint " << n << "\n");
         push(value_trail(m_lit_tail));
         push(restore_vector(m_proof_literals));