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

Tasks in seq-mthreaded wrongly marked as non-terminating #1259

Closed tautschnig closed 3 years ago

tautschnig commented 3 years ago

786 claimed that the following tasks are non-terminating:

c/seq-mthreaded/pals_floodmax.4.2.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_floodmax.4.3.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_floodmax.4_overflow.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_floodmax.5.2.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_floodmax.5_overflow.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_lcr.6_overflow.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_lcr.7_overflow.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_lcr.8_overflow.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_opt-floodmax.4.3.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_opt-floodmax.4_overflow.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.yml c/seq-mthreaded/pals_opt-floodmax.5_overflow.ufo.UNBOUNDED.pals.yml

without citing any evidence. According to CBMC, the above are in fact terminating, and should thus have their verdicts changed.

skanav commented 3 years ago

The verdicts of these tasks seems to have been effected by the PR #1072

mchalupa commented 3 years ago

These are just variations of benchmarks reported in #1240 , so it is very likely that they are really incorrectly labeled.