./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_1.cil-2+token_ring.15.cil.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_1.cil-2+token_ring.15.cil.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.15.cil.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.15.cil.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.15.cil.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.15.cil.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.15.cil.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.15.cil.c:497:3-525:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:548:3-561:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:584:3-597:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:620:3-633:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:656:3-669:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:692:3-705:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:728:3-741:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:764:3-777:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:800:3-813:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:836:3-849:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:872:3-885:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:908:3-921:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:944:3-957:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:980:3-993:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2305:3-2342: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.15.cil.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.15.cil.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.15.cil.c:511:9-511:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:556:5-556:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:592:5-592:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:628:5-628:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:664:5-664:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:700:5-700:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:736:5-736:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:772:5-772:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:808:5-808:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:844:5-844:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:880:5-880:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:916:5-916:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:952:5-952:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:988:5-988: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.15.cil.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.15.cil.c:391-391)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1657-1657)
  on line 1662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1662-1662)
  on line 1667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1667-1667)
  on line 1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1672-1672)
  on line 1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1677-1677)
  on line 1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1682-1682)
  on line 1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1687-1687)
  on line 1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1692-1692)
  on line 1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1697-1697)
  on line 1702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1702-1702)
  on line 1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1707-1707)
  on line 1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1712-1712)
  on line 1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1717-1717)
  on line 1722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1722-1722)
  on line 1727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1727-1727)
  on line 1732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1732-1732)
  on line 1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1737-1737)
  on line 1742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1742-1742)
  on line 1747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1747-1747)
  on line 1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1752-1752)
  on line 1757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1757-1757)
  on line 1762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1762-1762)
  on line 1767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1767-1767)
  on line 1772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1772-1772)
  on line 1777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1777-1777)
  on line 1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1782-1782)
  on line 1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1787-1787)
  on line 1792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1792-1792)
[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.15.cil.c:217-217)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:222-222)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1282-1282)
  on line 1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1287-1287)
  on line 1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1292-1292)
  on line 1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1297-1297)
  on line 1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1302-1302)
  on line 1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1307-1307)
  on line 1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1312-1312)
  on line 1317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1317-1317)
  on line 1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1322-1322)
  on line 1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1327-1327)
  on line 1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1332-1332)
  on line 1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1337-1337)
  on line 1342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1342-1342)
  on line 1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1347-1347)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1805-1805)
  on line 1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1810-1810)
  on line 1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1815-1815)
  on line 1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1820-1820)
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1825-1825)
  on line 1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1830-1830)
  on line 1835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1835-1835)
  on line 1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1840-1840)
  on line 1845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1845-1845)
  on line 1850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1850-1850)
  on line 1855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1855-1855)
  on line 1860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1860-1860)
  on line 1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1865-1865)
  on line 1870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1870-1870)
  on line 1875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1875-1875)
  on line 1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1880-1880)
  on line 1885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1885-1885)
  on line 1890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1890-1890)
  on line 1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1895-1895)
  on line 1900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1900-1900)
  on line 1905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1905-1905)
  on line 1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1910-1910)
  on line 1915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1915-1915)
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1920-1920)
  on line 1925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1925-1925)
  on line 1930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1930-1930)
  on line 1935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1935-1935)
  on line 1940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1940-1940)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2111-2111)
  on line 2116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2116-2116)
  on line 2121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2121-2121)
  on line 2126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2126-2126)
  on line 2131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2131-2131)
  on line 2136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2136-2136)
  on line 2141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2141-2141)
  on line 2146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2146-2146)
  on line 2151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2151-2151)
  on line 2156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2156-2156)
  on line 2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2161-2161)
  on line 2166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2166-2166)
  on line 2171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2171-2171)
  on line 2176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2176-2176)
  on line 2181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2181-2181)
  on line 2186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2186-2186)
  on line 2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2191-2191)
  on line 2196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2196-2196)
  on line 2201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2201-2201)
  on line 2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2206-2206)
  on line 2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2211-2211)
  on line 2216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2216-2216)
  on line 2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2221-2221)
  on line 2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2226-2226)
  on line 2231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2231-2231)
  on line 2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2236-2236)
  on line 2241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2241-2241)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 703
  dead: 101
  total lines: 804
