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

    <tr>
        <th>Summary</th>
        <td>
            clang static analyzer doesn't realize that `(x > 0) && ((x + 1) < 0)` is unsatisfiable with `-analyzer-constraints=z3`
        </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: `--analyze -Xclang -analyzer-stats -Xclang -analyzer-checker=core,debug.ExprInspection -Xanalyzer -analyzer-constraints=z3 --analyzer-output text`

```c
void clang_analyzer_explain();
void clang_analyzer_eval();
void clang_analyzer_warnIfReached();
void clang_analyzer_printState();

int foo(int x)
{
    if (x > 0)
 {
        if ((x + 1) < 0)
        {
 clang_analyzer_warnIfReached();
 clang_analyzer_printState();
            clang_analyzer_explain((x > 0) && ((x + 1) < 0));
            clang_analyzer_eval((x > 0) && ((x + 1) < 0));
        }
    }
}
```

I copied part of the output from the `clang_analyzer_printState()` function.

```console
"program_state": {
  "store": null,
 "environment": { "pointer": "0x5602f04e7b00", "items": [
    { "lctx_id": 1, "location_context": "#0 Call", "calling": "foo", "location": null, "items": [
      { "stmt_id": 719, "kind": "ImplicitCastExpr", "pretty": "clang_analyzer_printState", "value": "&code{clang_analyzer_printState}" }
    ]}
  ]},
 "constraints": [
    { "symbol": "(reg_$0<int x>) > 0", "range": "(bvsgt reg_$0 #x00000000)" },
    { "symbol": "((reg_$0<int x>) + 1) < 0", "range": "(bvslt (bvadd reg_$0 #x00000001) #x00000000)" }
  ], "dynamic_types": null,
  "dynamic_casts": null,
 "checker_messages": null
```

Ummm...I found that GCC Static Analyzer doesn't have such an issue with this case (https://godbolt.org/z/hneve8Yfh).
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJykVt2O6jYQfhpzY4HMJCRwwcVZOFR726rS6RVykkniHseO7AkL-_RV_jbZLUv3qBEK8fib8Td_tqX3qjCIe7Z5YpvjQjZUWrcvpdZ2-YIOdbZIbHbbX9B5ZQ0LvvFUS1Nwco35ycSRiW_SFb6dYJFYLqWR-vaKfPmjx40Ct_Qkyd-RpyWmP9Gx4JhahwwOGSZNsfp-rd2z8TWmpKzhyx-jwlzVGk9OKkOeBcfXgC-nOdtQ3RAnvBKLRM90eEei_6X9-GJV1nt1HrXPeK21VIbBlsGOBU8PkBepvwB7kc4857-jTEvMvoCvnTL0B0nCD-D-rQzx3FoG2_br2gL62XiAcc65yjmD7ZWz4DsXbxD-DjPheig88TWDHWfBYa4zPJPqL7j3Zdf47HmQj5lHnEHEIHpA_4vmxyT-X9ssPk6Ct8H0MZbePJfPPLW1wozX0hG3OacS-VC-ubNVN27L9T_CGAmeN6Zrl9X9erfGW42DFKB2tnCyOvveCHRNPBUHA_DUtWQ3YxqtGRzGIgJAc1HOmgoNTcrtRG2VIXSjEEBcN5GAXIQYJ0K0cji0ckVY-RG2eZpHrjOkU7qeVTYg1oOWtqlsnTyn1nTt_bYOg0Dwg2x5jkukUmtlignTdQ18MPXexYfU3sh5qmgiF693g-ZPZbJpueeq1ipVdJCe2i1tWrt2SHSbkA_SO6pcpG5w7m6U2gxZ_PS5bnxkAB_KcnOcjYfRPLHzbfXz5PhblVg9Z7N1WJwZhIIFh35bCr73DdN11OiFk6Z458U2ufiC-KjNGQRXMTxdn_UOvFF8yOEBjQ8N_JCPJt59yCy7S6w3dJ_oLLL9CtnNyEqlZ7rV6O-20xyVSk_3UW1u-tPyXKH3snhv7fMt5s-qqlar1TPPbWMyTqUk_tvhwNsaUSn_Nh6tmUVvGMTES3lB7pu05NJw5X2D_EVRyalUnqfSYxuekqhuj34GJwanwmaJ1bSyrmBwemVwKg1ecPtXXjLYrRbZPsh2wU4ucL-Otus4gDAMFuV-HaWYJwKTNQTBVmQhbkIR7bYRxDIIcbdQexAQiHAdr9ebUASrfAd5HiaByDdBHmPIQoGVVHql9aVq1190jPcRrOPdQssEte-uOAAGX3p32sBtjgu3b3WWSVN4FgqtPPnJCinSuO8vLL4Plfx3qBxKrV6xj2ob-F87RSLBleeN8ZKUz5VM9BDq9j716VWHRWLROL3_kAJFZZOsUlsxOLVuDH_L2tm_MSUGp855z-DUBeefAAAA__8uidel">