From a7eed2a9f381c79d10d9602121132fbe538562bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Sep 2025 16:42:11 -0700 Subject: [PATCH] remove flush_smc after m_solver.get_model #7855 the SAT model converter is applied by m_solver.get_model() Calling m_sat_mc->flush_smc causes the SAT model converter to be inherited within m_sat_mc and then the model converter gets applied again. This time breaking the model. flush_smc is reserved for incremental use: --- src/sat/sat_solver/inc_sat_solver.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index f74e0fca1..4d92dcb81 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -1091,10 +1091,9 @@ private: CTRACE(sat, m_sat_mc, m_sat_mc->display(tout);); 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); + if (m_sat_mc) (*m_sat_mc)(ll_m); - } + expr_ref_vector var2expr(m); m_map.mk_var_inv(var2expr);