mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 22:23:22 +00:00
lvl -> _lvl
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0b8dbf2854
commit
3c96b51e97
1 changed files with 1 additions and 1 deletions
|
@ -761,7 +761,7 @@ namespace sat {
|
||||||
|
|
||||||
void solver::assign_core(literal l, unsigned _lvl, justification j) {
|
void solver::assign_core(literal l, unsigned _lvl, justification j) {
|
||||||
SASSERT(value(l) == l_undef);
|
SASSERT(value(l) == l_undef);
|
||||||
TRACE("sat_assign_core", tout << l << " " << j << " level: " << lvl << "\n";);
|
TRACE("sat_assign_core", tout << l << " " << j << " level: " << _lvl << "\n";);
|
||||||
if (_lvl == 0 && m_config.m_drat) {
|
if (_lvl == 0 && m_config.m_drat) {
|
||||||
m_drat.add(l, !j.is_none());
|
m_drat.add(l, !j.is_none());
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue