mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 08:51:55 +00:00
Code Activity

neat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-20 00:27:50 -07:00
parent 6b66cbf547
commit f86702a49b
2 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_context.cpp
View file

@ -4751,6 +4751,11 @@ namespace smt {
} }
mdl = m_model.get(); 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<expr> const& vars, unsigned_vector& depth) { void context::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {

4
src/smt/smt_parallel.cpp
View file

@ -118,10 +118,10 @@ namespace smt {
b.set_unsat(m_l2g, unsat_core); b.set_unsat(m_l2g, unsat_core);
return; return;
} }
// report assumptions used in unsat core, so they can be used in final core
for (expr *e : unsat_core) for (expr *e : unsat_core)
if (asms.contains(e)) if (asms.contains(e))
b.report_assumption_used( b.report_assumption_used(m_l2g, e);
m_l2g, e); // report assumptions used in unsat core, so they can be used in final core
LOG_WORKER(1, " found unsat cube\n"); LOG_WORKER(1, " found unsat cube\n");
b.backtrack(m_l2g, unsat_core, node); b.backtrack(m_l2g, unsat_core, node);