Some instruction simplifications can be quite tricky and thus easy to get wrong. Often, they also are hard to test (for example, you can test it with a few input values but of course not all combinations). I'm used to validate some of these with an independent tool (Alive cfr. [1], [2]) which is quite neat but has some issues: 1) This tool doesn't work with Sparse's IR or C source but it needs to have the tests written in its own language (very close to LLVM's IR). So it can be used to test if the logic of a simplification but not if implemented correctly. 2) This tool isn't maintained anymore (has some bugs too) and it's successor (Alive2 [3]) is not quite as handy to me (I miss the pre-conditions a lot). So, this patch implement the same idea but fully integrated with Sparse. This mean that you can write a test in C, let Sparse process and simplify it and then directly validate it and not only for a few values but symbolically, for all possible values. Note: Of course, this is not totally stand-alone and depends on an external library for the solver (Boolector, see [4], [5]). Note: Currently, it's just a proof of concept and, except the included tests, it's only very slightly tested (and untested with anything more complex than a few instructions). [1] https://blog.regehr.org/archives/1170 [2] https://www.cs.utah.edu/~regehr/papers/pldi15.pdf [3] https://blog.regehr.org/archives/1722 [4] https://boolector.github.io/ [5] https://boolector.github.io/papers/BrummayerBiere-TACAS09.pdf Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>