I see that, but since you still need to record the explicit choice for each BinaryOperator in the state, why do you need the leaves? (Sorry, I didn't remember that some leaves could be Unknown, which makes everything fall apart.) http://llvm-reviews.chandlerc.com/D1340