Example (functions + sequences) with a potential matching loop

[viper-admin]

Created by @mschwerhoff on 2016-01-14 13:59 Last updated on 2019-08-28 10:05

Attached file arraylist-quantified-permissions_LOOP.sil appears to have a matching loop, when it is simplified by removing function content (cf. arraylist-quantified-permissions.sil), then it verifies quickly.

linked-list-predicates-with-wands.sil uses a similar combination of functions and sequences, and is also fairly slow.

---

Attachments:

• arraylist-quantified-permissions_LOOP.sil
• linked-list-predicates-with-wands.sil
• logfile-0208.smt2
• arraylist-quantified-permissions.sil
• logfile-0208-z3.zip

[viper-admin]

@mschwerhoff commented on 2016-09-26 12:57

Attached a stripped-down version of the SMT2 logfile Silicon generated when run on the example arraylist-quantified-permissions_LOOP.sil, and the logfile generated by Z3 when run on that SMT2 file.

Observations so far:

• Z3 terminates immediately if only one check-sat occurs in the SMT2 file. This could mean that the poor performance is due to Z3's incremental solver.
• The axiom profiler unfortunately crashes on the generated Z3 logfile, see this issue.

[viper-admin]

@mschwerhoff on 2016-09-26 12:57:

• changed attachment from (none) to logfile-0208.smt2

[viper-admin]

@mschwerhoff commented on 2016-10-25 12:13

The example examples\vmcai2016\linked-list-predicates-with-wands.sil has been disabled for now since the verification time exhibited by Silicon is unstable. It is still unclear, why - see the previous comment.

[viper-admin]

@mschwerhoff commented on 2018-06-09 12:10

@alexanderjsummers The files mentioned in this issue might be of interest to Nils Becker

[viper-admin]

@alexanderjsummers commented on 2019-08-28 10:05

Is it possible to analyse these with the new version of the Axiom Profiler?