[schoen]

Oh wait, I left that part out! I'll edit my post.

... there we go.

You use Z3 objects that represent unknowns of particular types, like Z3.Int, Z3.Bool, etc. Each one returns an object representing a variable of that type, which can then be used in (Python-formatted!) expressions that you give to a solver.