Philipp Wendler

Should these tasks simply be renamed to remove the other verdict? Probably it would be better to fix them, but I can't do this.

@dbeyer What should be do here? Will you contact the authors of these tasks and ask for fixes, or should we remove the label for the other property (the one...

`c/check.py` already has [some property-related checks](https://github.com/sosy-lab/sv-benchmarks/blob/63db68c3d3dcf9e5cf4a1a95efccb04e9d40c08e/c/check.py#L430-L491) including checks that ensure consistency between some properties, so I guess it would not be difficult to add it there (depending on how complex...

Yes, the licensing should be properly handled. The best and easiest way to do this would be to decide on #1099, add machine-readable (REUSE-style) license headers to all relevant source...

Now that #1099 is closed to getting merged: For which directories would you need REUSE-style license declarations in order to be able to update this PR? After we have this...

Oh, that's a problem. For both `systemc` and `bitvector` we still do not know the license (cf. #165), so if we want to do this correctly and add new these...

Right, I overlooked this pair. This seems doable. All ECA programs should be easy, because I think there were never any cases where other people added tasks to their directories...

Is this actually reachable in the code? If not, there is no problem, right? I had a look at a few calls of those calls, and all where cases where...

`__VERIFIER_nondet_charp` can be replaced by `__VERIFIER_nondet_pchar`. But actually, we removed `__VERIFIER_nondet_pointer` in the past (https://github.com/sosy-lab/sv-benchmarks/issues/767) and the same reasoning also applies to other pointer-returning nondet methods. So these should probably...

It is my understanding that extern functions should just be treated as returning a nondeterministic value. If their precise semantics is not important for the safety of the benchmark, we...