diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 75b6b0588..05b93d38b 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -1031,14 +1031,14 @@ extern "C" {
         Z3_TRY;
         RESET_ERROR_CODE();
         init_solver(c, s);     
-        user_propagator::on_clause_eh_t _on_clause = [=](void* user_ctx, expr* proof, unsigned nd, unsigned const* deps, unsigned n, expr* const* _literals, unsigned const status) {
+        user_propagator::on_clause_eh_t _on_clause = [=](void* user_ctx, expr* proof, unsigned nd, unsigned const* deps, unsigned n, expr* const* _literals) {
             Z3_ast_vector_ref * literals = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
             mk_c(c)->save_object(literals);
             expr_ref pr(proof, mk_c(c)->m());
             scoped_ast_vector _sc(literals);
             for (unsigned i = 0; i < n; ++i)
                 literals->m_ast_vector.push_back(_literals[i]);
-            on_clause_eh(user_ctx, of_expr(pr.get()), nd, deps, of_ast_vector(literals), status);
+            on_clause_eh(user_ctx, of_expr(pr.get()), nd, deps, of_ast_vector(literals));
         };
         to_solver_ref(s)->register_on_clause(user_context, _on_clause);
         auto& solver = *to_solver(s);
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 3264226f3..baa2fa34c 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1441,7 +1441,7 @@ Z3_DECLARE_CLOSURE(Z3_final_eh,   void, (void* ctx, Z3_solver_callback cb));
 Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t));
 Z3_DECLARE_CLOSURE(Z3_decide_eh,  void, (void* ctx, Z3_solver_callback cb, Z3_ast t, unsigned idx, bool phase));
 Z3_DECLARE_CLOSURE(Z3_on_binding_eh, bool, (void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst));
-Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals, unsigned const status));
+Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals));
 
 
 /**
diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp
index 22348fd2b..ea585bfae 100644
--- a/src/cmd_context/extra_cmds/proof_cmds.cpp
+++ b/src/cmd_context/extra_cmds/proof_cmds.cpp
@@ -314,7 +314,7 @@ public:
         if (m_trim)
             trim().assume(m_lits);
         if (m_on_clause_eh)
-            m_on_clause_eh(m_on_clause_ctx, assumption(), m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data(), 0u);
+            m_on_clause_eh(m_on_clause_ctx, assumption(), m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data());
         m_lits.reset();
         m_proof_hint.reset();
         m_deps.reset();
@@ -328,7 +328,7 @@ public:
         if (m_trim)
             trim().infer(m_lits, m_proof_hint);
         if (m_on_clause_eh)
-            m_on_clause_eh(m_on_clause_ctx, m_proof_hint, m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data(), 0u);
+            m_on_clause_eh(m_on_clause_ctx, m_proof_hint, m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data());
         m_lits.reset();
         m_proof_hint.reset();
         m_deps.reset();
@@ -342,7 +342,7 @@ public:
         if (m_trim)
             trim().del(m_lits);
         if (m_on_clause_eh)
-            m_on_clause_eh(m_on_clause_ctx, del(), m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data(), 0u);
+            m_on_clause_eh(m_on_clause_ctx, del(), m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data());
         m_lits.reset();
         m_proof_hint.reset();
         m_deps.reset();
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index b28f5e9a2..6f240a88d 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -382,7 +382,7 @@ namespace euf {
         for (unsigned i = 0; i < n; ++i) 
             m_clause.push_back(literal2expr(lits[i]));
         auto hint = status2proof_hint(st);
-        m_on_clause(m_on_clause_ctx, hint, 0, nullptr, m_clause.size(), m_clause.data(), 0u);
+        m_on_clause(m_on_clause_ctx, hint, 0, nullptr, m_clause.size(), m_clause.data());
     }
 
     void solver::on_proof(unsigned n, literal const* lits, sat::status st) {
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index b537a44dc..0b5a4930c 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -194,16 +194,7 @@ namespace smt {
             m_trail.push_back(info(st, v, p));
         if (m_on_clause_eh) {
             // Encode status as an integer flag for simplicity.
-            unsigned st_code = 0;
-            switch (st) {
-                case status::assumption:    st_code = 1; break;
-                case status::lemma:         st_code = 2; break;
-                case status::th_lemma:      st_code = 3; break;
-                case status::th_assumption: st_code = 4; break;
-                case status::deleted:       st_code = 5; break;
-                default:                    st_code = 0; break;
-            }
-            m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data(), st_code);
+            m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());
         }
         
         if (m_has_log) {
diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h
index ffe87d27c..1b480fb04 100644
--- a/src/tactic/user_propagator_base.h
+++ b/src/tactic/user_propagator_base.h
@@ -27,7 +27,7 @@ namespace user_propagator {
     typedef std::function<void(void*, callback*, unsigned)>                  pop_eh_t;
     typedef std::function<void(void*, callback*, expr*)>                     created_eh_t;
     typedef std::function<void(void*, callback*, expr*, unsigned, bool)>     decide_eh_t;
-    typedef std::function<void(void*, expr*, unsigned, unsigned const*, unsigned, expr* const*, unsigned const)>        on_clause_eh_t;
+    typedef std::function<void(void*, expr*, unsigned, unsigned const*, unsigned, expr* const*)>        on_clause_eh_t;
     typedef std::function<bool(void*, callback*, expr*, expr*)>              binding_eh_t;
 
     class plugin : public decl_plugin {