mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix cleanup bug exposed by reordering simplifcations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-23 01:25:50 +02:00
parent e8080d2307
commit 1e21ea4645
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_cleaner.cpp
View file

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