"Packaging wand might fail" in Viper online example

[fabiopakk]

Carbon is emitting the following messages for the program in attachment:

• Packaging wand might fail. Assertion elems(l1) == old(elems(l1)[..index]) ++ oldlhs might not hold.

• Postcondition of appendit_wand might not hold. Assertion elems(l1) == old(elems(l1) ++ elems(l2)) might not hold.

The same program verifies correctly in Silicon. This program is part of Viper tutorial and is located in magic wands section, heap-dependent expressions subsection. The issue consistently occurs both in Viper online and in local setups.

field next : Ref
field val : Int

predicate list(start : Ref)
{
  acc(start.val) && acc(start.next) &&
    (start.next != null ==> list(start.next))
}

function elems(start: Ref) : Seq[Int]
  requires list(start)
{
  unfolding list(start) in (
    (start.next == null ? Seq(start.val) :
     Seq(start.val) ++ elems(start.next) ))  
}

method appendit_wand(l1 : Ref, l2: Ref)
  requires list(l1) && list(l2) && l2 != null
  ensures list(l1) && elems(l1) == old(elems(l1) ++ elems(l2))
  {
    unfold list(l1)
    if(l1.next == null) {
      l1.next := l2
      fold list(l1)
    } else {
      var tmp : Ref := l1.next
      var index : Int := 1

      package list(tmp) --* list(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
      {
        fold list(l1)
      }

      while(unfolding list(tmp) in tmp.next != null)
        invariant index >= 0
        invariant list(tmp) && elems(tmp) == old(elems(l1))[index..]
        invariant list(tmp) --* list(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
      {
        unfold list(tmp)
        var prev : Ref := tmp
        tmp := tmp.next
        index := index + 1

        package list(tmp) --* list(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
        {
          fold list(prev)
          apply list(prev) --* list(l1) && elems(l1) == old(elems(l1)[..index-1]) ++ old[lhs](elems(prev))
        }  
      }
      unfold list(tmp)
      tmp.next := l2
      fold list(tmp)
      apply list(tmp) --* list(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
    }

[fabiopakk]

Due to this bug, I've removed Carbon from the list of verifiers in Viper Online, for this example only. This removal should be reverted once this bug is fixed.