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

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

Closed
tautschnig opened this issue Dec 6, 2020 · 2 comments · Fixed by #1260
Closed

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

tautschnig opened this issue Dec 6, 2020 · 2 comments · Fixed by #1260
Labels
C Task in language C issue with benchmark

Comments

@tautschnig
Copy link
Contributor

#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.
@tautschnig tautschnig added C Task in language C issue with benchmark labels Dec 6, 2020
tautschnig added a commit to tautschnig/sv-benchmarks that referenced this issue Dec 6, 2020
@tautschnig
Fix termination verdicts in seq-mthreaded
849f857 
The previous verdicts were introduced in sosy-lab#786 without any evidence. CBMC
reports these tasks to be terminating, see
https://sv-comp.sosy-lab.org/2021/results/results-verified/cbmc.2020-12-05_12-30-28.results.SV-COMP21_termination.Termination-Other.xml.bz2.merged.xml.bz2.table.html#/table?filter=0(0*status*(category(in(wrong)))).

Fixes: sosy-lab#1259
@tautschnig tautschnig mentioned this issue Dec 6, 2020
Merged
tautschnig added a commit to tautschnig/sv-benchmarks that referenced this issue Dec 6, 2020
@tautschnig
Remove termination verdicts from disputed seq-mthreaded tasks
1d2113c 
See sosy-lab#1259 and sosy-lab#1260.
@tautschnig tautschnig mentioned this issue Dec 6, 2020
Merged
tautschnig added a commit to tautschnig/sv-benchmarks that referenced this issue Dec 7, 2020
@tautschnig
Remove termination verdicts from disputed seq-mthreaded tasks
76a9077 
See sosy-lab#1259 and sosy-lab#1260.
@skanav
Copy link
Contributor

skanav commented Dec 9, 2020

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

@mchalupa
Copy link
Contributor

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

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

Successfully merging a pull request may close this issue.

Fix termination verdicts in seq-mthreaded tautschnig/sv-benchmarks
3 participants
@tautschnig @mchalupa @skanav