This is a very rough proof of concept.

As discussed in https://github.com/llvm/llvm-project/issues/53020 / https://reviews.llvm.org/D116692,

SCEV is forbidden from reasoning about 'backedge taken count'

if the branch condition is a poison-safe logical operation,

which is conservatively correct, but is severely limiting.

Instead, we should have a way to express those

poison blocking properties in SCEV expressions.

The proposed semantics is:

Sequential/in-order min/max SCEV expressions are non-commutative variants of commutative min/max SCEV expressions. If none of their operands are poison, then they are functionally equivalent, otherwise, if the operand that represents the saturation point* of given expression, comes before the first poison operand, then the whole expression is not poison, but is said saturation point.

- saturation point - the maximal/minimal possible integer value for the given type

The lowering is straight-forward:

compare each operand to the saturation point, perform sequential in-order logical-or (poison-safe!) ordered reduction over those checks, and if reduction returned true then return saturation point else return the naive min/max reduction over the operands

https://alive2.llvm.org/ce/z/Q7jxvH (2 ops)

https://alive2.llvm.org/ce/z/QCRrhk (3 ops)

Note that we don't need to check the last operand: https://alive2.llvm.org/ce/z/abvHQS

Note that this is not commutative: https://alive2.llvm.org/ce/z/FK9e97

That allows us to handle the patterns in question.