Oh wait, Hackernews seems to have removed one of the astericks symbols. It should be Python's exponentiation operator (2 astericks symbols), ya. (edit: fixed now).
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.
... 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.