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

    <tr>
        <th>Summary</th>
        <td>
            [MLIR] Potentially incorrect check in PresburgerSet.cpp subtract
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            mlir:presburger
      </td>
    </tr>

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

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

<pre>
    The check at this line looks unsafe/incorrect:

https://github.com/llvm/llvm-project/blob/b0d1f87b5943b695be44e7ae186a28e263143a6b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp#L313

Note that `b`'s local vars could be reduced post `b.mergeLocalVars` (since duplicates are also eliminated) at https://github.com/llvm/llvm-project/blob/b0d1f87b5943b695be44e7ae186a28e263143a6b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp#L250

As a result, the difference at L313 could just lead to an overflow. An `assert` is needed as well. 

CC: @Superty @Groverkss
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJzMk01v-zYMxj-NfCFmyJJf4oMPWYsMA7qhaIfdaYmO1SqWIUot8u0HZd2aHXf7X0zToCnx9_BBZnfeiCbR_Sy6xwpzWkOc5rDZNZ-zx2oO9jr9sRKYlcw7YIK0OgbvNgIfwjtD3hgXEurkNhNiJJOEPgr5KOTXc01p5_JNnYQ6nV1a81ybcBHq5P3HP-GnPYa38rM6zT7MJUjbLIdh7sZWz_3YzdS2NCA1hx7VgVSvm1ZjX0ov3sXSx5XkuKG_smOhTs-ReM7xTPE_yQt5TC5stdl3ofSTbvT9hX8PiSCtmED0cha9FGpg8MGghw-MDCZkb2EmiGSzIQt74L-L6wvFMz2V0j8xsuglCHVgtxkCm3fvDCZiwEiAngOQdxe3YSIr1Fjo_viwVCfvYR0ZECJx9kmoB0grgXXLQpHKzJig0P0i9pY5gSe0kALgBuGD4uLDZw3HreBDZoqpQHMMG5ElC8jwSd7XcH_ow4PQRxCtfM07xXQtr7_E0u6dubKTtqMesaKp6YdBDlo2slqndpi7vjdLY61F2bVLowfsrZEHpdvFYOUmJZWWSqlG676TNY2jtFYfcDTaDnoRraQLOl8XEeoQz5VjzjT1cmzGyuNMnm9eUupGWR_3O6iqWCxONwHnfGbRSu848Xe35JK_mfG3p19fRPcIzyHRlhx6f4V__fXlRbfBt0qvlIpAwHlOEU2qcvTT_16m2zRlF24D_RUAAP__r0xTYg">