Remove witness exclude-vars from svcomp conf

[sim642]

Similarly to #1592, this is something where we appear to fingerprint tasks... Although these exclusion don't affect our verdict, only the generated witnesses.
But witness validation still affects SV-COMP scores, so it's not harmless.

I want to do some runs with witnesses to see what difference this really makes. Over time we've improved invariant generation to be smarter and avoid redundant data, so maybe this sort of witness size reduction is unnecessary now.

[sim642]

I want to do some runs with witnesses to see what difference this really makes. Over time we've improved invariant generation to be smarter and avoid redundant data, so maybe this sort of witness size reduction is unnecessary now.

This doesn't seem to impact the size at all (with 60s timeout): before and after we produce 2.5GB of YAML witnesses.
In terms of results, Goblint can validate 30 fewer ldv-linux-3.4-simple/ task witnesses out of ~7000.

[michael-schwarz]

Maybe we need to some mechanism to give up on witnesses once they become too large and produce the trivial witness so we can still get points?

I'm not sure I'm happy with the general direction, we currently seem to solve fewer tasks in each of the PRs from the last few weeks. Is this really a good strategy?

[sim642]

This is just self-validation though. I sampled some of the differing tasks and we don't score points just from self-validation, but other validators also confirm our results. So I don't think there's much of a loss here. As I said, this doesn't make a notable size difference.

Solving fewer tasks is better than getting disqualified for using task-specific identifiers to score more points.