The monotonicity definition states its domain as follows:
```
/// The property of monotonicity of a SCEV. To define the monotonicity, assume
/// a SCEV defined within N-nested loops. Let i_k denote the iteration number
/// of the k-th loop. Then we can regard the SCEV as an N-ary function:
///
/// F(i_1, i_2, ..., i_N)
///
/// The domain of i_k is the closed range [0, BTC_k], where BTC_k is the
/// backedge-taken count of the k-th loop
```
Current monotonicity check implementation doesn't match this definition
because:
- Just checking nowrap property of addrecs recursively is not sufficient
to ensure monotonicity over the entire domain. The nowrap property may
hold for certain paths but not for all possible iteration combinations
of nested loops.
- It doesn't consider cases where exact backedge-taken counts are
unknown.
Therefore we need to fix either the definition or the implementation.
This patch adds the test cases that demonstrate this mismatch.