From 24090fc48c347af3cadb4a7df57594bd159802c7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 27 Apr 2025 11:44:45 -0700
Subject: [PATCH] move flush smc to first use

---
 src/sat/sat_solver/inc_sat_solver.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 29238be74..adea6eec1 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -1092,6 +1092,7 @@ private:
         sat::model ll_m = m_solver.get_model();
         mdl = alloc(model, m);
         if (m_sat_mc) {
+            m_sat_mc->flush_smc(m_solver, m_map);
             (*m_sat_mc)(ll_m);
         }        
         expr_ref_vector var2expr(m);
@@ -1115,8 +1116,7 @@ private:
         }
 
         TRACE("sat", m_solver.display(tout););
-        if (m_sat_mc)
-            m_sat_mc->flush_smc(m_solver, m_map);
+           
         if (m_sat_mc) {
             (*m_sat_mc)(mdl);
         }