Also, should we maybe make an issue for the improved autotuner (or ask AI to fix the autotuner right away)?
I'll open a separate issue about it because unlike the existing single-threaded SV-COMP autotuner, this is more aggressive and requires a bit more care. This can become unsound if there are other things which we also treat as thread-like (signal handlers, atexit, etc.). Not sure if any of those are covered by sv-benchmarks though.
And improvements like #1965 which change our approach to thread-like things (e.g. making them non-threads in some sense, but not other) can lead to new problematic interactions.
I'd like to have it for SV-COMP 2027 and it's easy to do closer to it happening. I want to see where we can get with the signal handlers (like #1966) before needing to worry about the SV-COMP interactions.
Originally posted by @sim642 in #1981 (comment)
This requires #1981 to be merged first.
I'll open a separate issue about it because unlike the existing single-threaded SV-COMP autotuner, this is more aggressive and requires a bit more care. This can become unsound if there are other things which we also treat as thread-like (signal handlers,
atexit, etc.). Not sure if any of those are covered by sv-benchmarks though.And improvements like #1965 which change our approach to thread-like things (e.g. making them non-threads in some sense, but not other) can lead to new problematic interactions.
I'd like to have it for SV-COMP 2027 and it's easy to do closer to it happening. I want to see where we can get with the signal handlers (like #1966) before needing to worry about the SV-COMP interactions.
Originally posted by @sim642 in #1981 (comment)
This requires #1981 to be merged first.