Corner-case incompleteness with vacuous magic wand

[mschwerhoff]

Silicon fails to assert false after a vacuous wand has been applied. The program originates from the discussion around #485.

field val: Bool

method first(x: Ref)
    requires acc(x.val)
    ensures acc(x.val)
    ensures acc(x.val) --* acc(x.val) && x.val
{
    package acc(x.val) --* acc(x.val) && x.val {
        assume x.val == true // In general unsound
    }
}

method second(x: Ref)
    requires acc(x.val)
{
    first(x)
    x.val := false
    apply acc(x.val) --* acc(x.val) && x.val
    assert x.val == true
    assert x.val == false // Fails in Silicon, but not in Carbon
    assert false          // Likewise
}