Turn set files into actual task categories, independent of the SV-COMP competition categories

Turn set files into actual task categories, independent of the SV-COMP competition categories

This commit turns set files like ReachSafety-Arrays.set and MemSafety-Arrays.set into a single set file Arrays.set that includes all tasks that focus on array handling, independent of their properties.

The goal is to get set files that are independent of SV-COMP, but still allow to keep the SV-COMP categories as they are, without changes.

With the old set files, the following issues occurred:

• additional maintenance effort because some set files needed to be synced manually, e.g. MemSafety-MemCleanup and MemSafety-Juliet, or ReachSafety-Arrays and MemSafety-Arrays.
• it was difficult to create any benchmark categories that are different from the SV-COMP categories.
• for categories like MemSafety-Other it was only implicitly visible what categories of tasks they actually contain. Example: WIth the new set files it is now more explicit that in the current SV-COMP configuration, there are separate SoftwareSystems-NoOverflow categories for some SoftwareSystems-Tasks, but that category NoOverflows-Main contains task sets SoftwareSystems-AWS-C-Common and SoftwareSystems-DeviceDriversLinux64. This seems like an inconsistency. Similarly, category Termination-Other includes task set SoftwareSystems-uthash.

While the ReachSafety task set was well maintained with separate task categories, the other SV-COMP categories were often an agglomeration of different tasks. Examples are 'NoOverflows-Main' or 'MemSafety-Other'. Because of this unalignment in set files across properties, we made the following decisions to resolve inconsistencies:

• Tasks verifythis/*.yml were only all included by NoOverflows-Main.set, and other tasks from that category in other meta categories. We introduce sets VerifyThis-Loops.set and VerifyThis-Recursive.set to have a place for verifythis tasks. This more generic categorization adds one additional task to the SV-COMP MemSafety-Other category, namely verifythis/prefixsum_rec.yml. This task was forgotten before.
• Tasks signedintegeroverflow-regression/*.yml were in no category with clear meaning before. We added them to ControlFlow.set. They are similar to unsignedintegeroverflow-sas23, which already is part of ControlFlow.set.
• Tasks termination-15/*.yml were part of Termination-MainHeap, but also of MemSafety-Arrays. Because of the name 'MainHeap' I would have expected to see them in category MemSafety-Heap. I still keep this, use the termination category as ground truth and add the tasks to set Heap-Termination.set.
• Tasks pthread-memsafety/*.yml were part of the MemSafety-Other category, even though category ConcurrencySafety-MemSafety exists. We moved these tasks to that category to avoid an additional set file for this seeming inconsistency
• Some tasks of termination-crafted are part of Termination-MainControlFlow and of MemSafety-Arrays. Other tasks of termination-crafted are part of Termination-MainControlFlow and of MemSafety-Other. In addition, some tasks of termination-crafted with a memsafety property were not included in any memsafety category.
  We now add all tasks of termination-crafted to Termination-MainControlFlow (no change) and to MemSafety-Other (some move from MemSafety-Arrays). This adds some new tasks to SV-COMP's MemSafety category that are visible through this fingerprint comparison: !1542 (351223f1)