[stevesimmons]

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.