SVCOMP-benchmark wrong proof in Device Drivers

[xbauch]

Probably the worst incorrectness: CBMC marks this benchmark as "true", where it probably shouldn't be.

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--misc--legousbtower.ko_false-unreach-call.cil.c

CBMC version: 5.10
Operating system: 64-bit linux
Exact command line resulting in the issue: ./cbmc --graphml-witness witness.graphml --64 --propertyfile ../../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--misc--legousbtower.ko_false-unreach-call.cil.c
What behaviour did you expect: VERIFICATION FAILED
What happened instead:

VERIFICATION SUCCESSFUL
EC=0
TRUE

[TGWDB]

Closing as the benchmarks are no longer available and it is unclear if this can be reproduced. Please reopen if you believe this is erroneous/if you can show a current example.