3. The system of claim 1 , wherein the concurrency bug comprises a data race, and wherein the trace property comprises a conflicting operation pair of events from different threads being executed in succession.
4. The system of claim 3 , wherein the formula encodes all feasible traces corresponding to each respective of a plurality of data races.