mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f2e636c598
commit
0b7021d2c8
|
@ -1636,7 +1636,10 @@ namespace opt {
|
|||
}
|
||||
// TBD: check that optimal was not changed.
|
||||
}
|
||||
TRACE("opt", tout << "value " << value << "\n";);
|
||||
maxsmt& ms = *m_maxsmts.find(obj.m_id);
|
||||
rational value0 = ms.get_lower();
|
||||
TRACE("opt", tout << "value " << value << " other " << value0 << "\n";);
|
||||
SASSERT(value0 == value);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue