* output much data, we will need to buffer it in user-space during execution.
* This also means that if ModelChecker decides not to print an execution, it
* should promptly clear the pipe.
* output much data, we will need to buffer it in user-space during execution.
* This also means that if ModelChecker decides not to print an execution, it
* should promptly clear the pipe.