This was a debugging hack to deal with #32. But we need a better solution because the current hack leaves BENCHMARK TIMEOUTS NOT WORKING.
