Simmo Saan
Simmo Saan
Hmm, the cputime plot is odd: just using more jobs (with either HTML generation) uses less CPU time. And this is not only CPU time measured by Goblint's own timing,...
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...
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...
I fixed it directly on master now.
I tried just hard-coding it to 100 to see what happens, but just doing that loses points. It seems that by allowing more globals to be picked, the cost in...
Yeah, that's a good idea. I now did that and the diff table is here: https://goblint.cs.ut.ee/results/275-all-autotune-globals-100-2/table-generator-cmp.diff.html#/. The summary is: 1. 13 `true`s turned into `TIMEOUT`/`OUT OF MEMORY`: some LDV ones...
Oh, I never realized that `Ctrl+o` is different from all the other things like `Shift+o`, `t`, `gh`, etc. All of the latter, including the other similar-looking open interface of `Shift+o`,...
> What would you propose instead of `top`? Raising deadcode? These seem to be the only sensible things we can do. I haven't yet thought about what exactly this is...