Incompleteness with respect to quantifiers in functions ?

viperproject / carbon

Verification-condition-generation-based verifier for the Viper intermediate verification language.

Mozilla Public License 2.0

29 stars 19 forks source link

Open viper-admin opened 8 years ago

viper-admin commented 8 years ago

Created by @alexanderjsummers on 2015-10-26 17:09 Last updated on 2015-11-10 16:13

The attached file verifies in Silicon but not in Carbon

Attachments:

viper-admin commented 8 years ago

@mschwerhoff commented on 2015-11-10 16:13

FYI: The example verifies in Silicon, but (currently) only with --recursivePredicateUnfoldings 2 (see also https://github.com/viperproject/silicon/issues/181)