Suppress redundancies
•Avoid deriving variables: suppress 25-50%
–equal to another variable
–nonsensical
•Avoid checking invariants:
–false invariants: trivial improvement
–true invariants: suppress 90%
•Avoid reporting trivial invariants:
suppress 25%
[Don’t say “tautologically equal”.]

Make it clear that all of this is a good thing.
First two are runtime improvements; third is UI improvement.

Equal to another variable.  EXAMPLE.
Nonsensical:  a[i] when i<0  (or when i>length(a) )
Staged inference and derivation is key to avoiding deriving variables; that is why this works.

All this is a substantial chunk of code.
All of the percentages are cumulative.  It’s not just a quantitative but a qualitative improvement; system wouldn’t run without staging.