./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.05.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.05.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.05.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.05.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.05.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.05.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.05.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.05.cil-1.c:449:3-470:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:493:3-506:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:529:3-542:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:565:3-578:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:601:3-614:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:637:3-650:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1298:3-1335: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.05.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.05.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.05.cil-1.c:463:9-463:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:501:5-501:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:537:5-537:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:573:5-573:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:609:5-609:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:645:5-645: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.05.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.05.cil-1.c:391-391)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:970-970)
  on line 975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:975-975)
  on line 980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:980-980)
  on line 985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:985-985)
  on line 990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:990-990)
  on line 995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:995-995)
  on line 1000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1000-1000)
  on line 1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1005-1005)
  on line 1010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1010-1010)
  on line 1015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1015-1015)
  on line 1020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1020-1020)
  on line 1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1025-1025)
[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.05.cil-1.c:217-217)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:222-222)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:787-787)
  on line 792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:792-792)
  on line 797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:797-797)
  on line 802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:802-802)
  on line 807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:807-807)
  on line 812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:812-812)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1038-1038)
  on line 1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1043-1043)
  on line 1048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1048-1048)
  on line 1053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1053-1053)
  on line 1058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1058-1058)
  on line 1063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1063-1063)
  on line 1068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1068-1068)
  on line 1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1073-1073)
  on line 1078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1078-1078)
  on line 1083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1083-1083)
  on line 1088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1088-1088)
  on line 1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1093-1093)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1192-1192)
  on line 1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1197-1197)
  on line 1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1202-1202)
  on line 1207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1207-1207)
  on line 1212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1212-1212)
  on line 1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1217-1217)
  on line 1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1222-1222)
  on line 1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1227-1227)
  on line 1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1232-1232)
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1237-1237)
  on line 1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1242-1242)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 411
  dead: 45
  total lines: 456
[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.05.cil-1.c:637:10-637:11)
[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.05.cil-1.c:1019:7-1019: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.05.cil-1.c:125:10-125:11)
[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.05.cil-1.c:799:7-799: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.05.cil-1.c:255:10-255:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1024:7-1024:15)
[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.05.cil-1.c:804:7-804:16)
[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.05.cil-1.c:1037:7-1037: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.05.cil-1.c:1042:7-1042:16)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:809:7-809: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.05.cil-1.c:1047:7-1047: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.05.cil-1.c:1298:10-1298: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.05.cil-1.c:1052:7-1052: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.05.cil-1.c:493:10-493:11)
[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.05.cil-1.c:1057:7-1057:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1062:7-1062: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.05.cil-1.c:160:9-160:27)
[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.05.cil-1.c:1067:7-1067:15)
[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.05.cil-1.c:1072:7-1072: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.05.cil-1.c:255:10-255:11)
[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.05.cil-1.c:441:9-441: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.05.cil-1.c:1077:7-1077: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.05.cil-1.c:1082:7-1082: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.05.cil-1.c:565:10-565: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.05.cil-1.c:521:9-521: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.05.cil-1.c:449:10-449: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.05.cil-1.c:1087:7-1087: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.05.cil-1.c:529:10-529:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1092:7-1092: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.05.cil-1.c:1298:10-1298: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.05.cil-1.c:864:10-864: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.05.cil-1.c:637:10-637:11)
[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.05.cil-1.c:593:9-593: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.05.cil-1.c:601:10-601: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.05.cil-1.c:168:10-168: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.05.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.05.cil-1.c:449:10-449: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.05.cil-1.c:331:10-331: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.05.cil-1.c:1186:7-1186: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.05.cil-1.c:1191:7-1191:16)
[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.05.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.05.cil-1.c:331:10-331:11)
[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.05.cil-1.c:117:9-117:27)
[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.05.cil-1.c:1196:7-1196: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.05.cil-1.c:529:10-529: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.05.cil-1.c:219:7-219:24)
[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.05.cil-1.c:1201:7-1201:16)
[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.05.cil-1.c:485:9-485:19)
[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.05.cil-1.c:1206:7-1206: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.05.cil-1.c:493:10-493: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.05.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1211:7-1211: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.05.cil-1.c:969:7-969:15)
[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.05.cil-1.c:1216:7-1216: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.05.cil-1.c:974:7-974:16)
[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.05.cil-1.c:1221:7-1221: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.05.cil-1.c:331:10-331:11)
[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.05.cil-1.c:979:7-979:16)
[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.05.cil-1.c:1226:7-1226: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.05.cil-1.c:601:10-601:11)
[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.05.cil-1.c:984:7-984:16)
[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.05.cil-1.c:557:9-557: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.05.cil-1.c:255:10-255: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.05.cil-1.c:1231:7-1231:15)
[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.05.cil-1.c:989:7-989:16)
[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.05.cil-1.c:1236:7-1236: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.05.cil-1.c:565:10-565: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.05.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:994:7-994:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:1241:7-1241: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.05.cil-1.c:784:7-784:15)
[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.05.cil-1.c:999:7-999: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.05.cil-1.c:1004:7-1004: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.05.cil-1.c:789:7-789:16)
[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.05.cil-1.c:1009:7-1009:15)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-1+token_ring.05.cil-1.c:629:9-629:19)
[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.05.cil-1.c:794:7-794: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.05.cil-1.c:331:10-331: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.05.cil-1.c:1014:7-1014:15)
[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
