Silicon's verification never ends in some Viper tutorial's examples

[viper-admin]

Created by @fabiopakk on 2019-01-18 15:45 Last updated on 2019-08-29 09:46

Silicon doesn&~~https://github.com/viperproject/silicon/issues/39~~;t terminate (in reasonable time) for the examples listed below. It seems that Z3 gets &https://github.com/viperproject/silicon/issues/34;stuck&https://github.com/viperproject/silicon/issues/34;. The following files can be found in the examples repository:

Directory cav2017:

• FencesDblMsgPass.sil
• RSLLockNoSpin-not-in-appendix.sil
• FencesDblMsgPassSplit.sil
• FencesDblMsgPassAcqRewrite.sil
• FollyRWSpinlock_err.sil
• FollyRWSpinlockStronger.sil
• RelAcqRustARCStronger.sil
• RSLSpinlock.sil
• RustARCOriginal_err.sil
• RustARCStronger.sil

Directory vmcai2016:

• ~~linked-list-predicates-with-wands.sil~~

[viper-admin]

@fabiopakk on 2019-01-21 08:31:

• edited the title
• edited the description

[viper-admin]

@mschwerhoff on 2019-03-02 22:38:

• edited the description

[viper-admin]

@alexanderjsummers commented on 2019-08-29 09:45

• linked-list-predicates-with-wands.sil seems to be fine again

[viper-admin]

@alexanderjsummers on 2019-08-29 09:46:

• edited the description