SVCOMP-benchmark incorrect (valid-deref)

[xbauch]

Reporting on one SVCOMP benchmarks that were working in previous versions (5.8) but CBMC give incorrect result now. The benchmark code is here:

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/memsafety/test-0521_true-valid-memsafety.c

CBMC version: 5.10
Operating system: 64-bit linux
Exact command line resulting in the issue: ./cbmc --graphml-witness witness.graphml --32 --propertyfile ../sv-benchmarks/c/MemSafety.prp ../sv-benchmarks/c/memsafety/test-0521_true-valid-memsafety.i
What behaviour did you expect:

VERIFICATION SUCCESSFUL
EC=42
UNKNOWN

What happened instead:

Violated property:
file ../sv-benchmarks/c/memsafety/test-0521_true-valid-memsafety.i line 715 function main
dereference failure: dead object in *pdst
!(POINTER_OBJECT(pdst) == POINTER_OBJECT(__CPROVER_dead_object))

VERIFICATION FAILED
EC=10
FALSE(valid-deref)

[tautschnig]

I believe either #1996 or #2000 might fix this.

[xbauch]

The benchmark: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-memsafety/memleaks_test3_false-valid-free.i

results in:

Violated property:
file ../sv-benchmarks/c/ldv-memsafety/memleaks_test3_false-valid-free.i function entry_point line 1440 thread 0
free argument must be dynamic object
(void *)p == NULL || DYNAMIC_OBJECT((void *)p)

VERIFICATION FAILED
EC=10
FALSE(valid-deref)

where 5.8 resulted in:

Violated property:
file ../sv-benchmarks/c/ldv-memsafety/memleaks_test3_false-valid-free.i line 1440 function entry_point
free argument must be dynamic object
(void *)p == 0 || DYNAMIC_OBJECT((void *)p)

VERIFICATION FAILED
EC=10
FALSE(valid-free)

[xbauch]

The benchmark: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/memsafety-ext3/freeAlloca_false-valid-free.c

results in:

Violated property:
file ../sv-benchmarks/c/memsafety-ext3/freeAlloca_false-valid-free.c function main line 9 thread 0
dereference failure: pointer NULL in p[i]
!(POINTER_OBJECT(p) == POINTER_OBJECT(((char *)NULL)))

VERIFICATION FAILED
EC=10
FALSE(valid-deref)

I'm not sure what the previous result was. The correct result would be "FALSE(valid-free)".

[TGWDB]

Closing as the benchmarks are no longer available and so cannot reproduce. Please reopen if you believe this is erroneous/with a link to an appropriate example.