viper-admin

> **@fabiopakk** commented on 2019-11-18 13:22 The following files no longer have this issue and were removed from the ignore file clause: * tree\_delete\_min.vpr * arrays\_quickselect\_rec.vpr Issues with the files...

> **@mschwerhoff** commented on 2018-11-25 12:02 Observation: - The code verifies if the explicit triggers are removed - Changing `none < old[pre_havoc](perm(P(r, x)))` to `none < perm(P(r, x))` in the...

> **@marcoeilers** commented on 2017-04-23 18:09 I looked into this a little, I think I now have some idea what's going on. In Boogie, at some point during the verification...

> **@marcoeilers** on 2017-04-23 18:09: > * edited the description > * changed `priority` from `major` to `critical`

> **@marcoeilers** on 2017-05-02 09:57: > * edited the description

> **@marcoeilers** commented on 2017-05-02 10:03 I found what I think is another instance of the same problem: ``` function SCIONPath_get_hof(self: Ref): Ref requires acc(outer(self), wildcard) { ( let idx_0...

> **@marcoeilers** commented on 2017-05-02 10:05 Attached Boogie file for first example.

> **@marcoeilers** on 2017-05-02 10:05: > * changed `attachment` from `(none)` to `test1.bpl`

> **@marcoeilers** commented on 2017-05-02 10:06 Attached Boogie file for second example.

> **@marcoeilers** on 2017-05-02 10:06: > * changed `attachment` from `(none)` to `test2.bpl`