mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

patch to fix #5145

Browse source 
underlying issue is that model updates for multi-objective and single objective solving are too brittle to serve its use cases among different plugins.
For maxlex, the last model is always the best and it doesn't use multiple objectives.
This commit is contained in:
Nikolaj Bjorner 2021-04-02 12:23:01 -07:00
parent cebf83c460
commit c0e74f946b
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/opt/opt_solver.cpp
View file

@ -191,6 +191,8 @@ namespace opt {
r = adjust_result(r);
if (r == l_true) {
m_context.get_model(m_last_model);
if (m_models.size() == 1)
m_models.set(0, m_last_model.get());
}
m_first = false;
if (dump_benchmarks()) {