[Python] Unexpected Behaviour in Z3 when working with exponentials

I have the following code in which I am trying to return the value of e^x using z3. However, this code is returning y = 0

import z3

x, y = z3.Real('x'), z3.Real('y')
e = z3.RealVal(str(gmpy2.exp(gmpy2.mpfr(1)))) # or e^1, the Euler's number e
print(e)
s = z3.Solver()
s.add(x == 1134585759063987950064875850350910837993/1361129467683753853853498429727072845824)
s.add(y == e ** x)
s.check()
model = s.model()
print(model)


The output of this code is:

3397852285573806544200359339189/1250000000000000000000000000000
[x = 260488115293581/312500000000000, y = 0]


How can I fix this code?

Continue reading...