From df981666fd4c99e744be145ba4df35c9908ed896 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Apr 2022 16:27:46 +0200 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/opt/maxcore.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp index 4369b10faef..c71a7944ede 100644 --- a/src/opt/maxcore.cpp +++ b/src/opt/maxcore.cpp @@ -882,9 +882,11 @@ class maxcore : public maxsmt_solver_base { ncore.push_back(mk_not(m, f)); m_unfold_upper -= b.weight; } - m_unfold_upper += rational(core.size() - 1) * weight; - expr* am = mk_atmost(ncore, 1, weight); - new_assumption(am, weight); + if (core.size() > 1) { + m_unfold_upper += rational(core.size() - 2) * weight; + expr* am = mk_atmost(ncore, 1, weight); + new_assumption(am, weight); + } }