When executing (as opposed to model checking) programs, DIVINE can currently record system call traces. During model checking, then, it can load these traces back and play them back to the program. However, currently only executions that exactly correspond to the system call trace can be explored by the model checker. The overall goal of this thesis is to make the model checker more flexible with respect to the recorded trace. The first possible improvement is that certain system calls commute, that is, the observed effects of two such system calls do not depend on their order. The linear order of the trace can therefore be changed to a partial order, increasing the number of executions available for exploration. A different approach is increasing coverage by introducing non-deterministic mutations into the traces -- an approach similar to fuzzing: an established and successful technique. Finally, it is also possible to use symbolic methods to represent key locations in the trace, improving the coverage further.