keep going when the solver stops?

[regehr]

For some time, souper's default behavior has been to continue optimizing a file if the solver times out, but to abort if the solver exits for any other reason. I think perhaps this is the wrong way to do things. In a few hours of Csmith tests, Souper in integer synthesis mode successfully optimized almost zero programs because at some point, the solver would use all RAM and be stopped by the OS, and then souper would give up.

Should we have souper keep going when the solver dies? The only drawback I can think of is that this can hide bugs. For example, if we mis-print an SMTLIB query, we'll miss optmizations and see no overt symptom. It may be possible to distinguish OOM crashes from other errors, but I've played that game before and don't like it.

[chenyang78]

Probably we could first try hard to simplify the quries sent to the solver? I have a little concern about hiding bugs because I had a very bad experience on that when I did our optimization harvester stuff long time ago.

[regehr]

I agree that hiding bugs is very bad. Perhaps there is some reliable way to distinguish OOM errors. I'll think about it. Yang, I'm sure you remember from Csmith/C-Reduce how hard it can be to determine why something crashed, though here we're solving a more constrained problem.

I'm personally not interested in trying to simplify queries. Solvers such as Z3 already have very sophisticated optimizers.

We should, of course, ensure that Souper's output is not gratuitously stupid in any way.

[chenyang78]

You are right. I agree that we shouldn't put more effort on simplifying queries.