search

sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

Remove property for task with undefined behavior (Collatz.yml) #1299

Open MartinSpiessl opened 3 years ago

MartinSpiessl commented 3 years ago

This task contains an overflow, so stating the termination property makes no sense, especially since no verdict is given.

PhilippWendler commented 3 years ago

A case of #480.

MartinSpiessl commented 3 years ago

480 is related, but Collatz.yml is the only one I found in my experiments with the SV-COMP21 results that has the property without an expected verdict, so I would like to at least fix this such that there is no task without expected verdict in SV-COMP.

480 is about tasks that have other properties (with expected verdict).

dbeyer commented 2 years ago

I like the suggestion to add a new task with a bound. Would you be willing to add it @peterschrammel ? (in another pull request?)