Hacker News Reader

You should look at supercompilation.

sometimes also known as superoptimization, which many of them also use SMT solvers like Z3 mentioned in the article

Yes, sorry, superoptimization is the correct term.