mirror of
https://github.com/Z3Prover/z3
synced 2026-02-28 10:51:28 +00:00
fix reset code for level marking
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
908dfd392e
commit
19b858dbea
2 changed files with 8 additions and 3 deletions
|
|
@ -1389,7 +1389,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
else if (lvl(lit) < m_conflict_lvl) {
|
||||
slack -= std::abs(coeff);
|
||||
m_lemma.push_back(~lit);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue