ftsrg/theta

Witnesses get wrong programfile names when using portfolio (xcfa-cli)

Opened this issue · 0 comments

Flags to reproduce:

--input simple.c --backend portfolio --portfolio COMPLEX --loglevel RESULT --enable-output --disable-arg-generation --disable-xcfa-serialization --disable-c-serialization --property ../../../sw-verifiers/unreach-call.prp --architecture LP64

simple.c.txt
witness.graphml.txt

I am not sure if this went unnoticed on SV-COMP or if it was not present yet - the witness linter should find such issues, but it didn't.