My theorem prover makes a lot of calls to random number generators. It’s definitely non-deterministic. This makes it harder to tell if a change is an improvement or not. So not trying stupid paths to a proof can make a run worse.

One needs to do a lot of runs with different seeds. Enough runs and one can vaguely invoke the central limit theorem and get an idea of a mean and standard deviation.