In [19]:
from z3 import *
In [22]:
x, y = Reals("x y")
In [21]:
solve(x * x + 3 * x == 3)

[x = -3.7912878474?]
In [23]:
solve(y ** 5 + 2 * y ** 4 + 3 * y ** 3 + y ** 2 + y == 3)

[y = 0.7121129580?]