./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pc_sfifo_1.cil-1+token_ring.04.cil-1.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pc_sfifo_1.cil-1+token_ring.04.cil-1.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/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c


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


[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/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:125:3-145:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:168:3-203:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:255:3-295:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:331:3-343:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:443:3-464:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:487:3-500:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:523:3-536:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:559:3-572:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:595:3-608:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:793:3-873:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1173:3-1210:3 with factor 1
[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] cannot unassume entry of type violation_sequence
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:139:5-139:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:184:5-184:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:457:9-457:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:495:5-495:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:531:5-531:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:567:5-567:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:603:5-603:15)
[Warning][Deadcode] Function 'error1' has dead code:
  on line 28 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:28-28)
[Warning][Deadcode] Function 'error2' has dead code:
  on line 391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:391-391)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:885-885)
  on line 890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:890-890)
  on line 895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:895-895)
  on line 900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:900-900)
  on line 905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:905-905)
  on line 910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:910-910)
  on line 915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:915-915)
  on line 920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:920-920)
  on line 925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:925-925)
  on line 930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:930-930)
[Warning][Deadcode] Function 'init_threads1' has dead code:
  on line 217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:217-217)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:222-222)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:726-726)
  on line 731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:731-731)
  on line 736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:736-736)
  on line 741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:741-741)
  on line 746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:746-746)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:943-943)
  on line 948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:948-948)
  on line 953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:953-953)
  on line 958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:958-958)
  on line 963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:963-963)
  on line 968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:968-968)
  on line 973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:973-973)
  on line 978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:978-978)
  on line 983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:983-983)
  on line 988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:988-988)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1078-1078)
  on line 1083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1083-1083)
  on line 1088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1088-1088)
  on line 1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1093-1093)
  on line 1098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1098-1098)
  on line 1103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1103-1103)
  on line 1108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1108-1108)
  on line 1113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1113-1113)
  on line 1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1118-1118)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 375
  dead: 38
  total lines: 413
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:125:10-125:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:793:10-793:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:255:10-255:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1072:7-1072:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1077:7-1077:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:487:10-487:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1082:7-1082:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1087:7-1087:16)
[Warning][Deadcode][CWE-571] condition 'c_dr_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:160:9-160:27)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1092:7-1092:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1097:7-1097:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:255:10-255:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1102:7-1102:15)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:435:9-435:18)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1107:7-1107:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:723:7-723:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:559:10-559:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:515:9-515:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:443:10-443:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1112:7-1112:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:523:10-523:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1117:7-1117:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:728:7-728:16)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:733:7-733:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:884:7-884:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:889:7-889:16)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:738:7-738:16)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:587:9-587:19)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:894:7-894:16)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:743:7-743:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:899:7-899:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:595:10-595:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:168:10-168:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:904:7-904:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:909:7-909:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:914:7-914:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1173:10-1173:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:919:7-919:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:443:10-443:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:924:7-924:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:929:7-929:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:942:7-942:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:947:7-947:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:952:7-952:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:793:10-793:11)
[Warning][Deadcode][CWE-571] condition 'p_dw_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:214:7-214:24)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:957:7-957:16)
[Warning][Deadcode][CWE-571] condition 'p_dw_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:117:9-117:27)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:962:7-962:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:523:10-523:11)
[Warning][Deadcode][CWE-571] condition 'c_dr_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:219:7-219:24)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:479:9-479:19)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:967:7-967:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:1173:10-1173:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:487:10-487:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:972:7-972:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:977:7-977:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:982:7-982:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:987:7-987:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:595:10-595:11)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:551:9-551:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:255:10-255:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:559:10-559:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.04.cil-1.c:331:10-331:11)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
