viper-admin

> **@alexanderjsummers** commented on 2018-08-15 11:30 I guess there should be no longer chains in such an example. I assume this concerns axioms which the back end generates (similarly for...

> **@alexanderjsummers** commented on 2014-09-12 09:14 see also Carbon issue 28

> Bitbucket user **robinsierra** commented on 2019-06-04 17:47 See also Carbon issue [275](https://github.com/viperproject/carbon/issues/275).

> **@marcoeilers** commented on 2019-07-29 12:58 Similar to the Carbon issue, this can be worked around by calling Silicon with the command line argument ``` --z3Args "smt.qi.lazy_threshold=N" ``` \(where the...

> **@mschwerhoff** commented on 2016-04-10 17:23 This is an incompleteness due to Silicon's missing support for disjunctive aliasing when exhaling permissions (see also ): the branch condition `perm(P(e)) >none` is...

> **@mschwerhoff** on 2016-04-11 18:25: > * edited the title

> **@mschwerhoff** on 2016-04-14 07:39: > * edited the title

> **@mschwerhoff** commented on 2016-04-14 07:39 was marked as a duplicate of this issue. That issue also includes a code snippet that could be added to an eventual regression test.

> **@mschwerhoff** commented on 2017-09-23 13:47 See also ,

> **@mschwerhoff** commented on 2017-09-23 13:47 The non-greedy consume algorithm implemented as part of robinsierra's bachelor's thesis solves this problem. For now, this algorithm is not used by default, it...