I’ve been toying with using an llm to compile to smtlib and solving with z3. It works quite well, although I’m not quite sure how practical (large programs, reliably good runtime) I can make it.