Действительно ли это - ошибка в статическом средстве проверки контракта?

Если я пишу это:

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        if (count == 1)
            owner = null;
        --count;
    }
}

Статическое средство проверки контракта может доказать все утверждения.

Но если я пишу это вместо этого:

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        --count;
        if (count == 0)
            owner = null;
    }
}

Это требует постусловия owner == null || count > 0 бездоказательно.

Я думаю, что могу доказать, что вторая форма не нарушает это постусловие:

// { count > 0 } it's required
--count;
// { count == 0 || count > 0 } if it was 1, it's now zero, otherwise it's still greater than zero
if (count == 0)
{
    // { count == 0 } the if condition is true
    owner = null;
    // { count == 0 && owner == null } assignment works
}
// { count == 0 && owner == null || count != 0 && count > 0 } either the if was entered or not
// { owner == null || count > 0 } we can assume a weaker postcondition

Что-то не так с моим доказательством?

Я добавил утверждения в своем доказательстве как Contract.Assert вызовы к коду, и я пришел к выводу, что, если я добавляю просто этого, ему удается доказать постусловие:

--count;
Contract.Assert(count == 0 || count > 0)
if (count == 0)
    owner = null;

Но, если я теперь изменяю то же самое утверждение на "более естественный" путь, оно перестало работать:

--count;
Contract.Assert(count >= 0)
if (count == 0)
    owner = null;

Ожидалось бы, что те два утверждения были эквивалентны, но статическое средство проверки рассматривает их по-другому.

(Я использую бету 2 VS10 между прочим),