viper-admin

> **@alexanderjsummers** on 2015-06-10 09:46: > * edited the description > * edited the title

> **@alexanderjsummers** on 2015-11-25 15:53: > * edited the description > * edited the title

> **@alexanderjsummers** commented on 2015-11-25 16:11 The behaviour doesn't seem to be consistent between the two verifiers. We should check that the axiomatisations are in sync.

> **@aterga** commented on 2017-01-08 23:10 This issue is (at least partially) related to triggering. The following code verifies: ``` function notNull(x: Ref): Bool { x != null } method...

> **@alexanderjsummers** commented on 2018-04-30 10:07 Some improvements were made in Carbon commit

> **@mschwerhoff** commented on 2018-05-01 12:43 @alexanderjsummers Should these recent changes be ported to Silicon?

> **@alexanderjsummers** commented on 2018-05-02 10:21 I'm not sure how stable the solution is yet.

> **@alexanderjsummers** commented on 2018-07-06 14:04 For reference, I reverted the changes, but am still optimistic that something better can be done..

> **@alexanderjsummers** commented on 2018-07-09 15:45 Here's another good one: ``` #!scala field data: Seq[Int] function f(x:Int) : Bool method test(i:Int) { var s : Seq[Int] assume forall x :...

> **@alexanderjsummers** commented on 2018-07-10 09:21 I edited the example above, as Carbon's behaviour changed (I think there was a related bug fixed)