Should the Code Contracts static checker be able to check arithmetic bound?

I’ve had an answer on the MSDN forum. It turns out I was very nearly there. Basically the static checker works better if you split out “and-ed” contracts. So, if we change the code to this:

public static int RollDice(Random rng)
{
    Contract.Ensures(Contract.Result<int>() >= 2);
    Contract.Ensures(Contract.Result<int>() <= 12);

    if (rng == null)
    {
        rng = new Random();
    }
    Contract.Assert(rng != null);

    int firstRoll = rng.Next(1, 7);
    Contract.Assume(firstRoll >= 1);
    Contract.Assume(firstRoll <= 6);
    int secondRoll = rng.Next(1, 7);
    Contract.Assume(secondRoll >= 1);
    Contract.Assume(secondRoll <= 6);

    return firstRoll + secondRoll;
}

That works without any problems. It also means the example is even more useful, as it highlights the very point that the checker does work better with separated out contracts.