Implement counterexample reduction to the model's main test program. If running a test results in finding a bug, the test program should automatically find the smallest possible workload that reproduces it to make the subsequent debugging easier.