Well worth reading. This was one of the major sources that helped me learn SMT, and I now have some projects in the area (yet another superoptimizer).

Z3 has been very good as an 'external brain' for all sorts of problems.