viper-admin

> **@alexanderjsummers** commented on 2018-05-08 16:04 See also [the same Silicon issue](https://github.com/viperproject/silicon/issues/330)

> **@alexanderjsummers** commented on 2018-05-09 15:42 See [this Z3 Stackoverflow post](https://stackoverflow.com/questions/50250336/unexpected-unknown-with-ill-defined-function-definition-axiom)

> **@mschwerhoff** commented on 2019-02-20 08:20 For the record: I think Silicon doesn't properly handle `old` expressions and triggering. I'd be interested in sitting down at some point to discuss...

> **@marcoeilers** commented on 2019-08-28 13:03 This no longer causes Boogie errors, but assertions cannot be proved even though they apparently should, so I’ll leave this open.

> **@alexanderjsummers** on 2019-08-19 13:15: > * edited the description

> **@vakaras** commented on 2018-07-25 09:16 Silicon [issue](https://github.com/viperproject/silicon/issues/349).

> **@fabiopakk** commented on 2019-10-04 14:08 Added unexpected output annotations in the following files: * quickselect//arrays\_quickselect\_rec.sil * vmcai2016//linked-list-predicates-with-wands.sil ‌

> **@aterga** on 2019-11-04 15:05: > * changed the assignee from (none) to **@aterga**

> **@alexanderjsummers** commented on 2018-06-06 09:42 At the moment, Carbon also selects the location for the QP as a trigger, both in the Heap and in the Mask (for permission...

> **@mschwerhoff** commented on 2018-10-12 14:01 Note: could actually be caused by .