Fix termination verdicts in seq-mthreaded

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

Fix termination verdicts in seq-mthreaded #1260

Closed tautschnig closed 3 years ago

tautschnig commented 3 years ago

The previous verdicts were introduced in #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: #1259

skanav commented 3 years ago

Seems that the implementation of __VERIFIER_ASSUME with an abort if the condition does not hold have made the tasks terminating. Previously, the semantics of __VERIFIER_ASSUME were an infinite loop if the condition does not hold. see #1072

I have tried to execute cbmc on one of these tasks by replacing the abort in assume_abort_if_not by a while(1). cbmc produces ERROR in such a case.