Algebraic numbers in Z3

The following code sets some Z3 constraints for x,y that are satisfied (only) by: x = sqrt(2) and y = -sqrt(2).

x, y = Reals('x y')
s = Solver()
s.add( x*x == 2 )
s.add( x>0)
s.add( y*y == 2 )
s.add( y<0)
s.check()
m = s.model()
val_x = m.get_interp(x)
val_y = m.get_interp(y)

print(f"The solutions are: x={val_x} and y={val_y}")
print(f"The defining polynomial of x has integer coefficients", val_x.poly(), " and root index ", val_x.index())
print(f"The defining polynomial of y has integer coefficients", val_y.poly(), " and root index ", val_y.index())

The output is:

The solutions are: x=1.4142135623? and y=-1.4142135623?

the defining polynomial of x has integer coefficients [-2, 0, 1]  and root index  0

the defining polynomial of y has integer coefficients [-2, 0, 1]  and root index  0

It thus appear that the .index() function, which is supposed to extract the index of an algebraic number, does not work: Both $sqrt(2)$ and $- sqrt(2)$ are given the same index.

I have reported this issue in the Z3 github (link) but unfortunately the devs do not have the bandwidth to solve this issue.

I had a look at the python code for the .index() function (path z3/lib.z3.py):

def index(self):
    return Z3_algebraic_get_i(self.ctx_ref(), self.as_ast())

which just calls:

def Z3_algebraic_get_i(a0, a1, _elems=Elementaries(_lib.Z3_algebraic_get_i)):
  r = _elems.f(a0, a1)
  _elems.Check(a0)
  return r

which basically (?) calls the method Z3_algebraic_get_i of the Z3 library in the C language.

I am not familiar myself with C, so I am seeking some help:

QUESTION is the Z3_algebraic_get_i function of the C Z3 library actually working, or it's just Python?

Thanks

EDIT: This is the source code of the C function from here

    unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a) {
        Z3_TRY;
        LOG_Z3_algebraic_get_i(c, a);
        RESET_ERROR_CODE();
        CHECK_IS_ALGEBRAIC(a, 0);
        algebraic_numbers::manager & _am = am(c);
        algebraic_numbers::anum const & av = get_irrational(c, a);
        return _am.get_i(av);
        Z3_CATCH_RETURN(0);
    }

Solution

This was fixed in https://github.com/Z3Prover/z3/pull/5888, so make sure to update z3 if you still see this issue. I'm not sure what the first version of z3 to have the fix was, but I just upgraded to 4.11.2.0, and it's working now.

Also worth noting: roots are 1-indexed in z3.