The thread join support from PR #137 didn't improve our results on SV-COMP's NoDataRace benchmarks as much as expected. At least some of them create and join threads conditionally. This currently renders the added thread join support useless because joins in the thread analyses lose the necessary precision. Making threadflag and maybe even thread analysis path-sensitive would help with that.

I made a quick experiment but turns out this is problematic and cannot currently easily be done. The issue is the S.context d call here:

If d is a path-sensitivity domain set that happens to contain more than one path, then S.context fails because it can just return a single context. It might be necessary to rework this mechanism to be more like our previous function call mechanism where enter returns a list, not a single element, which is then handled in FromSpec to apply S.context per-element.
(That in itself is a weird mechanism because the path-sensitivity handling isn't localized to the corresponding lifter but throughout the analysis specification hierarchy.)

I have my doubts about being able to achieve this by SV-COMP 2021.