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

    <tr>
        <th>Summary</th>
        <td>
            [ConstraintElimination] Incomplete signed to unsigned system transfer for facts when handling equality 
        </td>
    </tr>

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

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

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

<pre>
    I know this is known, I'm adding the following primarily as a remainder. Signed facts seem to be handled well in the majority of the cases, however, there are a few cases left to be improved when (non-)equality is involved in facts/solving.
```llvm
define i1 @assume1(i64 %a, i64 %b, i64 %c) {
   %1 = icmp sgt i64 %a, %b
   tail call void @llvm.assume(i1 %1)  ; assume a > b
   %2 = icmp sge i64 %b, %c
   tail call void @llvm.assume(i1 %2)  ; assume b >= c
   %3 = icmp eq i64 %a, %c ; a == c to be folded to false
   ret i1 %3
}

define i1 @assume2(i64 %a, i64 %b, i64 %c)  {
   %1 = icmp sgt i64 %a, %b
   tail call void @llvm.assume(i1 %1)  ; assume a > b
   %2 = icmp eq i64 %b, %c
   tail call void @llvm.assume(i1 %2)  ; assume b == c
   %3 = icmp slt i64 %a, %c            ; a < c to be folded to false
   ret i1 %3
}
```
Godbolt: https://llvm.godbolt.org/z/PdfeKToWo & proofs: https://alive2.llvm.org/ce/z/rG_WMo, https://alive2.llvm.org/ce/z/EEfDcU.
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJzMVcFu4zYQ_RrqMoghjSzLPuiQxPEiKAoUaIs9FpQ4krilOF6StuH9-oKUknh30SJFe1jDhmdEznvDefaj9F4PlqgR1YOo9pk8hZFdI21gq7l3ehgpBM5aVtfmGf60fIEwag_ap8QKfIRngfUEUiltBwgjQc_G8CVmR6cn6bS5gvQgwdEktVXkVvBr5FXQyy548EQTBIaWYJRWGVJwIWNA24Q3yU_sdLgC9ynvpCcfmUe-0JlcDMNIjkDGD_R0mfeAoT4swHo6Oj5H5JEsCNxatncCd_T5JE0Ej6eyZzZxj7ZzZwIPns1Z22El8r3I78Umn9_GnKf5kaJeWwJdgFjn0vvTRIXArd6sQWAlY3NL3N7EncAdiPphxgCIzwoQ5R50Nx3BDwFuEVL1y9YgtYFOGgNn1irSxm5WM3ekLhJaZABRPsC8ABJE-QTtLSPeMtJXfaYe_x0jfsvYRsbI0N2Slm-k9PnbU3ZzfdySChf1ejaKVEx6aTy9wjkKMJOXi0D1fgn-Thx8pzg_lDpvg_pfxdn_kzjefHfKDm5eL0I9_heVXv5Pc_qBVcsmiPIexhCOXpT3Ag8CD-lEw7y6YjcIPHwRePhF9fTTb_yRQeAGjo65998XS6PPhKuEMdd2tAC4D398_JmTl7y35Omp33e_rzLVlGpX7mRGTbHZ1nW-LrHOxqas67zoWqqp6JTabFFWuF7XUtV9TtjuMt1gjmW-wapYryusV_1GbWVXKKyl7FSxE-s8GqV5pc-09ydqNmWVV5mRLRmfHBsx2VB5z8egJ_1FBs3WC0SBjwJx0t6TurtdjGvVPnNNLLxrT4OPPxftg38jCzqYdCM8svXBSW3Dk9GTtjNCtYdn2_F0NBQI_OzjgeFkl9hffYh-7qT1PTno2S0-n6w3OXy8HF6dNzs503w9_0GH8dSuOp4W8Zevu6PjT9QFgYc0k-jQaSx_BQAA___WMQQs">