Expand the evaluator API to allow ignoring contracts locally (!197) · Merge requests · LARA / inox

Viktor Kuncak requested to merge github/fork/mario-bucev/ignore-contracts-locally into main Mar 22, 2023

Created by: mario-bucev

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.

Expand the evaluator API to allow ignoring contracts locally

Merge request reports