openai
optillm
z3-solver