./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_3.cil+token_ring.05.cil-2.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_3.cil+token_ring.05.cil-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/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.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_3.cil+token_ring.05.cil-2.c:172:3-195:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:218:3-255:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:418:3-458:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:499:3-536:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:658:3-691:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:714:3-727:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:750:3-763:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:786:3-799:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:822:3-835:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:858:3-871:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1519:3-1556: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_3.cil+token_ring.05.cil-2.c:191:5-191:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:672:9-672:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:722:5-722:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:758:5-758:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:794:5-794:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:830:5-830:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:866:5-866:15)
[Warning][Deadcode] Function 'error1' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:23:1-30:1)
[Warning][Deadcode] Function 'immediate_notify_threads' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:128:1-152:1)
[Warning][Deadcode] Function 'do_read_c' has dead code:
  on lines 225..229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:225-229)
  on line 233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:233-233)
  on lines 237..243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:237-243)
  on line 247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:247-247)
  on line 252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:252-252)
[Warning][Deadcode] Function 'error2' has dead code:
  on line 600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:600-600)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1191-1191)
  on line 1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1196-1196)
  on line 1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1201-1201)
  on line 1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1206-1206)
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1211-1211)
  on line 1216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1216-1216)
  on line 1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1221-1221)
  on line 1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1226-1226)
  on line 1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1231-1231)
  on line 1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1236-1236)
  on line 1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1241-1241)
  on line 1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1246-1246)
[Warning][Deadcode] Function 'init_threads1' has dead code:
  on line 284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:284-284)
  on line 289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:289-289)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 1008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1008-1008)
  on line 1013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1013-1013)
  on line 1018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1018-1018)
  on line 1023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1023-1023)
  on line 1028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1028-1028)
  on line 1033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1033-1033)
[Warning][Deadcode] Function 'is_do_read_c_triggered' has dead code:
  on lines 114..115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:114-115)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1259-1259)
  on line 1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1264-1264)
  on line 1269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1269-1269)
  on line 1274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1274-1274)
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1279-1279)
  on line 1284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1284-1284)
  on line 1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1289-1289)
  on line 1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1294-1294)
  on line 1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1299-1299)
  on line 1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1304-1304)
  on line 1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1309-1309)
  on line 1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1314-1314)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1413-1413)
  on line 1418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1418-1418)
  on line 1423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1423-1423)
  on line 1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1428-1428)
  on line 1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1433-1433)
  on line 1438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1438-1438)
  on line 1443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1443-1443)
  on line 1448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1448-1448)
  on line 1453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1453-1453)
  on line 1458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1458-1458)
  on line 1463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1463-1463)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 463
  dead: 70 (9 in uncalled functions)
  total lines: 533
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1519:10-1519:11)
[Warning][Deadcode][CWE-571] condition 'c_dr_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:286:7-286:24)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1085:10-1085:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:858:10-858:11)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:814:9-814:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:822:10-822:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:499:10-499:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:658:10-658:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:172:10-172:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1407:7-1407:15)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:685:17-685:29)
[Warning][Deadcode][CWE-571] condition 'fast_clk_edge == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:373:7-373:31)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1412:7-1412:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:499:10-499:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1417:7-1417:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1422:7-1422:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:750:10-750:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:706:9-706:19)
[Warning][Deadcode][CWE-570] condition 'c_dr_pc == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:210:9-210:27)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1427:7-1427:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:714:10-714:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:218:10-218:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1432:7-1432:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1190:7-1190:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1437:7-1437:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1195:7-1195:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:418:10-418:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1442:7-1442:15)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1200:7-1200:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1447:7-1447:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:822:10-822:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1205:7-1205:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:778:9-778:19)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1452:7-1452:15)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1210:7-1210:16)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1457:7-1457:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:786:10-786:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1215:7-1215:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1462:7-1462:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1005:7-1005:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1220:7-1220:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1225:7-1225:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1010:7-1010:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1230:7-1230:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:418:10-418:11)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:850:9-850:19)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1015:7-1015:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1235:7-1235:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:858:10-858:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1240:7-1240:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:218:10-218:11)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1020:7-1020:16)
[Warning][Deadcode][CWE-570] condition 'c_dr_pc == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:113:7-113:25)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1245:7-1245:15)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1025:7-1025:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1258:7-1258:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1263:7-1263:16)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:650:9-650:18)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1030:7-1030:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1268:7-1268:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:658:10-658:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1519:10-1519:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1273:7-1273:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:714:10-714:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:418:10-418:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1278:7-1278:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1283:7-1283:16)
[Warning][Deadcode][CWE-571] condition 'p_dw_pc == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:163:11-163:29)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1288:7-1288:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1293:7-1293:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1298:7-1298:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1303:7-1303:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:786:10-786:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:742:9-742:19)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1308:7-1308:15)
[Warning][Deadcode][CWE-571] condition 'p_dw_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:281:7-281:24)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:750:10-750:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.05.cil-2.c:1313:7-1313: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
