alexanderjsummers

Same issue posted for Silicon here: https://github.com/viperproject/silicon/issues/656

It could be that the code in [viper.silver.ast.MagicWand.structure](https://github.com/viperproject/silver/blob/bab3e3ef57b3cbdead702ca5641a5a3dd0c69750/src/main/scala/viper/silver/ast/Expression.scala#L165) should be adapted; the "identity" of the old state used is not considered a "hole" in the structure generated. I'm not exactly...

Here's a smaller one: ```field f : Int function toSeq(s: Seq[Ref]) : Seq[Int] requires forall i : Int :: 0 acc(s[i].f) ensures |result| == |s| ensures forall i : Int...

Interestingly, it seems to also verify when the triggers are made {r.next}{r.val} - without r.val as a trigger there seems to be a difficulty in finding the permissions to r.val...

Hi Malte, Thanks - that explains why some triggers are needed (although in this example other choices will get made by Viper if we leave triggers out, that unfortunately lead...

I think we should check self-framedness with the unknown positive multiplier. This means the check remains attached to the definition where the problem is introduced; dually, it doesn't rely on...

Hi there, Sorry to join the thread so late. I had a quite look at the example. The trigger nodes[next(tid, |nodes|)].out would generally only be matched by a correspondingly used...

A minor wrinkle, but only added here for the sake of completeness of the discussion: Right now, under certain slightly fiddly conditions, one can syntactically check that a heap-dependent function...