Surprising Verification Failures with Nested Datatypes + Classes about dafny HOT 2 OPEN

I agree, this is unexpected behavior.

from dafny.

Thanks you for the many useful test cases! (Note from @keyboardDrummer: this is indeed a bug)

Workaround

As a workaround, adding any one of these three statements in the body of Fail1 makes the postcondition verify:

assert c.inner.inner.Foo() == 0;
assert c.inner.Wrap?;
var cc := c.inner.inner;

Notes on fixing the problem in the Dafny verifier

The problem is that the verifier needs the information that c.inner (in Fail1) has type Wrap<C> or, alternatively, that c.inner.Wrap? holds. This assumption is generated by the verifier, but the information is missing since the c.inner appears in a postcondition.

The information is generated into a free ensures postcondition for Impl$$_module.__default.Fail1 in Boogie. However, a free ensures in Boogie is ignored when checking an implementation. The Boogie attribute {:always_assume} that turns a free ensures into an assumption when verifying the implementation. The fix is to add that attribute (to all "assume conditions" generated by TrSplitExpr, both when those condition go into free ensures and when they go into free requires. This fix may have a large impact on other verifications.

from dafny.