There exist no sound, scalable methods to assemble comprehensive datasets of concurrent programs annotated with data races.
As a consequence, it is unclear how well the multiple heuristics and SMT-based algorithms, that have been proposed over the last three decades to detect data races, perform.
To address this problem, we propose \sys—an SMT-based approach which, for any given program, creates arbitrarily many program traces of it containing injected data races.
The injected races are guaranteed to follow the given program's semantics.
{\sys} hence can produce an arbitrarily large, labeled benchmark which is independent of how detection algorithms work.
We demonstrate {\sys} by injecting races into popular program benchmarks and generating a small dataset of traces with races in them.
Among the traces {\sys} generates, we begin to find counterexamples which four state-of-the-art race detection algorithms fail to detect.
We thus demonstrate the utility of generating such datasets, and recommend using them to train machine learning-based models which can potentially replace and improve upon existing race-detection heuristics.