I think the remarkable point in the above optimisation was that the non-pure functions define() and require() were also subject of optimisation even though the optimizer had no special knowledge about them. Using symbolic execution, the optimizer nevertheless was able to reason about them.