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

remove flush_smc after m_solver.get_model #7855

Browse source 
the SAT model converter is applied by m_solver.get_model()
Calling m_sat_mc->flush_smc causes the SAT model converter to be inherited within m_sat_mc and then the model converter gets applied again. This time breaking the model.
flush_smc is reserved for incremental use:
This commit is contained in:
Nikolaj Bjorner 2025-09-07 16:42:11 -07:00
parent d701702735
commit a7eed2a9f3
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1091,10 +1091,9 @@ private:
CTRACE(sat, m_sat_mc, m_sat_mc->display(tout);); CTRACE(sat, m_sat_mc, m_sat_mc->display(tout););
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);
m_map.mk_var_inv(var2expr); m_map.mk_var_inv(var2expr);