Weird behavior in goblint-coreutils, SV-Benchmarks

Hi, I was looking at CPAChecker's scalability and precision on the goblint-coreutils benchmarks. I think I found a weird behavior in c/goblint-coreutils/instrumented_dd_comb.i with property unreach-call.prp. On the original program, the verification result is TRUE.

However, when I add reach_error calls in (what I think are) reachable parts of the program, the verification result is still TRUE. Attached is the patched file, with only two reach_errors added (on in main just after install_signal_handlers, one early in install_signal_handlers). I have the impression the { if(!(stdlib_allocator.die == 0)) { reach_error(); abort(); } }; is the culprit.

Command used

$ ./bin/cpachecker --svcomp26 --heap 10000M  --timelimit '900 s' --stats --spec ~/work/sv-benchmarks/c/properties/unreach-call.prp --64 ~/work/sv-benchmarks/c/goblint-coreutils/instrumented_dd_comb.i

$ ./bin/cpachecker --version
CPAchecker 4.1-693-g7a3415e5c6 (OpenJDK 64-Bit Server VM 21.0.8)