numpy
pysmt
z3-solver
