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

    <tr>
        <th>Summary</th>
        <td>
            Static analyzer throws constraints in the subsequent ExplodedNode on a branch. Is it a bug?
        </td>
    </tr>

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

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

    <tr>
      <th>Reporter</th>
      <td>
          jackniu1234
      </td>
    </tr>
</table>

<pre>
    I' m now trying to understand the ExplodedGraph of clang static analyzer using debug.ViewExplodedGraph checker and I hope to select some ExplodedNode to achieve the effect of function summary. However, I found CSA sometimes throws constraints in the subsequent ExplodedNode on a branch, which makes it impossible to just use one ExplodedNode without considering the previous nodes.

Here are two simple examples with similar code. The example 1 throwed constraints while example 2 didn't.

Code of example 1:
```c
#include <stdio.h>

int main() {
    int a;
    scanf("%d", &a);

    if (a > 10) {
 a = a + 1;
    }
    else {
        a = a + 2;
    }
 return a;
}
```
The ExplodedGraph like this:

Here are two simple examples with similar code. The example 1 throwed constraints while example 2 didn't.

Code of example 1:
```c
int rand();
int main() {
    int a = 2;

    if (rand() > 10) {
 a = a + 1;
    }
    else {
        a = a+ 2;
    }
 return 0;
}
```

The ExplodedGraph like this:

I'm wondering if it is a bug. If not, why?
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJzUVUuP5CYQ_jX0pTSWjfvlgw87PeNsX3LZVe4YyoYZDB0e4-38-gg86scmm4kURUosywiK-oqv_FHFvFejQWzJ5pFsnlYsBmld-8L4q1GxovV61Vtxbo-E7mACY2cI7qzMCMFCNAKdD8wICBLh-dtJW4HiJ8dOEuwAXDMzgg8sKA7MMH3-DR1En9wF9nEsflE437txifwVHSTQI0h7whTJo0YewNvpGuZnK7KNcanwDfMRcBjSPjvAEA0PyhrwcZqYOxfw2c74ho7QAxxhsNEIOHz5lDGDmtBDkM7OHrg1PjimTPCgTIb1sff4a0QT7qNbAwx6xwyXCXaWikuY2Ct6UAHUdLLeq17nY75EHyD65PQdh1kFaWPIgZVAl7MrEU4O35SNHowV6AtSPpHy0_L9jA6BOYQwW_BqOmkE_MbS6DNeWlSaOeBWYAFf5cUO1UIUxR3TWaorBlAQShhCd-Eu7CGTHq5QpH63kG25vPx9TmtluI4CgdQHH4SyhST18y2aMgEmpgyhe0IbILvHZR0AINkYqW9WPGdmyFspoRuRhwMQumWENpedNwgDELpnQOpnqMr7AGn1KX3pY-JwE4Xsnq4T1B7vj5WeW2f6A2eHITpzw-BiuiRqmX79w73R6jVpWflrbmm13E5C9zKEU7bQjtBuVEHGvuB2IrS7ubOEdnegD0fvIxLa9dr2hHZL1junRhmKkxlTBv9P6krqcMyIRTmXJH8oqPzn6A_FcoX811TzN0RTfiia_4B0ZmfN-CfSSX1igtma9zqmhlwJfaqTcSzgOICxYSmWZ1J3K9HWoqkbtsK22jb7fVVuduuVbLHZ1rtyxzclX68H7EXVNEJwNvTNdr3nYqVaWtK6qsqqrNdNvS6qWnCanv0Gh3pTk3WJE1O60PptKqwbVypRaXflvqErzXrUPrc9Sg3OoBaeNHVB1yafhz6OnqxLrXzwV5Sggsb2y3dd7R81jwKOuWPkJKWsRKfbv_hf6Szvw8PJ2RfkgdAuM_CEdpnh7wEAAP__pYBgzw">