diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 6877b328f..6ee96264e 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -182,20 +182,20 @@ namespace intblast {
             translate_expr(e);
     }
 
-    lbool solver::check_axiom(sat::literal_vector const& lits) {
+    lbool solver::check_axiom(char const* name, sat::literal_vector const& lits) {
         sat::literal_vector core;
         for (auto lit : lits)
             core.push_back(~lit);
-        return check_core(core, {});
+        return check_core(name, core, {});
     }
-    lbool solver::check_propagation(sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
+    lbool solver::check_propagation(char const* name, sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
         sat::literal_vector core;
         core.append(lits);
         core.push_back(~lit);
-        return check_core(core, eqs);
+        return check_core(name, core, eqs);
     }
 
-    lbool solver::check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
+    lbool solver::check_core(char const* name, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
         m_core.reset();
         m_vars.reset();
         m_is_plugin = false;
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index 0aceb8b2b..83ff52f11 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -105,9 +105,9 @@ namespace intblast {
         
         ~solver() override {}
 
-        lbool check_axiom(sat::literal_vector const& lits);
-        lbool check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
-        lbool check_propagation(sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
+        lbool check_axiom(char const* name, sat::literal_vector const& lits);
+        lbool check_core(char const* name, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
+        lbool check_propagation(char const* name, sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
 
         lbool check_solver_state();
 
diff --git a/src/sat/smt/polysat_model.cpp b/src/sat/smt/polysat_model.cpp
index 815f6df51..8f68ede0a 100644
--- a/src/sat/smt/polysat_model.cpp
+++ b/src/sat/smt/polysat_model.cpp
@@ -97,24 +97,24 @@ namespace polysat {
         return out;
     }
 
-    void solver::validate_propagate(sat::literal lit, sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
+    void solver::validate_propagate(char const* name, sat::literal lit, sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
         if (!ctx.get_config().m_core_validate)
             return;
-        auto r = m_intblast.check_propagation(lit, core, eqs);
+        auto r = m_intblast.check_propagation(name, lit, core, eqs);
         VERIFY (r != l_true);
     }
 
-    void solver::validate_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
+    void solver::validate_conflict(char const* name, sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
         if (!ctx.get_config().m_core_validate)
             return;
-        auto r = m_intblast.check_core(core, eqs);
+        auto r = m_intblast.check_core(name, core, eqs);
         VERIFY (r != l_true);
     }
 
-    void solver::validate_axiom(sat::literal_vector const& clause) {
+    void solver::validate_axiom(char const* name, sat::literal_vector const& clause) {
         if (!ctx.get_config().m_core_validate)
             return;
-        auto r = m_intblast.check_axiom(clause);
+        auto r = m_intblast.check_axiom(name, clause);
         VERIFY (r != l_true);
     }
 
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 7ae6c99ef..5a20737d0 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -130,7 +130,7 @@ namespace polysat {
         TRACE("bv", tout << "conflict: " << lits << " ";
                     for (auto [a, b] : eqs) tout << ctx.bpp(a) << " == " << ctx.bpp(b) << " "; 
                     tout << "\n"; s().display(tout));
-        validate_conflict(lits, eqs);
+        validate_conflict(hint_info, lits, eqs);
         ctx.set_conflict(ex);
     }
 
@@ -264,7 +264,7 @@ namespace polysat {
             verbose_stream() << "contradictory propagation " << sc << " <- " << deps << "\n";
         }
         auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint);     
-        validate_propagate(lit, core, eqs);
+        validate_propagate(hint_info, lit, core, eqs);
         ctx.propagate(lit, ex);
         return dependency(lit.var()); 
     }
@@ -313,7 +313,7 @@ namespace polysat {
                 if (ctx.use_drat() && hint_info)
                     hint = mk_proof_hint(hint_info, core, eqs);
                 auto ex = euf::th_explain::conflict(*this, core, eqs, hint);
-                validate_conflict(core, eqs);
+                validate_conflict(hint_info, core, eqs);
                 ctx.set_conflict(ex);
             }
         }
@@ -328,7 +328,7 @@ namespace polysat {
                 core.pop_back();
             }
             auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint);
-            validate_propagate(lit, core, eqs);
+            validate_propagate(hint_info, lit, core, eqs);
             ctx.propagate(lit, ex);
         }
         else if (sign) {  
@@ -341,7 +341,7 @@ namespace polysat {
             if (ctx.use_drat() && hint_info)
                 hint = mk_proof_hint(hint_info, core, eqs);
             auto ex = euf::th_explain::conflict(*this, core, eqs, hint);
-            validate_conflict(core, eqs);
+            validate_conflict(hint_info, core, eqs);
             ctx.set_conflict(ex);
         }
     }
@@ -385,7 +385,7 @@ namespace polysat {
             }
         TRACE("bv", display_clause(name, tout, lits));
         IF_VERBOSE(1, display_clause(name, verbose_stream(), lits));
-        validate_axiom(lits);
+        validate_axiom(name, lits);
         s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
         return true;
     }
@@ -393,7 +393,7 @@ namespace polysat {
     void solver::add_axiom(char const* name, sat::literal const* begin, sat::literal const* end, bool is_redundant) {
         ++m_stats.m_num_axioms;
         sat::literal_vector lits;
-        validate_axiom(sat::literal_vector(static_cast<unsigned>(end - begin), begin));
+        validate_axiom(name, sat::literal_vector(static_cast<unsigned>(end - begin), begin));
         for (auto it = begin; it != end; ++it) {
             auto lit = *it;
             if (s().value(lit) == l_true && s().lvl(lit) == 0)
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index 3eba74a82..1bfeb4f18 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -239,9 +239,9 @@ namespace polysat {
         void add_axiom(char const* name, sat::literal const* begin, sat::literal const* end, bool is_redundant);
         void equiv_axiom(char const* name, sat::literal a, sat::literal b);
 
-        void validate_propagate(sat::literal lit, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
-        void validate_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
-        void validate_axiom(sat::literal_vector const& clause);
+        void validate_propagate(char const* name, sat::literal lit, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
+        void validate_conflict(char const* name, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
+        void validate_axiom(char const* name, sat::literal_vector const& clause);
 
         std::ostream& display_clause(char const * name, std::ostream& out, sat::literal_vector const& lits) const;