It's worth noting these notes are 11 years old. The first give-away was the comment that in Python 3/2 is an integer, which is indeed true in Python 2 but not in Py3.

For modern users of Z3, you'd want to do `pip install z3-solver` rather than use `Z3Py` mentioned at the very bottom of this doc.

That’s a very clean API.

https://www.hakank.org/z3/

Very good to see all this in one short page!