division-comparison: incorrect rewrite for negative dividend

[intrigus-lgtm]

PostIntervalsRewritePatterns.kt guards the divisor's sign (post-bbe9c58a) but
never the dividend's. For IntDiv (CVL mathint division, which truncates toward
zero) the rewrite a / B < C ~~> a < B*C is wrong for negative a.

// Concrete counterexample is correctly caught (constants fold correctly):
rule B1_concrete_counterexample() {
    mathint a = -3; mathint c = -1;
    mathint q = a / 2;
    // (q < c) is (-1 < -1) = false ; (a < 2c) is (-3 < -2) = true. NOT equivalent.
    assert (q < c) == (a < 2*c);   // Violated: correctly caught on constants.
}

// Symbolic version -- the buggy rewrite fires and proves the false equivalence:
rule B1_divLt_mathint(mathint a, mathint c) {
    require a < 0 && a > -1000000;
    mathint q = a / 2;
    assert (q < c) == (a < 2*c);   // FALSE at a=-3,c=-1. Verified + non-vacuous => BUG.
}

Reproduce

Unpack repro.tar.gz

certoraRun.py B1.conf

Actual: Rule is verified.
Expected: Rule should be violated.

Version

Self-built 07.07.26 Release