description
A common idiom in writing object invariants is to write "soft approval" invariants of the form $p \/ \inv2(o)$, where o is of a known type. When the proof of such an invariant fails, there is no indication about which invariant of $o$ is failing, which makes debugging the proof difficult if o has a large number of invariants.
One possible approach to providing a more informative error message would be to expand \inv2(o) to its definition when it occurs in a proof obligation with positive polarity.