pysmt
sbol3
z3-solver
