From 71b5e440588e6223ffad9bdd97ce6872044c8e8e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Apr 2025 10:36:27 -0700 Subject: [PATCH] #7596 - flush smc before copy Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 102f65c2f..c121e5fda 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -137,7 +137,10 @@ public: for (unsigned h : m_fmls_head_lim) result->m_fmls_head_lim.push_back(h); for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f)); if (m_mcs.back()) result->m_mcs.push_back(m_mcs.back()->translate(tr)); - if (m_sat_mc) result->m_sat_mc = dynamic_cast(m_sat_mc->translate(tr)); + if (m_sat_mc) { + m_sat_mc->flush_smc(m_solver, m_map); + result->m_sat_mc = dynamic_cast(m_sat_mc->translate(tr)); + } result->m_has_uninterpreted = m_has_uninterpreted; // copy m_bb_rewriter? result->m_internalized_converted = m_internalized_converted;