./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pc_sfifo_2.cil-2+token_ring.11.cil-2.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pc_sfifo_2.cil-2+token_ring.11.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_2.cil-2+token_ring.11.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_2.cil-2+token_ring.11.cil-2.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.11.cil-2.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.11.cil-2.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.11.cil-2.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.11.cil-2.c:591:3-612:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.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.11.cil-2.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.11.cil-2.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.11.cil-2.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.11.cil-2.c:779:3-792:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:815:3-828:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:851:3-864:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:887:3-900:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:923:3-936:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:959:3-972:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:995:3-1008:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2154:3-2191: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_2.cil-2+token_ring.11.cil-2.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.11.cil-2.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.11.cil-2.c:605:9-605:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.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.11.cil-2.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.11.cil-2.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.11.cil-2.c:751:5-751:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:787:5-787:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:823:5-823:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:859:5-859:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:895:5-895:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:931:5-931:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:967:5-967:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1003:5-1003: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.11.cil-2.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.11.cil-2.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.11.cil-2.c:497-497)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1586-1586)
  on line 1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1591-1591)
  on line 1596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1596-1596)
  on line 1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1601-1601)
  on line 1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1606-1606)
  on line 1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1611-1611)
  on line 1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1616-1616)
  on line 1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1621-1621)
  on line 1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1626-1626)
  on line 1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1631-1631)
  on line 1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1636-1636)
  on line 1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1641-1641)
  on line 1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1646-1646)
  on line 1651 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1651-1651)
  on line 1656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1656-1656)
  on line 1661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1661-1661)
  on line 1666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1666-1666)
  on line 1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1671-1671)
  on line 1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1676-1676)
  on line 1681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1681-1681)
  on line 1686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1686-1686)
  on line 1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1691-1691)
  on line 1696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1696-1696)
  on line 1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1701-1701)
[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.11.cil-2.c:248-248)
  on line 253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:253-253)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 1259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1259-1259)
  on line 1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1264-1264)
  on line 1269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1269-1269)
  on line 1274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1274-1274)
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1279-1279)
  on line 1284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1284-1284)
  on line 1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1289-1289)
  on line 1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1294-1294)
  on line 1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1299-1299)
  on line 1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1304-1304)
  on line 1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1309-1309)
  on line 1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1314-1314)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1714-1714)
  on line 1719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1719-1719)
  on line 1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1724-1724)
  on line 1729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1729-1729)
  on line 1734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1734-1734)
  on line 1739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1739-1739)
  on line 1744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1744-1744)
  on line 1749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1749-1749)
  on line 1754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1754-1754)
  on line 1759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1759-1759)
  on line 1764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1764-1764)
  on line 1769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1769-1769)
  on line 1774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1774-1774)
  on line 1779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1779-1779)
  on line 1784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1784-1784)
  on line 1789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1789-1789)
  on line 1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1794-1794)
  on line 1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1799-1799)
  on line 1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1804-1804)
  on line 1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1809-1809)
  on line 1814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1814-1814)
  on line 1819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1819-1819)
  on line 1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1824-1824)
  on line 1829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1829-1829)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1982-1982)
  on line 1987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1987-1987)
  on line 1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1992-1992)
  on line 1997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1997-1997)
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2002-2002)
  on line 2007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2007-2007)
  on line 2012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2012-2012)
  on line 2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2017-2017)
  on line 2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2022-2022)
  on line 2027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2027-2027)
  on line 2032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2032-2032)
  on line 2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2037-2037)
  on line 2042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2042-2042)
  on line 2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2047-2047)
  on line 2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2052-2052)
  on line 2057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2057-2057)
  on line 2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2062-2062)
  on line 2067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2067-2067)
  on line 2072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2072-2072)
  on line 2077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2077-2077)
  on line 2082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2082-2082)
  on line 2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2087-2087)
  on line 2092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2092-2092)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 657
  dead: 94 (7 in uncalled functions)
  total lines: 751
