InlineAssume attribute for ensures clauses; if present, the ensures condition is assumed while inlining.