Ugh, the code in Figure 13 is mis-compiled by the super-optimizer. It seems that their checking procedure is flawed. How was that not caught in peer-review?

The problem is that the ranges pointed by x and y could (partially) overlap, in which case the SSE-based optimization is incorrect.

Edit: Even more damning, gcc actually does produce an equivalent optimal code sequence for me when the incoming pointers are correctly marked as restrict and -march=native is used. (Although perhaps that's due to different gcc versions; maybe a gcc improvement was inspired by that article.)

Edit #2: I see they actually discuss this in the main article text. Oh well, I'm leaving the comment here since the figure by itself is misleading.

But it seems to me that the fact that they have a theorem prover at all means they do know ahead of time what semantic preserving transformations are available.

No. They have a verificator that can show that two (sub-)programs (more accurately; that an applied transformation preserves semantics) are semantically identical. This is a bit like a P-verificator for the solution to a NP-hard problem using a certificate. It can only help you prove that the solution is right, not find new solutions.