From a626cd0fed5df854f76815d6ad376b23b064d1f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Apr 2025 11:18:18 -0700 Subject: [PATCH] flush smc before use in model construction --- src/sat/sat_solver/inc_sat_solver.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index c121e5fda..29238be74 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -1115,6 +1115,8 @@ 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); } @@ -1123,6 +1125,7 @@ private: 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)) {