To me this 'problem' of reproducibility from time-outs had been 'solved' in many static analysis tools or solvers, with an actual 'steps' counter or some form of tuneable constant-across-runs metric... one way to do it anyway.