Bojan- dont know where to place this. perhaps in the reviewer's comments?

As to the comment that  "I assert a problem too large for one tool
is very likely to be too large for all other tools". For the standard
set of verification engines (Salsa, NuSMV, SPIN) that may be true
but it is demonstrably NOT true when considering random search tools
like Lurch. We have conducted extensive studies of scale-up with
Lurch and have found that its memory requires scale linearly with
specification size (while SPIN's memory requirements increase
exponentially).  For example, consider the following slides show
memory and runtimes requirements for Lurch and SPIN processing
dining philisophers, n-queens, leader election, and tic tac toe.
The x-axis of these slides shows increasing problem size. For these
studies, SPIN was run in six different modes (while Lurch was run
once, using its default settings. Note the vertical dashed line in
all results- this are the largest problems SPIN can process. Note
that after SPIN fails, due to scale up, Lurch continues to find
solutions.
