Klever

Datarace detections needs MEA approach. How it is implemented in master?

Current code for VTG strategies and for scheduler do not properly work with BenchExec and needs to be rewriten to support MEA.

It doesn't need that approach since this comes with the completely specific rule specification and even very specific verification approach & tool. It just can leverage something from it like it was before, but it shouldn't do this. Taking into account that current master is absolutely free from any nonstandard verification task generation and processing techniques (#7617) and they are very far from it, I assume that Pavel will develop quite simple and straightforward approach for processing several witnesses and preparing corresponding reports to bring this high demanded rule specification to master at last. Perhaps later some parts of implementations can be combined but this also isn't very necessary.

Race detection do not use a specific verification tool - the tool is a cpachecker, and uses the same BenchExec tool-info module (cpachecker.py) as all the others instances of CPAchecker in SV-COMP (https://sv-comp.sosy-lab.org/2017/systems.php).
Race detection needs the same functionality as MEA and suffers from the same problems described in #7877

Nevertheless Pavel will add specific support for finding data races in several days. All considerable improvements will be made just in several months or even years.

I don't think that another crutch is the right way to go