TLDR: parse regex and convert to Z3 constraints. Solve.

https://meashiri.github.io/ctf-writeups/posts/202308-litctf/#iloveregex

Original writeup (https://meashiri.github.io/ctf-writeups/posts/202308-litctf/#iloveregex).