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

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

    <tr>
      <th>Labels</th>
      <td>
            llvm:instcombine,
            missed-optimization
      </td>
    </tr>

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

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

<pre>
    `x == y` is correctly folded to `false` when `x > y` is assumed, or when `x >= y + 1` is assumed, but not when `x > y + 1` is assumed:

[godbolt](https://godbolt.org/z/s583h36oh)
```llvm
; folded to false
define i1 @assume_x_ugt_y(i64  %x, i64  %y)  {
  %1 = icmp ugt i64 %x, %y
  tail call void @llvm.assume(i1 %1)
  %2 = icmp eq i64 %x, %y
  ret i1 %2
}

; folded to false
define i1 @assume_x_uge_y_plus_1(i64  %x, i64  %y)  {
  %1 = add nuw i64 %y, 1
 %2 = icmp uge i64 %x, %1
  tail call void @llvm.assume(i1 %2)
  %3 = icmp eq i64 %x, %y
  ret i1 %3
}

; not folded to false
define i1 @assume_x_ugt_y_plus_1(i64  %x, i64  %y)  {
  %1 = add 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
}

declare void @llvm.assume(i1) 
```

[alive proof](https://alive2.llvm.org/ce/z/YRcN-b)
```llvm
define i1 @src(i64 %x, i64 %y)  {
  %1 = add 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
}
=>
define i1 @tgt(i64 %x, i64 %y)  {
  ret i1 false
}

declare void @llvm.assume(i1) 
```
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJzEVU2P2jAQ_TWTiwWKxyTAIYdls0hV1R566wk5sRPcOjGNnd1lf31lJ-wusFSlnxICEb954_dmJsOtVXUrZQbJCpI84r3bmi5730j-VbVRYcQ-gzR-JMByYDnZQxoTZUlpuk6WTu9JZbSQgjhDII0rrq30kIetbMkYePccxa3tGykAb4npjjGBnACuCD0HF70jrXGnrG_C2Q3EOcSH72RVG1EY7SDJARdb53bWY3ANuB6PpqarAddPgGubLNiWpWYLuBwZ0nj4aH3fjI_Y6pXsQXM4ELJSrSSKEpjFw4U2j5u-dps94EKlM0IAk0cv6fBnD7gkBOargSE8o95tospmR_raBeghLESMSMeVJiXXmtwbJXxKf8XpkNfno4HsWUngxhdu-e0idScdGcJxlDzPj2y91gG52W92urcber0RXAjS9g-Hy-59FB1Rx4r6Wp5Kote5hcdusSvdYhfd8u17bc_8FcfOLDtrsF-37I85JmSpeScv5vXKT8bzZOq5VveS7DpjqrcmPxzjNPAO01_K8RXw-VP5cVL8aP6PSma7cizQ6_r8g_L8n4b2a-DuDRtc7X7ShpH81Qj8fvEjkTGxZEseyYym88U8pRgn0TZLeSlkyRnnVbqoCs4LOhMsFZQWgsvlIlIZxshiRmcxMobJlFdxUfCKyrRgrMQEZrFsuNLPvRIpa3uZpZQtWaR5IbUN2xMxdAi7Ua11pWkK1UpABLwFxEZZK8XE7Jxq1BN3yrT-LMmjLvNhk6KvrdeqrLMvqZxyOuzmd611tyNnkpMPylrV1uGNQirTkbMdfXFVjnsy6judnWxD5bZ9MS1NA7gOWoafya4zX2TpANdBugVcB_XfAwAA__-slETN">