sosy-lab/sv-benchmarks

Duplicate Verification Tasks

dbeyer opened this issue · 3 comments

dbeyer commented

Category definition file
SoftwareSystems-DeviceDriversLinux64-ReachSafety.set
contains some verification tasks that are also contained in
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety.set

What is the best solution? Move the verification tasks that are in
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety.set
into separate folders with suffice -large?

kfriedberger commented

Changing the directory structure is maybe not a good idea, but would be simpe to implement.

For the benchmark execution, you can exclude one set from the other.
For CPAchecker, we found a solution that works. See here

dbeyer commented

Nice idea. Let's do it like this.