smod: incorrect encoding leads to incorrectly pruned path

[intrigus-lgtm]

TACExpr.BinOp.SMod.toLExpression computes the negative-dividend branch with mathematical IntSub (no mod-2^256 wrap): when a positive divisor exactly divides a negative dividend the result is 2^256, outside the 256-bit range, so the type-bound 0 <= v < 2^256 makes the path contradictory and it is pruned.
Reality: a=-12, b=6 -> 0.

The prover incorrectly concludes that the rule cannot be violated therefore:

rule A1_sMod_negative_never_zero(int256 a, int256 b) {
    require b != 0;
    require a < 0;
    int256 r = sMod(a, b);
    assert r != 0;   // FALSE at a=-12,b=6.  Verified => BUG.
}

Reproduce

Unpack repro.tar.gz

certoraRun.py A1.conf

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

Version

Self-built 07.07.26 Release