Description
Hello,
I have noticed a strange (pathological) behaviour in total runtime of certain tests. This was the result of investigating some of the issues that the runner check-ubuntu-20_04-cmake-gcc-THOROUGH is currently experiencing.
I am currently unsure as to what's currently plugging that runner and it completely timeouts (is killed by Github after spending more than 6hrs running tests).
However, it appears that some tests, even though marked THOROUGH, are spending a ludicrous amount of time to run, both locally and in CI. We could try to either debug them/profile them and fix CBMC, or deactivate them (temporarily?) in an attempt to bring the runtime back within an acceptable threshold.
One test that demonstrates this behaviour is regression/cbmc/gcc_popcount2, which appears to be needing somewhere around 1500 seconds to run, both on CI and locally (that is, on an M1 Max). Another one is the jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix, which also takes more than 1300 seconds on CI.
CBMC version: develop
Operating system: macOS or Linux (reproducible on both)
Exact command line resulting in the issue: cd build && ctest . -V -L THOROUGH -j4
What behaviour did you expect: The tests run in a reasonable amount of time.
What happened instead: The tests run in a ludicrous amount of time.