The paper explores how model checking can be hybridized with trace analysis. Traces are mined to produce a categorical model of thread behavior. A heuristic for race detection is retrofitted to exploit the behavior model. With proper parameterization, the novel heuristic finds bugs 8× faster. A novel mutation-based benchmark generation process is introduced for validation.