Почему этот строковый вызов Contract.Ensure недоказан?

В моем приложении .Net 4 есть следующий код:

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

static string S = "1";

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

Это дает мне гарантированное недоказанное предупреждение во время компиляции:

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

Что происходит? Это отлично работает, если S является целым числом. Он также работает, если я изменяю Ensure на S == Contract.OldValue (S + "1") , но это не то, что я хочу делать.