google/souper — pull request #133 by rsas (2014-12-08 17:28:19+00:00)
Title: Handle instruction UB on the RHS correctly

This patch teaches Souper to hande UB on the RHS correctly (issue #107). It implements the following query

```LHS UB assertion => (LHS == RHS) && RHS UB assertion ```

```GetCandidateExprForReplacement``` function first builds the LHS and the corresponding UB constraints. Afterwards, the RHS is parsed reusing the same ```ExprBuilder``` context and the RHS UB constraints are collected. The side-effect of reusing the same parsing context results in inclusion of LHS constraints inside of RHS constraints, but these should be easily eliminated by the solver, because they are ``true``.