Separating conjunction in package statement does not lead to unreachable state

[marcoeilers]

The following fails to verify in Carbon:

field data: Int


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

Silicon verifies this. Carbon does not, but it does if we change the assert to assert acc(x.data, 2/1). So Carbon does seem to know that it cannot have the double permission inside the package statement, but it doesn't realize this when it comes via the separating conjunction.

This might be a duplicate, but I haven't found an existing issue that describes this.