Skip to content
This repository has been archived by the owner on Oct 3, 2021. It is now read-only.

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

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

MartinSpiessl
Copy link
Contributor

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

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

A case of #480.

@MartinSpiessl
Copy link
Contributor Author

#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).

Copy link
Contributor

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apparently, the Collatz conjecture has been proven to hold up to at least 2^68 (https://link.springer.com/article/10.1007%2Fs11227-020-03368-x).
The given benchmark implementation will mostly overflow, though, and we don't consider benchmarks with undefined behaviour for termination checks.
If we want to keep a variant of this benchmark for the termination category, we could derive a variant of the benchmark that restricts the input up to a number that doesn't overflow and set the verdict of that variant to true.

@dbeyer
Copy link
Member

dbeyer commented Sep 27, 2021

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

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
C Task in language C issue with benchmark
Development

Successfully merging this pull request may close these issues.

4 participants