cvc5
python-sat
z3-solver
