flush smc before use in model construction

NikolajBjorner · NikolajBjorner · commit a626cd0fed5d · 2025-04-27T11:18:18.000-07:00
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -1115,6 +1115,8 @@ class inc_sat_solver : public solver {
         }
 
         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);
         }
@@ -1123,6 +1125,7 @@ class inc_sat_solver : public solver {
             TRACE("sat", m_mcs.back()->display(tout););
             (*m_mcs.back())(mdl);
         }
+
         TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););        
 
         if (!gparams::get_ref().get_bool("model_validate", false)) {

Original file line number	Diff line number	Diff line change
`@@ -1115,6 +1115,8 @@ class inc_sat_solver : public solver {`
`1115`	`1115`	`}`
`1116`	`1116`
`1117`	`1117`	`TRACE("sat", m_solver.display(tout););`
	`1118`	`+ if (m_sat_mc)`
	`1119`	`+ m_sat_mc->flush_smc(m_solver, m_map);`
`1118`	`1120`	`if (m_sat_mc) {`
`1119`	`1121`	`(*m_sat_mc)(mdl);`
`1120`	`1122`	`}`
`@@ -1123,6 +1125,7 @@ class inc_sat_solver : public solver {`
`1123`	`1125`	`TRACE("sat", m_mcs.back()->display(tout););`
`1124`	`1126`	`(*m_mcs.back())(mdl);`
`1125`	`1127`	`}`
	`1128`	`+`
`1126`	`1129`	`TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););`
`1127`	`1130`
`1128`	`1131`	`if (!gparams::get_ref().get_bool("model_validate", false)) {`