[PATCH] D103314: [Analyzer][solver] Simplify existing constraints when a new constraint is added

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

I had another thought, `merge` is usually called in situations when we found out that two symbols should be marked equal (and checked that it's possible to begin with), which is not true in your case.

If we update my case from before, we can get: `a + b == c` and `a != c` as given, and `b == 0` as a new constraint. In this situation, you will merge classes `{a + b, c}` and `{a}`, which contradicts our existing equality information.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103314/new/

https://reviews.llvm.org/D103314