But this seems like a reasonable approach for reverse-engineering, and it seems the bug they found is real.

The code was inconsistent with itself: that's not circular. Every path dropped the lock except one.

I took it as the extracted spec was weird and they looked into it.