Patch proposal for unsoundness issue #13

This is yet another attempt to solve the issue #13. So, far we couldn't find any miscompilations, but more thorough testing using csmith is still ongoing. In the meantime, it would be great to get some feedback. As discussed, this patch now reuses block predicates, tracks Phi path context, and includes surrounding predicates in addition to the selected predicate as well.