./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/sll-queue-2.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/sll-queue-2.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1024:3-1024:70 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1025:3-1025:70 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1028:2-1028:69 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1031:3-1031:70 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1032:3-1032:76 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1036:3-1036:70 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1037:3-1037:76 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1038:3-1038:82 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1042:3-1042:70 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1043:3-1043:76 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1044:3-1044:82 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1045:3-1045:88 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1046:3-1046:85 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1053:3-1053:77 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1058:2-1063:2 with factor 8
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1006:3-1006:26)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1020:4-1020:18)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1015:4-1015:18)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1010:4-1010:18)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1038:12-1038:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1044:12-1044:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1045:12-1045:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1046:12-1046:48)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 46
  dead: 0
  total lines: 46
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1031:68-1031:70)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1038:80-1038:82)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1045:86-1045:88)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )head != (unsigned long )((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1028:11-1028:32)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1028:67-1028:69)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1037:74-1037:76)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1044:80-1044:82)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:985:73-985:74)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )head != (unsigned long )((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1036:12-1036:33)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1025:68-1025:70)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1036:68-1036:70)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1043:74-1043:76)
[Warning][Deadcode][CWE-571] condition 'item->data > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1053:12-1053:40)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1053:75-1053:77)
[Warning][Deadcode][CWE-571] condition 'head' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1058:8-1058:12)
[Warning][Deadcode][CWE-571] condition 'status >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1018:12-1018:23)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )head != (unsigned long )((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1024:12-1024:33)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1024:68-1024:70)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )head != (unsigned long )((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1042:12-1042:33)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1032:74-1032:76)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1042:68-1042:70)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1046:83-1046:85)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )head != (unsigned long )((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-2.i:1031:12-1031:33)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
