Simple contracts on System.Guid failing

Question

Per this thread, the following should work perfectly for both the String and Guid property/field.  However, while it works for the String type, apparently there's something different about the Guid type that causes the static analyzer to fail when checking this code.

using System;
using System.Diagnostics.Contracts;

namespace MSDNForumSample
{
    public sealed class Foo
    {
        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(!String.IsNullOrEmpty(_bar));
            Contract.Invariant(!Guid.Equals(_id, Guid.Empty));
        }


        private string _bar;
        private Guid _id;


        public string Bar
        {
            [Pure]
            get
            {
                Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<string>()));
                return _bar;
            }
            set
            {
                Contract.Requires(!String.IsNullOrEmpty(value));
                _bar = value;
            }
        }

        public Guid Id
        {
            [Pure]
            get
            {
                Contract.Ensures(!Guid.Equals(Contract.Result<Guid>(), Guid.Empty));
                return _id;
            }
            set
            {
                Contract.Requires(!Guid.Equals(value, Guid.Empty));
                _id = value;
            }
        }


        //public Foo(string bar)
        //    : this(bar, Guid.NewGuid())
        //{
        //    Contract.Requires(!String.IsNullOrEmpty(bar));
        //}

        public Foo(string bar, Guid id)
        {
            Contract.Requires(!String.IsNullOrEmpty(bar));
            Contract.Requires(!Guid.Equals(id, Guid.Empty));
            Contract.Ensures(String.Equals(Bar, bar));
            Contract.Ensures(Guid.Equals(Id, id));

            _bar = bar;
            _id = id;
        }
    }
}

Result: "CodeContracts: Checked 10 assertions: 5 correct 5 unknown"

I'm pretty sure Guid is a value type. :)  So what's going on here?

(Note: The constructor overload that passes in Guid.NewGuid() is also not verified - apparently there's no postcondition on Guid.NewGuid() that the result will not be Guid.Empty?)

---

Lars Kemmann

P.S.: I'm using Code Contracts 1.4.50126.1 with a .NET Framework 4.0 project, VS 2010 Pro, assembly mode = "Standard Contract Requires", "Perform Static Contract Checking" with  "Show squigglies" and "Suggest Requires" plus "Warning Level = hi".