I am planning to do some work with SMT solvers and GCC. I usually start new projects by doing a naive implementation of the critical part to get a feel for the problems and find out what I need to learn before the real implementation. So I started this project by building a simple translation validator, similar to the LLVM Alive2 (but with many limitations).| Krister Walfridsson’s blog