Algebraic numbers, index problem

[makkiato83]

Hello, I am experimenting with z3 in Python.

I am not sure, but it looks like the index() method of the AlgebraicNumRef class is not working properly:

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

The polynomial defining the solutions is correct: polynomial $1x^2 + 0x -2 = 0$

But the two roots are both getting index 0.

[NikolajBjorner]

You are the only user of this feature. I am afraid you would have to fix this on your own.

[janvrany]

Fix in PR #5888 should fix the problem.