Expand the evaluator API to allow ignoring contracts locally

epfl-lara / inox

Solver for higher-order functional programs, used by Stainless

Apache License 2.0

88 stars 20 forks source link

Expand the evaluator API to allow ignoring contracts locally #197

Closed mario-bucev closed 1 year ago

mario-bucev commented 1 year ago

This change enables https://github.com/epfl-lara/stainless/issues/1377 to be fixed. stainless.evaluators.RecursiveEvaluator will override ignoreContractsOn to also consider expressions annotated with @DropVCs or @dropConjunct.