z3-solver
matplotlib
