Function targets_return_value 

fn targets_return_value(property: &Property<'_>) -> bool

Whether an invariant targets the function’s return value (as opposed to a parameter / the receiver). Only Atom invariants carry a first-argument place; And/Or invariants have no target_place, so they are never treated as return-value invariants.