Verifying optimizations using SMT solvers

I found a nice talk "Verifying optimizations using SMT solvers" from the 2013 LLVM Developers' Meeting where Nuno Lopes talked about similar things as my previous blog post (but more detailed and better).

In the talk he argues for using SMT solvers during compiler development. The obvious example is things like the bug PR17827 where the developers were unsure if a transformation is valid or not, but he also has an example of using it to help when implementing things like the LLVM ConstantRange data-structure. I'm not convinced it will help that often in reality, but I will definitely give it a try next time I have similar problems...