Applying an SMT solver to find missed optimisation opportunities in LLVM's arithmetic tooling: https://blog.regehr.org/archives/1714