mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

fix bug in trim code missing dependecy

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-07 15:39:05 -07:00
parent 2897661bb3
commit 9db227dbf1
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/sat_proof_trim.cpp
View file

@ -191,7 +191,7 @@ namespace sat {
s.propagate(false); s.propagate(false);
} }
if (!s.inconsistent()) if (!s.inconsistent())
IF_VERBOSE(0, s.display(verbose_stream())); IF_VERBOSE(0, s.display(verbose_stream() << "probe on " << cl << "\n"));
for (unsigned i = trail_size0; i < s.m_trail.size(); ++i) for (unsigned i = trail_size0; i < s.m_trail.size(); ++i)
m_propagated[s.m_trail[i].var()] = true; m_propagated[s.m_trail[i].var()] = true;
} }
@ -226,9 +226,11 @@ namespace sat {
if (!s.is_marked(v)) if (!s.is_marked(v))
s.mark(v); s.mark(v);
} }
else if (s.lvl(v) == 0) // literal depends on level 0, it is not assumed by ~C else if (s.lvl(v) == 0) { // literal depends on level 0, it is not assumed by ~C
// inefficient for repeated insertions ? // inefficient for repeated insertions ?
add_core(v); add_core(v);
add_dependency(s.get_justification(v));
}
} }
void proof_trim::add_dependency(justification j) { void proof_trim::add_dependency(justification j) {