Regression in concurrency analyis due to replacement of __VERIFIER_error
Our concurrency analysis for SV-COMP (which uses BDDs) produces several wrong proofs since __VERIFIER_error
was replaced with a different function.
Regression table: https://buildbot.sosy-lab.org/cpachecker/results/nightly-sv-comp/00142.nightly-sv-comp.diff.html
Example:
scripts/cpa.sh -timelimit 900s -svcomp20 -32 -spec test/programs/benchmarks/properties/unreach-call.prp test/programs/benchmarks/pthread/lazy01.i
The relevant change is sosy-lab/software/sv-benchmarks@e3f389a61aea5fc43e1d8380ef15cd405269f887. It replaces calls to __VERIFIER_error
with a call to an empty function named reach_error
and a call to abort
. Maybe the problem is that we now match a function entry instead of an extern function call, or the additional abort
.