From 1e21ea464511cbd9d955fba00f73ebf2577f5a99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Jun 2019 01:25:50 +0200 Subject: [PATCH] fix cleanup bug exposed by reordering simplifcations Signed-off-by: Nikolaj Bjorner --- src/sat/sat_cleaner.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index 5731c21b6..74ddbdbdb 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -53,6 +53,10 @@ namespace sat { for (; it2 != end2; ++it2) { switch (it2->get_kind()) { case watched::BINARY: + TRACE("cleanup_bug", + tout << ~to_literal(l_idx) << " " << it2->get_literal() << "\n"; + tout << s.value(~to_literal(l_idx)) << " " << s.value(it2->get_literal()) << "\n"; + tout << s.was_eliminated(it2->get_literal()) << " " << s.inconsistent() << "\n";); SASSERT(s.value(it2->get_literal()) == l_true || s.value(it2->get_literal()) == l_undef); if (s.value(it2->get_literal()) == l_undef) { *it_prev = *it2; @@ -212,7 +216,7 @@ namespace sat { cleanup_clauses(s.m_learned); s.propagate(false); } - while (trail_sz < s.m_trail.size()); + while (trail_sz < s.m_trail.size() && !s.inconsistent()); CASSERT("cleaner_bug", s.check_invariant()); return true; }