const-prop: wrong rewrite for 1 %n -> 1

[intrigus-lgtm]

ConstantPropagatorAndSimplifier rewrites 1 % n -> 1 whenever the divisor n is
symbolic. But 1 % 1 == 0, and n = 1 sails past Solidity's zero-check panic.

rule A4_oneMod_is_one(uint256 n) {
    require n != 0;
    uint256 r = oneMod(n);
    assert r == 1;   // FALSE at n=1 (1 % 1 = 0).  Verified => BUG.
}

Reproduce

Unpack repro.tar.gz

certoraRun.py A4a.conf

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

Version

Self-built 07.07.26 Release