If we get an item from a dictionary, we know that the item is non-null if and only if the key is non-null.

This patch is a rather hacky way to record this implication, because some logic needs to be duplicated from the solver.

And yet, it's pretty simple, performant, and works.

Other possible approaches:

- Record the implication, in future rely on Z3 to pick it up.
- Generalize the current code and move it to the constraint manager.

rdar://34990742