z3-solver
mpi4py
