Fix proposal for unsoundness issue #13 + test case

This patch addresses the unsoundness issue #13. The idea is to first collect the UB constraints and then add them together with the Phi node predicates. If no Phi nodes exist, add the UB constraints directly as instruction conditions. The recursive parsing at each Phi node can be improved, but we should discuss the proposed solution first.
It isn't clear what that would achieve. What would your condition be? You can't stop after one phi because there may be any number of phis between the top level and the UB. I think you need to figure out a way to maintain the context from the outer phis when building predicates.