Incorrect witnesses for concurrency violation
There are a few SV-COMP tasks where CPAchecker produces an invalid violation witness according to the witness linter.
Example:
scripts/cpa.sh -svcomp21 -heap 10000M -benchmark -timelimit '900 s' -stats -spec ../../sv-benchmarks/c/properties/unreach-call.prp -32 ../../sv-benchmarks/c/ldv-races/race-2_5-container_of.i
Output from witness linter:
WARNING : line 251: Thread with id 2 has already been created
WARNING : line 283: Thread with id 2 has already been created
WARNING : line 315: Thread with id 2 has already been created
WARNING : line 347: Thread with id 2 has already been created
WARNING : line 363: Thread with id 2 has already been created
WARNING : line 381: Thread with id 2 has already been created
witnesslint finished with exit code 1