./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/pc_sfifo_2.cil-2+token_ring.05.cil-1.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/pc_sfifo_2.cil-2+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_2.cil-2+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_2.cil-2+token_ring.05.cil-1.c:147:3-165:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:188:3-219:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:347:3-387:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:427:3-449:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:555:3-576:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:599:3-612:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:635:3-648:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:671:3-684:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:707:3-720:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:743:3-756:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1404:3-1441: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] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:161:5-161:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:203:5-203:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:569:9-569:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:607:5-607:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:643:5-643:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:679:5-679:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:715:5-715:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:751:5-751:15)
[Warning][Deadcode] Function 'immediate_notify_threads' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:107:1-131:1)
[Warning][Deadcode] Function 'error1' has dead code:
  on line 29 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:29-29)
[Warning][Deadcode] Function 'error2' has dead code:
  on line 497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:497-497)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1076-1076)
  on line 1081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1081-1081)
  on line 1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1086-1086)
  on line 1091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1091-1091)
  on line 1096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1096-1096)
  on line 1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1101-1101)
  on line 1106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1106-1106)
  on line 1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1111-1111)
  on line 1116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1116-1116)
  on line 1121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1121-1121)
  on line 1126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1126-1126)
  on line 1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1131-1131)
[Warning][Deadcode] Function 'init_threads1' has dead code:
  on line 248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:248-248)
  on line 253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:253-253)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:893-893)
  on line 898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:898-898)
  on line 903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:903-903)
  on line 908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:908-908)
  on line 913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:913-913)
  on line 918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:918-918)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1144-1144)
  on line 1149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1149-1149)
  on line 1154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1154-1154)
  on line 1159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1159-1159)
  on line 1164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1164-1164)
  on line 1169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1169-1169)
  on line 1174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1174-1174)
  on line 1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1179-1179)
  on line 1184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1184-1184)
  on line 1189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1189-1189)
  on line 1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1194-1194)
  on line 1199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1199-1199)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1298-1298)
  on line 1303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1303-1303)
  on line 1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1308-1308)
  on line 1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1313-1313)
  on line 1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1318-1318)
  on line 1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1323-1323)
  on line 1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1328-1328)
  on line 1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1333-1333)
  on line 1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1338-1338)
  on line 1343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1343-1343)
  on line 1348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1348-1348)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 441
  dead: 52 (7 in uncalled functions)
  total lines: 493
[Warning][Deadcode][CWE-571] condition 'p_dw_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:245:7-245:24)
[Warning][Deadcode][CWE-571] condition 'c_dr_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:250:7-250:24)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1292:7-1292:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1297:7-1297:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:427:10-427:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1302:7-1302:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1307:7-1307:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:635:10-635:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:591:9-591:19)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1312:7-1312:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:599:10-599:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:147:10-147:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1317:7-1317:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1075:7-1075:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1322:7-1322:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:427:10-427:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1080:7-1080:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1327:7-1327:15)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1085:7-1085:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1332:7-1332:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:707:10-707:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1090:7-1090:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:663:9-663:19)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1337:7-1337:15)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1095:7-1095:16)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1342:7-1342:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:671:10-671:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1100:7-1100:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1347:7-1347:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:890:7-890:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1105:7-1105:15)
[Warning][Deadcode][CWE-571] condition 'c_dr_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:180:9-180:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:427:10-427:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1110:7-1110:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:895:7-895:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:347:10-347:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1115:7-1115:15)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:735:9-735:19)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:900:7-900:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1120:7-1120:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:743:10-743:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1125:7-1125:15)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:905:7-905:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1130:7-1130:15)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:910:7-910:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1143:7-1143:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1148:7-1148:16)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:915:7-915:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1153:7-1153:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1404:10-1404:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1158:7-1158:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:347:10-347:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:599:10-599:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1163:7-1163:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1168:7-1168:16)
[Warning][Deadcode][CWE-570] condition 'p_dw_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:357:9-357:27)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1173:7-1173:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1178:7-1178:15)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:547:9-547:18)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1183:7-1183:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1188:7-1188:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:671:10-671:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:627:9-627:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:555:10-555:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1193:7-1193:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:635:10-635:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1198:7-1198:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:1404:10-1404:11)
[Warning][Deadcode][CWE-571] condition 'p_dw_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:139:9-139:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:347:10-347:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:188:10-188:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:970:10-970:11)
[Warning][Deadcode][CWE-570] condition 'p_dw_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:357:9-357:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:743:10-743:11)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:699:9-699:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:707:10-707:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.05.cil-1.c:555:10-555:11)
[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)
