goblint
Stop printing solver stats after solving finishes
Another thing that I noticed a while ago, but what's relevant to the case from the issue description (where the deadlock is during warning output): We never turn off the solver stats signal, so it keeps printing even after the solver has finished and we're doing some other (long) post-processing, e.g. g2html, witnesses, or I guess just printing warnings. An obvious thing (but not complete fix) would be to actually remove the interval signaling after solving is done.
Originally posted by @sim642 in #1781
Is it not useful to have this output to see how long which part of this post-processing is taking?
That's what the timing mechanism already does anyway.
The printing of solver stats every 10s during post-processing is very misleading: it looks like we're still solving, when we're not. Especially because the solve time keeps going up (past what it actually took to solve) but none of the solver stats change. So it looks like the solver is somehow stuck, even though the post-processing might be slow as well. For example, this was often the case with GraphML witness generation.
The point is just to stop the timer signal stuff.
Another enhancement for the future might be generalizing the every 10s thing to not just solver stuff, but everything under Timing. So one could see where we are in the middle of things, rather than having to wait till the very end.
This will currently cause a problem though: Timing now has DLS (via domain_shims) in it, so it would trigger #1781. Also there's the broader issue #1550 about it.