./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-2+token_ring.08.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_1.cil-2+token_ring.08.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_1.cil-2+token_ring.08.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_1.cil-2+token_ring.08.cil-2.c:125:3-145:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:168:3-203:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:255:3-295:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:331:3-343:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:467:3-500:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:523:3-536:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:559:3-572:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:595:3-608:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:631:3-644:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:667:3-680:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:703:3-716:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:739:3-752:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:775:3-788:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1685:3-1722: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-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.c:481:9-481:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.c:603:5-603:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:639:5-639:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:675:5-675:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:711:5-711:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:747:5-747:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:783:5-783:15)
[Warning][Deadcode] Function 'error1' has dead code:
  on line 28 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.c:391-391)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1237-1237)
  on line 1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1242-1242)
  on line 1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1247-1247)
  on line 1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1252-1252)
  on line 1257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1257-1257)
  on line 1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1262-1262)
  on line 1267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1267-1267)
  on line 1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1272-1272)
  on line 1277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1277-1277)
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1282-1282)
  on line 1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1287-1287)
  on line 1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1292-1292)
  on line 1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1297-1297)
  on line 1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1302-1302)
  on line 1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1307-1307)
  on line 1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1312-1312)
  on line 1317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1317-1317)
  on line 1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1322-1322)
[Warning][Deadcode] Function 'init_threads1' has dead code:
  on line 217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:217-217)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:222-222)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:982-982)
  on line 987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:987-987)
  on line 992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:992-992)
  on line 997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:997-997)
  on line 1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1002-1002)
  on line 1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1007-1007)
  on line 1012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1012-1012)
  on line 1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1017-1017)
  on line 1022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1022-1022)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1335-1335)
  on line 1340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1340-1340)
  on line 1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1345-1345)
  on line 1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1350-1350)
  on line 1355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1355-1355)
  on line 1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1360-1360)
  on line 1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1365-1365)
  on line 1370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1370-1370)
  on line 1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1375-1375)
  on line 1380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1380-1380)
  on line 1385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1385-1385)
  on line 1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1390-1390)
  on line 1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1395-1395)
  on line 1400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1400-1400)
  on line 1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1405-1405)
  on line 1410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1410-1410)
  on line 1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1415-1415)
  on line 1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1420-1420)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1546-1546)
  on line 1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1551-1551)
  on line 1556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1556-1556)
  on line 1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1561-1561)
  on line 1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1566-1566)
  on line 1571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1571-1571)
  on line 1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1576-1576)
  on line 1581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1581-1581)
  on line 1586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1586-1586)
  on line 1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1591-1591)
  on line 1596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1596-1596)
  on line 1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1601-1601)
  on line 1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1606-1606)
  on line 1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1611-1611)
  on line 1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1616-1616)
  on line 1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1621-1621)
  on line 1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1626-1626)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 525
  dead: 66
  total lines: 591
[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-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.c:1685:10-1685:11)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:659:9-659: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-2+token_ring.08.cil-2.c:667:10-667:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1236:7-1236:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1241:7-1241: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-2+token_ring.08.cil-2.c:255:10-255:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1246:7-1246: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-2+token_ring.08.cil-2.c:775:10-775:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1251:7-1251:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1256:7-1256: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-2+token_ring.08.cil-2.c:1685:10-1685:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1261:7-1261: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-2+token_ring.08.cil-2.c:523:10-523:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1266:7-1266:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1271:7-1271:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1276:7-1276:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1281:7-1281:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1286:7-1286:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1291:7-1291:15)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:551:9-551:19)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1296:7-1296: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-2+token_ring.08.cil-2.c:559:10-559:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1301:7-1301:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1306:7-1306: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-2+token_ring.08.cil-2.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1311:7-1311:15)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1316:7-1316: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-2+token_ring.08.cil-2.c:667:10-667:11)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1321:7-1321: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-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.c:1334:7-1334:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1339:7-1339: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-2+token_ring.08.cil-2.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1344:7-1344:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1349:7-1349:16)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:695:9-695:19)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1354:7-1354: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-2+token_ring.08.cil-2.c:117:9-117:27)
[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-2+token_ring.08.cil-2.c:703:10-703: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-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.c:1359:7-1359:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1364:7-1364:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1369:7-1369: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-2+token_ring.08.cil-2.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1374:7-1374:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1379:7-1379:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1384:7-1384: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-2+token_ring.08.cil-2.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1389:7-1389: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-2+token_ring.08.cil-2.c:559:10-559:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1394:7-1394:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1399:7-1399:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:979:7-979:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1404:7-1404: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-2+token_ring.08.cil-2.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1409:7-1409:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:984:7-984:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1414:7-1414:15)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:587:9-587:19)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1419:7-1419:15)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:989:7-989: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-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.c:994:7-994:16)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:999:7-999: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-2+token_ring.08.cil-2.c:703:10-703:11)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1004:7-1004:16)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1009:7-1009:16)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1014:7-1014: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-2+token_ring.08.cil-2.c:160:9-160:27)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1019:7-1019:16)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:459:9-459:18)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:731:9-731: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-2+token_ring.08.cil-2.c:467:10-467: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-2+token_ring.08.cil-2.c:739:10-739: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-2+token_ring.08.cil-2.c:595:10-595:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1540:7-1540: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-2+token_ring.08.cil-2.c:168:10-168:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1545:7-1545:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1550:7-1550:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1555:7-1555:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1560:7-1560:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1565:7-1565:16)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:623:9-623:19)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1570:7-1570: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-2+token_ring.08.cil-2.c:631:10-631:11)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1575:7-1575: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-2+token_ring.08.cil-2.c:1089:10-1089:11)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1580:7-1580:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1585:7-1585: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-2+token_ring.08.cil-2.c:467:10-467:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1590:7-1590: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-2+token_ring.08.cil-2.c:739:10-739: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-2+token_ring.08.cil-2.c:214:7-214:24)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1595:7-1595:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1600:7-1600:15)
[Warning][Deadcode][CWE-571] condition 'c_dr_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:219:7-219:24)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1605:7-1605:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1610:7-1610:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1615:7-1615:15)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:494:17-494:29)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:767:9-767:19)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1620:7-1620:15)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.c:1625:7-1625: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-2+token_ring.08.cil-2.c:775:10-775: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-2+token_ring.08.cil-2.c:255:10-255:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.08.cil-2.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-2+token_ring.08.cil-2.c:523:10-523: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-2+token_ring.08.cil-2.c:631:10-631: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
