mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix bug in unsat core finding

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-20 16:03:25 -07:00
parent 78c03ed835
commit 8822bc1755
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/sat/sat_mus.cpp
View file

@ -50,14 +50,16 @@ namespace sat {
literal_vector& mus = m_mus; literal_vector& mus = m_mus;
core.append(s.get_core()); core.append(s.get_core());
for (unsigned i = 0; i < core.size(); ++i) { for (unsigned i = 0; i < core.size(); ++i) {
s.m_user_scope_literals.contains(core[i]); if (s.m_user_scope_literals.contains(core[i])) {
mus.push_back(core[i]); mus.push_back(core[i]);
core[i] = core.back(); core[i] = core.back();
core.pop_back(); core.pop_back();
--i; --i;
}
} }
while (!core.empty()) { while (!core.empty()) {
IF_VERBOSE(2, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
TRACE("sat", TRACE("sat",
tout << "core: " << core << "\n"; tout << "core: " << core << "\n";
tout << "mus: " << mus << "\n";); tout << "mus: " << mus << "\n";);