i implemented a custom concolic execution engine[1] for this crackme, but it didn't work out: at the beginning of it, there is code that checks for an alphabet, smth like:
if x == '(': break
if x in 'a'..'z': break
goto fail
i split the solver state on each branch, which doesn't work out well for me: it means i will do a graph search of like 6**32 branches, which will take very long
state merging is hard
[1]: https://gist.github.com/whitequark/e8c7ffab0208d1b033aae715488881d6