From 1d8d85add9e1f9b9478fab3194e82c2f0d77df44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Jul 2020 15:05:06 -0700 Subject: [PATCH] fix #4575 - correction set resolution only works with uniform weights Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index e2bb32b89..3fc5f80e6 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -535,14 +535,19 @@ public: trace(); if (m_c.num_objectives() == 1 && m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) { exprs cs; - TRACE("opt", tout << "cs " << m_correction_set_size << " " << core.size() << "\n";); get_current_correction_set(m_csmodel.get(), cs); m_correction_set_size = cs.size(); - if (m_correction_set_size < core.size()) { - process_sat(cs); + 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) {