Unsoundness related to QPs with unsatisfiable conditions
Closed this issue · 2 comments
marcoeilers commented
The following program verifies even though it should not:
field f: Ref
field g: Ref
function one(): Int {1}
function two(): Int {2}
predicate P(x: Ref) {
forall i: Int :: one() == two() && x.f != null ==> acc(x.g.f)
}
method hmmm(x: Ref)
{
fold P(x)
assert false
}
This seems to be the problem behind the --conditionalizePermissions
unsoundness recently discovered by @jcp19 and @Dspil
marcoeilers commented
(This is different but vaguely similar to the problem fixed in #690)
marcoeilers commented
Fixed in #843