Predicate-Related Incompleteness

[dohrau]

In the example below, the assertion fails even though it should not. This is likely due to Silicon not being able to prove that the predicate instances p(x) and p(x.next) have to be different (the first one coming from the inhale statement and the other one from within the unfolded predicate). The fact that the assertion assert x != null ==> x != x.next fails if inserted right after the unfold statement supports this suspicion.

field next: Ref
predicate p(x: Ref) { x != null ==> acc(x.next) && p(x.next) }

method m(x: Ref)
{
    inhale p(x)
    unfold p(x)
    if (perm(p(x)) == write) {
        assert false
    }
}

[mschwerhoff]

Duplicate of issue #40