Possible soundness issue with Runner timeout

[jrmcclurg]

Hello! I'm running into interesting behavior when I create a Runner with a very short timeout (say 200 microseconds) and a large number of rules.

It tells me Saturated, and I extract the minimal expression, but if I increase the timeout (say to 400 microseconds), I again get Saturated with a smaller minimal expression. Unless I'm misunderstanding saturation, this behavior would seem to mean that the initial Saturated status was incorrect.

I think the source of this issue is the break statements inside run_one:
https://github.com/egraphs-good/egg/blob/master/src/run.rs#L423
https://github.com/egraphs-good/egg/blob/master/src/run.rs#L452
With a short timeout, these prevent the loop(s) from iterating through all the rules, meaning applied may be empty, even though there could be further work to do. The empty applied causes run_one to give a Saturated result.

As a temporary fix, does it make sense to just comment out those two breaks? This will allow the runner to exceed the limits, but only by one "iteration".

Maybe a better fix would be to change the two checks of the form

if self.check_limits().is_err()
    break;
}

to something like

result = result.and(self.check_limits());
if result.is_err() {
    break;
}

(where result is initially Ok(())), and then run_one could return result if its an Err? This approach is what I'm doing right now, and it seems to be working.

Let me know if I'm completely missing something here. Otherwise, I can create a pull request for the above, if it would help!

[mwillsey]

great catch! Fixing now :)