Attribute Macro open_inv_result
#[open_inv_result]Expand description
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.