[wolfspider]

If you have worked with F* or Low* then you probably have some exposure to using Z3 and getting this kind lexical analysis from it is a breakthrough. I just wish Z3 was available on more platforms by default.