Missing Counterexample when using `ldv-bam`
@enovikov reports that CPAchecker_files
with configuration -ldv-bam
does not produce a valid counterexample.
CPAchecker prints the following warning at the end of analysis:
could not compute full reached set graph (missing block), some output or statistics might be missing (BAMCPA:BAMARGStatistics.createReachedSetView, INFO)
Command-line used:
scripts/cpa.sh -ldv-bam -spec safe-prps.prp cil.i
(with the files from the archive above)