[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.11.cil-2.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.11.cil-2.c:250:7-250:24)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:879:9-879: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.11.cil-2.c:887:10-887: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.11.cil-2.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.11.cil-2.c:635:10-635: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.11.cil-2.c:995:10-995: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.11.cil-2.c:743:10-743:11)
[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.11.cil-2.c:1976:7-1976: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.11.cil-2.c:1981:7-1981: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.11.cil-2.c:347:10-347:11)
[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.11.cil-2.c:771:9-771:19)
[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.11.cil-2.c:1986:7-1986: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.11.cil-2.c:779:10-779: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.11.cil-2.c:1991:7-1991:16)
[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.11.cil-2.c:1996:7-1996: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.11.cil-2.c:2001:7-2001:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2006:7-2006: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.11.cil-2.c:887:10-887:11)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2011:7-2011:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2016:7-2016: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.11.cil-2.c:347:10-347:11)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2021:7-2021: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.11.cil-2.c:635:10-635:11)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2026:7-2026:17)
[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.11.cil-2.c:357:9-357:27)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2031:7-2031:17)
[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.11.cil-2.c:2036:7-2036:15)
[Warning][Deadcode][CWE-571] condition 't9_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:915:9-915:19)
[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.11.cil-2.c:2041:7-2041: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.11.cil-2.c:923:10-923:11)
[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.11.cil-2.c:2046:7-2046:15)
[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.11.cil-2.c:1585:7-1585:15)
[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.11.cil-2.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.11.cil-2.c:2051:7-2051:15)
[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.11.cil-2.c:1590:7-1590: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.11.cil-2.c:2056:7-2056: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.11.cil-2.c:671:10-671:11)
[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.11.cil-2.c:1595:7-1595: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.11.cil-2.c:2061:7-2061:15)
[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.11.cil-2.c:139:9-139:27)
[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.11.cil-2.c:1600:7-1600: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.11.cil-2.c:347:10-347:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2066:7-2066: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.11.cil-2.c:1605:7-1605:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2071:7-2071:15)
[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.11.cil-2.c:1610:7-1610: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.11.cil-2.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.11.cil-2.c:779:10-779:11)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2076:7-2076:15)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1615:7-1615:16)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2081:7-2081:15)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1620:7-1620:16)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2086:7-2086:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1625:7-1625:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:2091:7-2091:16)
[Warning][Deadcode][CWE-570] condition 'T9_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1630:7-1630:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1635:7-1635:17)
[Warning][Deadcode][CWE-570] condition 'T11_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1640:7-1640:17)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:807:9-807:19)
[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.11.cil-2.c:1645:7-1645: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.11.cil-2.c:815:10-815: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.11.cil-2.c:1650:7-1650:15)
[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.11.cil-2.c:1655:7-1655:15)
[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.11.cil-2.c:1660:7-1660:15)
[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.11.cil-2.c:1665:7-1665: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.11.cil-2.c:1256:7-1256: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.11.cil-2.c:923:10-923:11)
[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.11.cil-2.c:1670:7-1670: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.11.cil-2.c:427:10-427:11)
[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.11.cil-2.c:1261:7-1261:16)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1675:7-1675: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.11.cil-2.c:671:10-671:11)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1680:7-1680:15)
[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.11.cil-2.c:1266:7-1266:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1685:7-1685: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.11.cil-2.c:2154:10-2154: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.11.cil-2.c:147:10-147:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1690:7-1690: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.11.cil-2.c:1271:7-1271:16)
[Warning][Deadcode][CWE-571] condition 't10_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:951:9-951:20)
[Warning][Deadcode][CWE-570] condition 'E_10 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1695:7-1695: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.11.cil-2.c:427:10-427:11)
[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.11.cil-2.c:1276:7-1276:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1700:7-1700: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.11.cil-2.c:959:10-959:11)
[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.11.cil-2.c:1713:7-1713:15)
[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.11.cil-2.c:1281:7-1281: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.11.cil-2.c:699:9-699:19)
[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.11.cil-2.c:1718:7-1718: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.11.cil-2.c:707:10-707:11)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1286:7-1286: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.11.cil-2.c:1723:7-1723: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.11.cil-2.c:1728:7-1728:16)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1291:7-1291:16)
[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.11.cil-2.c:180:9-180:27)
[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.11.cil-2.c:1733:7-1733: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.11.cil-2.c:427:10-427: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.11.cil-2.c:2154:10-2154: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.11.cil-2.c:1738:7-1738:16)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1296:7-1296: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.11.cil-2.c:815:10-815:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1743:7-1743:16)
[Warning][Deadcode][CWE-571] condition 't9_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1301:7-1301:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1748:7-1748:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1753:7-1753:16)
[Warning][Deadcode][CWE-571] condition 't10_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1306:7-1306:17)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1758:7-1758:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1763:7-1763:17)
[Warning][Deadcode][CWE-571] condition 't11_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1311:7-1311:17)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:843:9-843:19)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1768:7-1768:17)
[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.11.cil-2.c:1773:7-1773: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.11.cil-2.c:851:10-851:11)
[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.11.cil-2.c:1778:7-1778:15)
[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.11.cil-2.c:1783:7-1783: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.11.cil-2.c:1788:7-1788: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.11.cil-2.c:959:10-959: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.11.cil-2.c:1793:7-1793:15)
[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.11.cil-2.c:1798:7-1798: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.11.cil-2.c:583:9-583:18)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1803:7-1803: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.11.cil-2.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.11.cil-2.c:591:10-591:11)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1808:7-1808:15)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1813:7-1813:15)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1818:7-1818:15)
[Warning][Deadcode][CWE-571] condition 't11_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:987:9-987:20)
[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.11.cil-2.c:188:10-188:11)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1823:7-1823: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.11.cil-2.c:995:10-995:11)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-2+token_ring.11.cil-2.c:1828:7-1828:16)
[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.11.cil-2.c:735:9-735: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.11.cil-2.c:743:10-743: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.11.cil-2.c:851:10-851: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.11.cil-2.c:1396:10-1396: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.11.cil-2.c:591:10-591: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
