mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix assertion violations (reported by Christoph Wintersteiger) at sage/bench_1300.smt2 and sage/bench/2861.smt2

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-04 12:24:25 -08:00
parent 825b72719c
commit 88675ec728
1 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/sat/sat_solver.cpp
View file

@ -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);