mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-27 14:36:35 +00:00
Code Activity

fix #8076

Browse source 
remove unsound "optimization" for correction sets. It misses feasible solutions
This commit is contained in:
Nikolaj Bjorner 2025-12-25 12:44:08 -08:00
parent cb5fb390bc
commit f26facaf8f
1 changed files with 0 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/opt/maxcore.cpp
View file

@ -589,22 +589,6 @@ public:
--m_correction_set_size;
}
trace();
bool no_hidden_soft = (m_st == s_primal_dual || m_st == s_primal || m_st == s_primal_binary);
if (no_hidden_soft && m_c.num_objectives() == 1 && m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) {
exprs cs;
get_current_correction_set(m_csmodel.get(), cs);
m_correction_set_size = cs.size();
TRACE(opt, tout << "cs " << m_correction_set_size << " " << core.size() << "\n";);
if (m_correction_set_size >= core.size())
return;
rational w(0);
for (expr* a : m_asms) {
rational w1 = m_asm2weight[a];
if (w != 0 && w1 != w) return;
w = w1;
}
process_sat(cs);
}
}
bool get_mus_model(model_ref& mdl) {