[llvm] [ConstraintElim] Add facts for sdiv with a positive divisor. (PR #225535)

[Florian Hahn via llvm-commits]

================
@@ -1595,17 +1553,20 @@ void State::addInfoFor(BasicBlock &BB) {
     }
 
     // Add facts from unsigned division, remainder and logical shift right, and
-    // from signed remainder.
+    // from signed division and remainder.
     //   urem x, n: result < n  and  result <= x
     //   udiv x, n: result <= x
     //   lshr x, n: result <= x
     //   srem x, n: result >= 0 and result <= x, if x >= 0
     //              result < n,                  if n > 0
+    //   sdiv x, n: result >= 0 and result <= x, if x >= 0 and n > 0
+    //              result > 0 and result < x,   if x > 0 and n > 1
----------------
fhahn wrote:

Ah yes, the alive2 proof (https://alive2.llvm.org/ce/z/KejNK2) did not return the `AND` of both conditions to prove... Should be fixed now, thanks! Fixed alive2 proof https://alive2.llvm.org/ce/z/sL-XyG

https://github.com/llvm/llvm-project/pull/225535