From 79fae355b8f0a8fec58a4723ccea8116a32762bd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 1 Mar 2020 12:17:37 -0800
Subject: [PATCH] fix #3101

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/tactic2solver.cpp | 3 +++
 1 file changed, 3 insertions(+)

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: