silicon Poor and/or fluctuating performance of two programs using magic wands

Poor and/or fluctuating performance of two programs using magic wands

Open viper-admin opened this issue 7 years ago • 3 comments

Created by @mschwerhoff on 2017-03-06 15:11 Last updated on 2019-08-28 10:21

Attached file BinomialHeap-SlowWand.sil takes surprisingly long to verify, but doesn&~~https://github.com/viperproject/silicon/issues/39~~;t use quantifiers, sequences, or any other &https://github.com/viperproject/silicon/issues/34;known&https://github.com/viperproject/silicon/issues/34; reason for possible performance degradation. The generated SMT2 file is also surprisingly large (about 5 MB).

The verification time of wands/examples_paper/list_insert_heuristics.sil currently fluctuates between a few seconds and more than 150s.

Attachments:

Mar 06 '17 15:03 viper-admin

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

Would it be worth running these again?

Aug 28 '19 10:08 viper-admin

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

(it seems they need converting to the new wand syntax)

Aug 28 '19 10:08 viper-admin

@alexanderjsummers on 2019-08-28 10:21:

edited the description

Aug 28 '19 10:08 viper-admin