Why not do this at a higher level on the python source itself?
I ask because z3 has been used for type inference (Typpete) and for solving equations written in Python.
I ask because z3 has been used for type inference (Typpete) and for solving equations written in Python.