@karoliineh found that for ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--block--paride--on26.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out in sv-benchmarks we output tens of thousands of invariants into the YAML witness. As of current master, 43083 loop invariants to be exact.

Most of them seemed to be equalities between __cil_tmp variables which are actually in the program (because it is cilled), not introduced by us, so it's not the filtering of temporaries at fault.
Instead, these equalities come from large var_eq equality clusters because there are many of those variables pulled up to function level, so all of the equalities are in scope in many points in large functions.

The current var_eq invariant generation is not that great: it outputs a quadratic number of pairwise equalities from a cluster (only deduplicating by reflexivity and symmetry). Arguably, this is very redundant: we shouldn't have to make transitivity explicit.
Therefore, this PR changes var_eq invariant generation to output a linear number of equalities with a single element from the cluster, the rest follow by transitivity implicitly.

For the SV-COMP task above, we now only output 859 loop invariants!
We no longer OOM when trying to validate our own witness to this task. However, we also don't confirm it yet because of #1710.