The numbers worked well enough to only enable the congruence domain for small files on the small part I tested them on but my machine is too slow to run all the tests.
I further just noticed that the option for congruence is not enabled in the sv-comp configuration, because like loop unrolling, at the time I tested it there were a lot of verify errors. Has someone tested it after these were fixed?

I moved the congruence changes over to #911 so we have two separate PRs.

With less than 5 loops, for sv-comp this does not trigger anywhere.

To get the results for the tasks we care about to change, we need to apply this if there are less than 17 loops. Will still benchmark that, but it is dubious if this will be positive overall.

We will not have time to benchmark this in time for the deadline, so let's move it to 2024.

I have now moved this to a separate autotuner forceLoopUnrollForFewLoops that is disabled by default. I propose to merge this now in the interest of reducing the number of stale PRs. We may then investigate the benefits of this option when it is time to prepare the configuration for this year's SV-Comp.