Comment by kaeluka

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.