<table border="1" cellspacing="0" cellpadding="8">
    <tr>
        <th>Issue</th>
        <td>
            <a href=https://github.com/llvm/llvm-project/issues/62215>62215</a>
        </td>
    </tr>

    <tr>
        <th>Summary</th>
        <td>
            clang static analyzer doesn't realize that `z > x && z < y` is unsatisfiable with the fact `x == y`
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            new issue
      </td>
    </tr>

    <tr>
      <th>Assignees</th>
      <td>
      </td>
    </tr>

    <tr>
      <th>Reporter</th>
      <td>
          hallo-wereld
      </td>
    </tr>
</table>

<pre>
    version: Clang trunk
args:
```shell
--analyze -Xclang -analyzer-stats -Xclang -analyzer-checker=core,debug.ExprInspection -Xanalyzer -analyzer-constraints=z3 --analyzer-output text
```
Clang Static Analyzer doesn't realize that `z > x && z < y` is unsatisfiable with the fact `x == y`. I find that the analysis results of the `clang_analyzer_warnIfReached()` are the same whether or not with Z3.

See it live: https://godbolt.org/z/Te3d9GPM6

</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJy8UsFu2zAM_Rr6QjiwpURxDj5kTT30MGBYdyh2KWSbtrUqUiDRTZqvH2w36FDsPMCwwCc94j0-6hhN74hK2HyBzSHRIw8-lIO21qdnCmTbpPbtW_lKIRrvQO7xzmrXI4fRvUB2gGyvQx9B7pcCVLZ8cSBrFyxNtdP27UqYPjUz-waENLLm-A-8Gah5oQDy0PhAIO5aqsd-dX85hQcXT9Sw8Q7Tpxvhb6p3kYM2jiPIw1Vi-nHnRz6NjEwX_qR3KRdzj6zZNLi_9W49RQdiyxhIW3Ml5EEzgsquCPIeLwhCgVA4lXf4BipDE3F0UbOJndG1JTwbHpAHwk43M_eCIA8gD_P7FT5gZ1y7dJ6ezZqjiRgojpYj-m7GQWXzsJ5vpp7POriH7gfpZqAWRAFiNynQgWZC1EfC80A8UEAf0HlexPySq_chzP9HIjSM1rzSlPPAfJpzFRWIqvdt7S2vfOhBVFcQ1U-S7e7r929qYSdtKdud3OmEylwVeSHznVLJUBbbLm-2dZ7Trq1JNrLtNqLIM1UItdnWMjGlyITM1nmRb6RYq9VatMW6aIqu7mTerTNYZ3TUxq6sfT1OChIT40ilEiLfJFbXZOO8wUI4OuN8CUJMCx3KiZPWYx9hnVkTOX50YcOWymXz4hK5_o-RJ2Ow5acpGx7GetX4I4hq0vl-pKfgf1PDIKrZXQRRze7_BAAA___fETLt">