From 8822bc17550bdb60feec8f55bcf8da5921752cdc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Aug 2014 16:03:25 -0700 Subject: [PATCH] fix bug in unsat core finding Signed-off-by: Nikolaj Bjorner --- src/sat/sat_mus.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index e6c9376ea..e582a9f5c 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -50,14 +50,16 @@ namespace sat { literal_vector& mus = m_mus; core.append(s.get_core()); for (unsigned i = 0; i < core.size(); ++i) { - s.m_user_scope_literals.contains(core[i]); - mus.push_back(core[i]); - core[i] = core.back(); - core.pop_back(); - --i; + if (s.m_user_scope_literals.contains(core[i])) { + mus.push_back(core[i]); + core[i] = core.back(); + core.pop_back(); + --i; + } } while (!core.empty()) { + IF_VERBOSE(2, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); TRACE("sat", tout << "core: " << core << "\n"; tout << "mus: " << mus << "\n";);