The model's main program performs counterexample reduction when it discovers a mismatch between WiredTiger and the model by selectively removing ranges of operations from the workload to see if it still fails. This has, however, an unfortunate effect of producing inherently illegal operation sequences—and thus useless reduced counterexamples because they fail due to the illegal sequences instead of the actual problems.

For example, consider this sequence:

set_stable_timestamp(100)
set_oldest_timestamp(100)
set_stable_timestamp(300)
set_oldest_timestamp(200)

Now let's say the algorithm removes the second set_stable_timestamp operation.

set_stable_timestamp(100)
set_oldest_timestamp(100)
set_oldest_timestamp(200)

As a result, the workload now fails due to the oldest timestamp racing ahead of the stable timestamp instead of the other problem that we were hoping to fix.

Unfortunately this seems to be a difficult issue, because timestamps are affected not only by set_stable_timestamp and set_oldest_timestamp, but also by checkpoint, crash, and restart.