From a51d65d58a2d0987efe24170d0d9f23ebba8ce4f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 Mar 2020 21:20:27 +0100
Subject: [PATCH] fix #3118 (without breaking #3101, #3111)

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

diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index a575e909d..637db3871 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -194,7 +194,9 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
               if (g->mc()) g->mc()->display(tout << "g:");
               if (md) tout << *md.get() << "\n";
               );
-
+        if (m_mc && md) {
+            (*m_mc)(md);
+        }
         m_mc = concat(g->mc(), m_mc.get());
 
     }