Zvonimir Rakamaric

I totally agree with @ccadar. I think that such text would be useful to have in the rules.

Wait, I am lost here. Are few busy box benchmarks going to be worth the same as thousands of device driver benchmarks? Is that what will happen if categories remain...

In this category this is crazy pronounced. Rechability error can easily be a security vulnerability (depending on what the assertion encodes), so that is a flawed argument for how "important"...

Anyhow, enough said. Given that we decided to freeze the categories, maybe we should not make any changes at this point.

Just read this. Personally, I like the idea of using target triplets.

Just to clarify, you are not suggesting that we add additional properties to check (such as undefined behaviors that are currently not specified/caught as SV-COMP properties), but rather only to...

Absolutely! That would be super valuable for a demo category and next year as well!

What do you think @tautschnig?

Given that the deadline has passed, I am of the opinion that all benchmarks with open issues should be moved into the todo folder and discussed after the competition. Otherwise,...

I support moving such benchmarks into the BitVectorsReach category, as you suggested. I could be wrong, but I think you could leave those files in their original folders, but just...