3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

Care for root index being undefine while calling Z3_algebraic_get_i() (#5888)

In some cases, Z3_algebraic_get_i() returned 0. For example, in the following
Python snippet, the last assert would fail:

    import z3
    x = z3.Real('x')
    s = z3.Solver()
    s.add( (x * x) - 2 == 0, x <= 0)
    s.check()
    val_x = s.model().get_interp(x)
    assert val_x.index() == 1

The problem was that `algebraic_numbers::manager:👿:get_i()` did not
check whether the root index was properly initialized.

This commit fixes this issue by checking whether root index is initialized
the same way various other routines do.

Fixes issue #5807.

Signed-off-by: Jan Vrany <jan.vrany@labware.com>
This commit is contained in:
Jan Vraný 2022-03-17 02:28:03 +00:00 committed by GitHub
parent 6455ae4350
commit bdf7de1703
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -2013,6 +2013,11 @@ namespace algebraic_numbers {
}
else {
algebraic_cell * c = a.to_algebraic();
if (c->m_i == 0) {
// undefined
c->m_i = upm().get_root_id(c->m_p_sz, c->m_p, lower(c)) + 1;
}
SASSERT(c->m_i > 0);
return c->m_i;
}
}