Attribute Macro creusot_contracts::macros::open_inv_result

#[open_inv_result]

This attribute can be used on a function or closure to instruct Creusot not to ensure as a postcondition that the return value of the function satisfies its type invariant.