Clean usage of options in regressions (#8190)

Clean usage of options in regressions (#8190)

We now support tester annotations, thus it is best practice not to use check-unsat-cores or check-models explicitly in the regressions.

This changes regressions to not use these options, where these options are either:

removed entirely (the benchmark was fixed in the meantime)
changed to -q (the benchmark succeeds with a warning)
changed to produce- instead of check- if the option on the benchmark is required to ensure a configuration of models/unsat-cores is run. This is done for unsat-cores on sat benchmarks and models on unsat benchmarks.
replaced by DISABLE-TESTER: model.
one spurious regression is deleted, which was identical to another + check-models.
It also makes some fixes to enable more benchmarks succeed with check-models, and adds a warning when fmf-fun is combined with check-model.