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

    <tr>
        <th>Summary</th>
        <td>
            [ConstraintElimination] Missing fold for `x == y` when `x > y + y` assumed
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            missed-optimization
      </td>
    </tr>

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

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

<pre>
    When assuming `x > y + y`, `x == y` is not folded to `false`:
```llvm
define i1 @assume_x_ugt_y_plus_y(i64 %x, i64 %y) {
  %1 = shl nuw i64 %y, 1
 %2 = icmp ugt i64 %x, %1
  tail call void @llvm.assume(i1 %2)
  %3 = icmp eq i64 %x, %y
  ret i1 %3
}
```
Godbolt: https://llvm.godbolt.org/z/jz1voT1v9 & proof: https://alive2.llvm.org/ce/z/nin4UX.

The constraints system built by ConstraintElimination appears to be satisfiable when evaluating if [`A > B`](https://github.com/llvm/llvm-project/blob/1774c14816f9d4881660b539fd190615e1bdeefd/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp#L588) is implied (negated of `ICMP_ULE`, as `ICMP_EQ` is simplified to it), hence we cannot prove the condition holds. Here's the system:
``` 
-1 * %x + 2 * %y <= -1
%x + -1 * %y <= 0
sat
```
I feel like this may not be solved within ConstraintElimination at the current state, without extending it to verify that the condition is checked against the solution set of the system.
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJyUVcGO2zYQ_Rr6MlhDomTJOviQ2Os2QAK0aIL2ZlDiUJqEIlWR8q726wtSWu82uz0UMGyRnBm9eXxvLJyj1iAe2O4j2502YvKdHQ_CeGvIqpHaDr23m9rK-fBnhwaEc1NPpgVWJI_AsnuYgfGPMLMiYfz4vH1i2SnuATkw1oOyWqIEb0OEEtphSMg-sOTEkg_hOX60vvbLlkRFBoFSYHkS34qXx8vU-st8GfTkLjPjeypyYHz3GN68Ps-MV8DKj0sVCFtpAASu02Cmh1dxR0jXKMZ3PAZR0w8wtR5eVw4lnst5QRoaoTVcLcmALUDeLgADojQWY7x6BSB7qY1__1x6fg4c0cOSnq2slKef6FmWv1hZW-1Z9gE67wcXaORnxs8RSrucbu3YMn5-Yvz8_Sm92q_ptQLGCxhGa9XbXKHpinwbSyypDa75hkz-7a_tiiV-f-0QGmucHwUZ78DNzmMP9UTaQz3D8XZ2r6knIzxZA2IYUIwuqKBGcMKTUyRqjfAQtIVXoSfhg7pIQZBkEe4mu4fwxHYnxvf_Bt2S76Z629h-7X79uRtG-x0bz_i51rZm_JyWZd6k-T4tVCXz_T4tiqTeZZWSaZUU6Q7TWiIq-aoOhbyvozBO2bF3jJ__aIQWI-Pnd9vbNsPAePZ5t98HDZID6gdNKIHxvcFWeJRgVTDAp-OX3y7fPt-vphHutnn_-2oaF5MVLaYhHxTFj9ChaRAeEBphgq-G0V4R_HIdkiLNndXSbeFXHJHx0sXT5YLeGg6W9V3QXfTBY7Qzf17OwLJjUO_daoFbyEvKLWbVpxP-Xd1-AoWoQdOPgJgc9GKOwyGIweorSngg35H5L_n4pdFpHNF4cF54DJyEJDt5wEePRkb5-EDaFUdSM_juOfHGEDloOmx-oATRCjJuCXBWT_HcoQ839ULcdiMPmayySmzwkBb7skhSzstNd1BlyUWJqi5lnmdYVGUhi6zeFWnCeSXEhg484VlS8DxNkjIpt0kuRSN4piqlRKNSlifYC9I3723IuQkPRZZXyUaLGrWLA5rznpxDeWcHTz09RVYY52Fyj4eo-3pqXZhJ5Lx7qefJ6zjj3-WV7U7whZwLxIUxDcqOb-d4dOg7Q3_5R0C5mUZ9-N_ujJ0Ga8Vm_wkAAP__dHIABg">