BAM (LDV BAM) performs unsound analysis
For cil.i with:
scripts/cpa.sh -setprop parser.readLineDirectives=true -setprop counterexample.export.extendedWitnessFile=witness.%d.graphml -setprop counterexample.export.exportExtendedWitness=true -setprop counterexample.export.compressWitness=false -setprop cpa.arg.witness.exportSourcecode=true -setprop cpa.arg.witness.removeInsufficientEdges=false -heap 2400m -ldv-bam -setprop analysis.machineModel=LINUX64 -setprop coverage.file=coverage.info -stats -spec test/programs/benchmarks/properties/unreach-call.prp cil.i
there is true although, say, with -predicateAnalysis-bam-rec
and -valueAnalysis-bam-rec
there is false as expected.