From f86702a49b9757cae6025dab1305579681e83e9c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Sep 2025 00:27:50 -0700 Subject: [PATCH] neat Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 5 +++++ src/smt/smt_parallel.cpp | 4 ++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index af460d549..01432cabf 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4751,6 +4751,11 @@ namespace smt { } mdl = m_model.get(); } + if (m_fmls && mdl) { + auto convert = m_fmls->model_trail().get_model_converter(); + if (convert) + (*convert)(mdl); + } } void context::get_levels(ptr_vector const& vars, unsigned_vector& depth) { diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index a286c2937..11371b29a 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -118,10 +118,10 @@ namespace smt { b.set_unsat(m_l2g, unsat_core); return; } + // report assumptions used in unsat core, so they can be used in final core for (expr *e : unsat_core) if (asms.contains(e)) - b.report_assumption_used( - m_l2g, e); // report assumptions used in unsat core, so they can be used in final core + b.report_assumption_used(m_l2g, e); LOG_WORKER(1, " found unsat cube\n"); b.backtrack(m_l2g, unsat_core, node);