solver doesn't realize that `z > x && z < y` is unsat with the fact `x == y`

[0x21af]

extern void clang_analyzer_eval();
extern void clang_analyzer_warnIfReached();

int foo(int x, int y, int z)
{
  if (x == y)
  {
    if (z > x)
    {
      clang_analyzer_eval(x == y);
      clang_analyzer_eval(z < y);
      if (z < y)
      {
        clang_analyzer_warnIfReached();
      }
    }
  }
}

report: https://github.com/llvm/llvm-project/issues/62215