viper-admin
viper-admin
> **@alexanderjsummers** on 2018-07-06 14:06: > * changed `state` from `duplicate` to `open`
> **@alexanderjsummers** commented on 2019-01-22 21:16 Hi Fábio, thanks for the issue. Could you attach the current versions of the examples, please? Thanks!
> **@fabiopakk** commented on 2019-02-04 08:58 Sure, files are in attachment now.
> **@fabiopakk** on 2019-02-04 08:58: > * changed `attachment` from `(none)` to `exercise2.sil`
> **@alexanderjsummers** on 2016-01-13 17:14: > * edited the title > * edited the description > * changed `priority` from `trivial` to `minor`
> **@mschwerhoff** commented on 2018-06-09 12:08 I just investigated `quantifiedpermissions/sequences/bsearch.sil` and found four genuine errors (two programming errors, two specification errors) that explain why the originally reported code doesn't verify....
> **@mschwerhoff** commented on 2018-01-23 16:53 Actually, I am surprised that Silicon verifies this program: `f1` essentially gives rise to the postcondition axiom `forall h: Heap :: {f1(h)} 1 ==...
> **@alexanderjsummers** on 2018-01-23 17:01: > * edited the title
> **@alexanderjsummers** on 2018-01-23 17:01: > * edited the title
> **@alexanderjsummers** commented on 2018-01-23 17:02 I agree that in principle the verifier would be allowed to prove false for such a program, and am not surprised that it doesn't...