Sorry, my original post was confusing. I did not meant to imply that I based my work on the Massalin paper, just that I liked it. As I said, my work is SMT-base

Sorry, my original post was confusing. I did not meant to imply that I based my work on the Massalin paper, just that I liked it. As I said, my work is SMT-based and more closely related to Regehr's 'souper' or the one described in Gulwani's "Synthesis of Loop Free Programs" in PLDI '11 (I think). While STOKE is interesting, I have trouble understanding why they even call it a "superoptimizer". The point of appending "super-" to optimizer was to get away from the (strictly speaking incorrect) practice of referring to compiler improvements as "optimizations" (when they don't achieve optimal outcomes). STOKE is "stochastic", so it cannot realistically claim to always find optimal sequences. So it's just another "improver", or if you will, an "optimizer".