Wand package incompleteness?

[marcoeilers]

The following example verifies in Silicon, as I think it should, but not in Carbon, where the assert false fails:

field data: Int

method bar(x: Ref)
    requires acc(x.data)
{
    package acc(x.data) --* false {
        assert acc(x.data) && acc(x.data)
        assert false
    }
}

As far as I can see, the wand holds. And in my understanding of package statements, which could be completely wrong, the first assertion should force the outside permission to x.data to be added to the wand's footprint, which should enable me to prove false. But I'm not 100% certain about either of these statements.