Develop new test suite based on patches accepted by Linux kernel developers
Klever find a lot of tricky and severe bugs in different programs with help of CPAchecker. Developers accept most of corresponding bug reports and patches. This is a great source of extremely valuable verification tasks. Any degradation for these tasks is awful.
There is a very old feature request that suggested to add such the test suite for Klever. This is a preliminary step before implementing the given task.