Code contracts warning DateTime.HasValue always evaluates to a constant value

Question

I have a problem which may be a bug in code contracts or I'm just missing something.

I have a class with a nullable DateTime property DateValue which gets set by the constructor. The class's == overload states that 2 objects are equal if first.DateValue == second.DateValue. Strangely, this comparison causes code contract warning:

The Boolean condition first.DateValue.HasValue always evaluates to a constant value. If it (or its negation) appear in the source code, you may have some dead code or redundant check

// relevant code only. full code posted later
public class ClassWithDate
{
    public DateTime? DateValue { get; private set; }

    public ClassWithDate(DateTime? dateValue)
    {
        DateValue = dateValue;
    }

    public static bool operator ==(ClassWithDate first, ClassWithDate second)
    {
        // ...

        // !! CODE CONTRACT WARNING HERE !!
        return (first.DateValue == second.DateValue);
    }

    // ...
}

I don't understand why the rewriter would think that DateValue.HasValue is always a constant value, nor what it has to do with DateTime equality.

Am I missing something with code contracts? Or with the equality overloads? Could this be a bug in code contracts?

Full code below.

public class ClassWithDate
{
    public DateTime? DateValue { get; private set; }

    public ClassWithDate(DateTime? dateValue)
    {
        DateValue = dateValue;
    }

    public override bool Equals(object obj)
    {
        return ((obj as ClassWithDate) != null) && (this == (ClassWithDate)obj);
    }

    public static bool operator ==(ClassWithDate first, ClassWithDate second)
    {
        if (object.ReferenceEquals(first, second)) return true;
        if (((object)first == null) || ((object)second == null)) return false;

        // compare dates
        return (first.DateValue == second.DateValue);
    }

    public static bool operator !=(ClassWithDate first, ClassWithDate second)
    {
        return !(first == second);
    }

    public override int GetHashCode()
    {
        return (DateValue == null ? 0 : DateValue.GetHashCode());
    }
}

Answer 1

From my experience this is a bug in Code Contracts. I have encountered it in other situations. Take a look at this question (and answers), which is similar in nature to your issue: CodeContracts: Boolean condition evaluates to a constant value, why?