One thing I missed the first time reading the paper is that those were the only bugs they could find in the compiler. After reporting them and getting fixes, se

One thing I missed the first time reading the paper is that those were the only bugs they could find in the compiler. After reporting them and getting fixes, several CPU-years more of random programs haven turned up another failure. All the other compilers pick up tens of failing cases a night, which they skim off and report as their previously reported tests are fixed (the LLVM and GCC teams are quite responsive, others less so). This kind of differential testing also provides some evidence that the formalization isn't too far off - each "passing" case means that almost all the compilers produced exactly the same results for the program. Both projects are awesome, especially if you like reliable compilers.