3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

add back missing initialization of lo

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-15 06:56:36 -08:00
parent 21f685fa5a
commit c3add4eeda

View file

@ -1251,6 +1251,7 @@ namespace nlsat {
rational lo;
m_am.int_lt(v, vlo);
if (!m_am.is_int(vlo)) continue;
m_am.to_rational(vlo, lo);
// derive tight bounds.
while (true) {
lo++;