Why can't this contract assertion be proven?

Question

I have a class that looks something like this:

class Foo
{
    private IEnumerable<Bar> bars;

    ...

    private void DoSomething()
    {
        Contract.Requires(bars != null);
        Contract.Requires(bars.Any());

        Bar result = bars.FirstOrDefault(b => SomePredicate) ?? bars.First();
        Contract.Assert(result != null); // This asserts fails the static checker as "cannot be proven"
    }
}

As far as I can tell, Contracts has all the information it needs to know that result will not be null. bars has at least one element in it. If one of those elements matches SomePredicate, result will be the first such element. If not, result will be the first element in bars.

Why does the assertion fail?

Answer 1

The colection bars could still contain an item that is null. If that item is the first item then result can still be null.