Z3 example in README does not work (wrong version?)

[kmicinski]

I installed Z3, and to confirm that Jeeves was working as expected, I did the following:

>>> from z3 import *
>>> solve(x > 2, y < 10, x + 2*y == 7)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
NameError: name 'x' is not defined

Is it perhaps the case that I need a specific version of Z3? Am I not defining a variable? I find this syntax a bit strange, I'm not sure how a Z3 expression could be passed to the library, since that expression looks like a python AST that Python would try to interpret?