z3/z3_init.py