From 64daa2977d1a961d387a3ab058850d16ae0c7ccd Mon Sep 17 00:00:00 2001
From: Anh-Dung Phan <t-anphan@microsoft.com>
Date: Tue, 12 Nov 2013 16:14:21 -0800
Subject: [PATCH] Fix termination conditions on core_maxsat

---
 src/opt/core_maxsat.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp
index 0ea239854..e131526cf 100644
--- a/src/opt/core_maxsat.cpp
+++ b/src/opt/core_maxsat.cpp
@@ -69,6 +69,10 @@ namespace opt {
                     m_answer.reset();
                     m_answer.append(ans);
                 }
+                if (m_answer.size() == m_upper) {
+                    return l_true;
+                }
+                SASSERT(m_soft.size() >= m_answer.size()+1);
                 unsigned k = m_soft.size()-m_answer.size()-1;
                 expr_ref fml = mk_at_most(core_vars, k);
                 TRACE("opt", tout << "add: " << fml << "\n";);