Unsoundness related to QPs with unsatisfiable conditions

[marcoeilers]

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]

(This is different but vaguely similar to the problem fixed in #690)

[marcoeilers]

Fixed in #843