Skip to content

Quantifiers for function contracts #2546

@JustusAdam

Description

@JustusAdam

A rudimentary implementation for forall and exists for kani function contracts. They are implemented as higher-order builtins, which compile to __CPROVER_forall and __CPROVER_exists respectively.

Metadata

Metadata

Labels

Z-QuantifiersIssues related to quantifiers[C] Feature / EnhancementA new feature request or enhancement to an existing feature.

Type

No type

Projects

Relationships

None yet

Development

No branches or pull requests

Issue actions