[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.15.cil.c:1279:7-1279:15)
[Warning][Deadcode][CWE-571] condition 't12_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:936:9-936:20)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2150:7-2150:16)
[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.15.cil.c:1686:7-1686: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.15.cil.c:255:10-255:11)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2155:7-2155:17)
[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.15.cil.c:1691:7-1691:16)
[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.15.cil.c:1284:7-1284: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.15.cil.c:944:10-944:11)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2160:7-2160:17)
[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.15.cil.c:1696:7-1696:16)
[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.15.cil.c:684:9-684:19)
[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.15.cil.c:1289:7-1289:16)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2165:7-2165:17)
[Warning][Deadcode][CWE-570] condition 'T9_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1701:7-1701: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.15.cil.c:692:10-692:11)
[Warning][Deadcode][CWE-570] condition 'T13_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2170:7-2170:17)
[Warning][Deadcode][CWE-570] condition 'T10_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1706:7-1706:17)
[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.15.cil.c:1294:7-1294: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.15.cil.c:2175:7-2175:15)
[Warning][Deadcode][CWE-570] condition 'T11_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1711:7-1711:17)
[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.15.cil.c:2180:7-2180:15)
[Warning][Deadcode][CWE-570] condition 'T12_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1716:7-1716:17)
[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.15.cil.c:1299:7-1299:16)
[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.15.cil.c:2185:7-2185:15)
[Warning][Deadcode][CWE-570] condition 'T13_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1721:7-1721:17)
[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.15.cil.c:800:10-800: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.15.cil.c:1304:7-1304:16)
[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.15.cil.c:2190:7-2190:15)
[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.15.cil.c:1726:7-1726: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.15.cil.c:255:10-255:11)
[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.15.cil.c:2195:7-2195: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.15.cil.c:1731:7-1731:15)
[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.15.cil.c:1309:7-1309:16)
[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.15.cil.c:2200:7-2200: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.15.cil.c:1736:7-1736: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.15.cil.c:548:10-548: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.15.cil.c:2205:7-2205:15)
[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.15.cil.c:1741:7-1741:15)
[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.15.cil.c:1314:7-1314: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.15.cil.c:2210:7-2210:15)
[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.15.cil.c:1746:7-1746:15)
[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.15.cil.c:1319:7-1319:16)
[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.15.cil.c:2215:7-2215: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.15.cil.c:1751:7-1751:15)
[Warning][Deadcode][CWE-571] condition 't9_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:828:9-828:19)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2220:7-2220:15)
[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.15.cil.c:1756:7-1756:15)
[Warning][Deadcode][CWE-571] condition 't9_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1324:7-1324: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.15.cil.c:836:10-836:11)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2225:7-2225:16)
[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.15.cil.c:1761:7-1761: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.15.cil.c:576:9-576:19)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2230:7-2230:16)
[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.15.cil.c:1766:7-1766:15)
[Warning][Deadcode][CWE-571] condition 't10_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1329:7-1329:17)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2235:7-2235:16)
[Warning][Deadcode][CWE-570] condition 'E_9 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1771:7-1771: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.15.cil.c:584:10-584:11)
[Warning][Deadcode][CWE-571] condition 't11_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1334:7-1334:17)
[Warning][Deadcode][CWE-570] condition 'E_13 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2240:7-2240:16)
[Warning][Deadcode][CWE-570] condition 'E_10 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1776:7-1776: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.15.cil.c:944:10-944:11)
[Warning][Deadcode][CWE-570] condition 'E_11 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1781:7-1781:16)
[Warning][Deadcode][CWE-571] condition 't12_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1339:7-1339:17)
[Warning][Deadcode][CWE-570] condition 'E_12 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1786:7-1786: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.15.cil.c:692:10-692: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.15.cil.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'E_13 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1791:7-1791:16)
[Warning][Deadcode][CWE-571] condition 't13_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1344:7-1344:17)
[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.15.cil.c:1804:7-1804: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.15.cil.c:1809:7-1809:16)
[Warning][Deadcode][CWE-571] condition 't13_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:972:9-972:20)
[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.15.cil.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.15.cil.c:1814:7-1814: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.15.cil.c:980:10-980:11)
[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.15.cil.c:1819:7-1819: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.15.cil.c:1824:7-1824: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.15.cil.c:720:9-720: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.15.cil.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.15.cil.c:1829:7-1829: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.15.cil.c:728:10-728:11)
[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.15.cil.c:1834:7-1834: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.15.cil.c:117:9-117:27)
[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.15.cil.c:1839:7-1839: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.15.cil.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:2305:10-2305: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.15.cil.c:1844:7-1844:16)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1849:7-1849: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.15.cil.c:836:10-836:11)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1854:7-1854:17)
[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.15.cil.c:331:10-331:11)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1859:7-1859:17)
[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.15.cil.c:584:10-584:11)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1864:7-1864:17)
[Warning][Deadcode][CWE-570] condition 'T13_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1869:7-1869:17)
[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.15.cil.c:331:10-331:11)
[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.15.cil.c:1874:7-1874:15)
[Warning][Deadcode][CWE-571] condition 't10_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:864:9-864:20)
[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.15.cil.c:1879:7-1879:15)
[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.15.cil.c:1884:7-1884: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.15.cil.c:872:10-872: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.15.cil.c:2305:10-2305: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.15.cil.c:1889:7-1889: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.15.cil.c:612:9-612: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.15.cil.c:331:10-331:11)
[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.15.cil.c:1894:7-1894: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.15.cil.c:620:10-620:11)
[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.15.cil.c:1899:7-1899: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.15.cil.c:980:10-980: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.15.cil.c:1904:7-1904: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.15.cil.c:125:10-125:11)
[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.15.cil.c:1909:7-1909: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.15.cil.c:1439:10-1439:11)
[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.15.cil.c:1914:7-1914: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.15.cil.c:728:10-728:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1919:7-1919:15)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1924:7-1924:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1929:7-1929:16)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1934:7-1934:16)
[Warning][Deadcode][CWE-570] condition 'E_13 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:1939:7-1939:16)
[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.15.cil.c:756:9-756:19)
[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.15.cil.c:160:9-160: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.15.cil.c:764:10-764:11)
[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.15.cil.c:489:9-489:18)
[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.15.cil.c:497:10-497: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.15.cil.c:872:10-872: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.15.cil.c:620:10-620:11)
[Warning][Deadcode][CWE-571] condition 't11_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:900:9-900:20)
[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.15.cil.c:168:10-168:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.15.cil.c:908:10-908:11)
[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.15.cil.c:648:9-648: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.15.cil.c:656:10-656: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.15.cil.c:497:10-497: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.15.cil.c:764:10-764: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.15.cil.c:214:7-214:24)
[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.15.cil.c:219:7-219:24)
[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.15.cil.c:519:17-519: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.15.cil.c:792:9-792: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.15.cil.c:800:10-800: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.15.cil.c:2105:7-2105:15)
[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.15.cil.c:540:9-540:19)
[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.15.cil.c:2110:7-2110: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.15.cil.c:2115:7-2115: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.15.cil.c:548:10-548: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.15.cil.c:255:10-255:11)
[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.15.cil.c:2120:7-2120:16)
[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.15.cil.c:1656:7-1656: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.15.cil.c:908:10-908:11)
[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.15.cil.c:2125:7-2125:16)
[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.15.cil.c:1661:7-1661: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.15.cil.c:2130:7-2130:16)
[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.15.cil.c:1666:7-1666: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.15.cil.c:656:10-656:11)
[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.15.cil.c:2135:7-2135:16)
[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.15.cil.c:1671:7-1671: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.15.cil.c:2140:7-2140: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.15.cil.c:1676:7-1676:16)
[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.15.cil.c:2145:7-2145:16)
[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.15.cil.c:1681:7-1681:16)
[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
