While debugging some benchmark programs, I noticed they themselves contain silly bugs:

1. Forgetting to unlock a mutex (e.g. at early return), which makes any following call of the function deadlock or undefined behavior: https://github.com/goblint/bench/blob/16ee6e2dfa54881be2161cb5bb6eee8cce5736d7/pthread/pfscan_comb.c#L1234-L1237.
2. Unlocking a mutex, which isn't held, which is undefined behavior, e.g. forgetting to relock at the end of a loop for protected condition check: https://github.com/goblint/bench/blob/16ee6e2dfa54881be2161cb5bb6eee8cce5736d7/pthread/smtprc_comb.c#L2379-L2386. MayLock Analysis & Sanity Checks of Mutex Usage & Analysis of Mutex Types #839
3. Re-initializing a locked mutex.

At least in the case of non-recursive mutexes, these issues and other similar ones might be useful to have some simple analysis for to warn about.