Incompleteness when exhaling a QP whose permission expression depends on the quantified variable inside a package statement
marcoeilers opened this issue · 0 comments
marcoeilers commented
@jcp19 found this one.
The following example does not verify but should:
field f: Int
method m(xs: Set[Ref], ys: Set[Ref])
{
inhale forall r: Ref :: r in xs ==> acc(r.f, r in ys ? 1/2 : none)
package true --* true {
assert forall r: Ref :: r in xs ==> acc(r.f, r in ys ? 1/2 : none)
}
}