mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

move flush smc to first use

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-27 11:44:45 -07:00
parent a626cd0fed
commit 24090fc48c
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -1092,6 +1092,7 @@ private:
sat::model ll_m = m_solver.get_model(); sat::model ll_m = m_solver.get_model();
mdl = alloc(model, m); mdl = alloc(model, m);
if (m_sat_mc) { if (m_sat_mc) {
m_sat_mc->flush_smc(m_solver, m_map);
(*m_sat_mc)(ll_m); (*m_sat_mc)(ll_m);
} }
expr_ref_vector var2expr(m); expr_ref_vector var2expr(m);
@ -1115,8 +1116,7 @@ private:
} }
TRACE("sat", m_solver.display(tout);); TRACE("sat", m_solver.display(tout););
if (m_sat_mc)
m_sat_mc->flush_smc(m_solver, m_map);
if (m_sat_mc) { if (m_sat_mc) {
(*m_sat_mc)(mdl); (*m_sat_mc)(mdl);
} }