diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 448adc479..70ee04ea2 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -173,6 +173,9 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
     try {
         switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) {
         case l_true: 
+            if (m_mc) {
+                (*m_mc)(md);
+            }
             m_result->set_status(l_true);
             break;
         case l_false: