Assertion failure when mixing unrelated unfolding and labeled old

[viper-admin]

Created by @vakaras on 2018-03-30 18:02

The following example succeeds in Silicon but fails in Carbon:

#!silver
field x: Ref

field y: Ref

function globalRd(): Perm
  ensures none < result && result < write 

predicate P(self: Ref) {
  acc(self.x, globalRd())
}

function int___unbox__(box: Ref): Int
  ensures __prim__int___box__(result) == box

function __prim__int___box__(prim: Int): Ref
  ensures int___unbox__(result) == prim

method test()
{
  var self: Ref
  inhale acc(self.y) && acc(P(self))
  self.y := __prim__int___box__(1)
  label l
  // Assert might fail. Assertion old[l]((unfolding acc(P(self), write) in int___unbox__(self.y) == 1)) might not hold. ([email protected])
  assert old[l](unfolding acc(P(self)) in int___unbox__(self.y) == 1)
}