Why is this string-based Contract.Ensure call unproven?

Question

I have the following code in my .Net 4 app:

static void Main(string[] args) {
    Func();
}

static string S = "1";

static void Func() {
    Contract.Ensures(S != Contract.OldValue(S));
    S = S + "1";
}

This givens me an ensures unproven warning at compile time:

warning : CodeContracts: ensures unproven: S != Contract.OldValue(S)

What is going on? This works fine if S is an integer. It also works if I change the Ensure to S == Contract.OldValue(S + "1"), but that's not what I want to do.

Answer 1

I'm guessing the contracts engine just isn't smart enough to understand that this is guaranteed. If you had said:

S = S + "";

... then the contract wouldn't work. So the engine would have to do some extra logic to determine that S = S + "1" will always change the value of the string. The team simply hasn't gotten around to adding that logic.