z3-solver
numpy
