From 88675ec728695d7df4e6f6ce8622332c23f1ed8f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Nov 2013 12:24:25 -0800 Subject: [PATCH] fix assertion violations (reported by Christoph Wintersteiger) at sage/bench_1300.smt2 and sage/bench/2861.smt2 Signed-off-by: Leonardo de Moura --- src/sat/sat_solver.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index bb08ae5c3..f4bf5393c 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -596,18 +596,19 @@ namespace sat { clause_offset cls_off = it->get_clause_offset(); clause & c = *(m_cls_allocator.get_clause(cls_off)); TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";); - if (c.was_removed()) { + if (c[0] == not_l) + std::swap(c[0], c[1]); + CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";); + if (c.was_removed() || c[1] != not_l) { // Remark: this method may be invoked when the watch lists are not in a consistent state, - // and may contain dead/removed clauses. - // See: sat_simplifier.cpp - // So, we must check whether the clause was marked for deletion, and ignore it. + // and may contain dead/removed clauses, or clauses with removed literals. + // See: method propagate_unit at sat_simplifier.cpp + // So, we must check whether the clause was marked for deletion, or + // c[1] != not_l *it2 = *it; it2++; break; } - if (c[0] == not_l) - std::swap(c[0], c[1]); - CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";); SASSERT(c[1] == not_l); if (value(c[0]) == l_true) { it2->set_clause(c[0], cls_off);