When Lincheck finds an error via stress testing, it could run a model-checking test in the hope of reproducing the bug and, this way, provide a trace of the error. We can fix the number of invocations for this model checking test to some big constant, e.g., 10000.
When Lincheck finds an error via stress testing, it could run a model-checking test in the hope of reproducing the bug and, this way, provide a trace of the error. We can fix the number of invocations for this model checking test to some big constant, e.g.,
10000.