viper-admin

> **@vakaras** commented on 2018-07-25 09:15 Carbon [issue](https://github.com/viperproject/carbon/issues/250).

> **@mschwerhoff** commented on 2018-08-07 14:01 @vakaras @alexanderjsummers Did you look at Z3's axiom instantiation statistics to confirm your matching loop theory ? It could also be that Z3's macro...

> **@vakaras** commented on 2018-08-15 10:00 @mschwerhoff I have added the following method: ``` #!silver method test3a(n: Int) { assert fib3(n) > 0 } ``` Executed Silicon with Z3 logging...

> **@mschwerhoff** commented on 2018-08-07 13:52 was marked as a duplicate of this issue.

> **@alexanderjsummers** commented on 2018-08-07 15:20 **(superceded by comment below)** In my opinion, this isn't a Silicon-specific issue; the behaviour is identical in both back-ends, and seems to me consistent...

> **@mschwerhoff** commented on 2018-08-07 15:34 So Carbon needs the 2nd invariant as well? I am fairly certain that this wasn't always the case; maybe something in the encoding changed...

> **@mschwerhoff** commented on 2018-10-15 08:53 was marked as a duplicate of this issue.

> **@alexanderjsummers** commented on 2018-10-15 08:56 It seems the additional loop invariant is not needed for Carbon. I suspect that my comment above was because of an unrelated issue; at...

> **@alexanderjsummers** commented on 2018-10-15 09:03 For Silicon, would a potential encoding (just looking at how to get from state before the loop to state at the start of the...

> **@alexanderjsummers** commented on 2018-10-15 09:09 I think the second half of my first comment above is also spurious. The point is that if some permission is framed around the...