Example of a concurrency witness
peterschrammel opened this issue · 2 comments
peterschrammel commented
A working example of a concurrency witness should be given. This would help reverse engineering the assumptions that the witness checker is making.
kfriedberger commented
Have you seen the example?
-> https://github.com/sosy-lab/sv-witnesses/blob/master/lazy01_false-unreach-call.i.graphml
peterschrammel commented
Thanks. Maybe move it into a separate folder as done for the termination witnesses to make it easier to find.