na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 18, 2022 · df98166 · df98166
1 parent 98c7069
commit df98166
Showing 1 changed file with 5 additions and 3 deletions.
diff --git 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);
+        }
     }