viper-admin
viper-admin
> Created by bitbucket user **nilsbecker_** on 2019-02-27 19:51 > Last updated on 2019-09-30 15:50 For simple loops as shown in the attached file where we have some term `f(x)`...
> Created by bitbucket user **jonhdotnet** on 2018-11-20 22:54 > Last updated on 2019-09-16 10:32 I filed a bug report, and realized I didn't have a way to learn the...
> Created by bitbucket user **nilsbecker_** on 2019-02-27 20:10 > Last updated on 2019-02-27 20:22 It is not uncommon that the bodies of quantifiers contain a number of implications which...
> Created by bitbucket user **nilsbecker_** on 2019-02-27 20:21 In some cases, when z3 doesn't rewrite nested quantifiers into a single quantifier, it may be useful to be able to...
> Created by bitbucket user **nilsbecker_** on 2019-02-27 20:17 Log files generated by z3 already contain information on decisions and corresponding backtracking during the model search. It may be useful...
> Created by bitbucket user **nilsbecker_** on 2019-02-27 20:12 It is currently possible to only load a prefix of a file by clicking "Cancel" while the file is loading. It...
> Created by bitbucket user **nilsbecker_** on 2019-02-27 19:55 When running the Axiom Profiler on Linux using Mono some of the text on the buttons on the right-hand-side ("Show Longest...
> Created by **@mschwerhoff** on 2016-09-26 12:53 The axiom profiler crashes (on Win 10 x64) if the second trace recorded in the zipped Z3 logfile is inspected, i.e. if invoked...
> Created by **@fpoli** on 2018-09-28 13:56 > Last updated on 2019-07-29 14:45 The following program does not verify with Silicon, but it verifies with Carbon. I'm trying to manually...
> Created by bitbucket user **fhahn** on 2016-03-26 18:56 > Last updated on 2016-03-28 11:41 When using unfolding to limit the range of indices of a quantified permission expression, non-nullness...