Skip to main content

errors.PostconditionError

Output data violates a postcondition (only raised by runtime checks).

Usage

Source

errors.PostconditionError()

Import it from sverify.errors. Raised with on_unproved="check", when a postcondition the checker could not prove fails on the output rows. The message says how many output rows violate which condition.