Is it possible to use pi, e and other non-algebraic real numbers in Z3Py?
I wouldn't want to run any C program, but directly from the Z3 Python API
Non-algebraic numbers are usually not supported by SMT solvers. Having said that, you can get pi in z3 indirectly via trigonometric functions, (sin, cos etc.); but the support is incomplete. (Meaning that the solver is most likely to return unknown for most inputs.)
See this answer for a related question: Support of trigonometric functions ( e.g.: cos, tan) in Z3