./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-1+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_2.cil-1+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_2.cil-1+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_2.cil-1+token_ring.15.cil.c:147:3-165:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:188:3-219:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:347:3-387:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:427:3-449:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:603:3-631:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:654:3-667:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:690:3-703:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:726:3-739:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:762:3-775:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:798:3-811:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:834:3-847:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:870:3-883:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:906:3-919:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:942:3-955:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:978:3-991:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1014:3-1027:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1050:3-1063:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1086:3-1099:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2411:3-2448: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-1+token_ring.15.cil.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-1+token_ring.15.cil.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-1+token_ring.15.cil.c:617:9-617:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:662:5-662:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:698:5-698:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:734:5-734:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:770:5-770:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:806:5-806:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:842:5-842:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:878:5-878:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:914:5-914:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:950:5-950:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:986:5-986:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1022:5-1022:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1058:5-1058:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1094:5-1094:15)
[Warning][Deadcode] Function 'immediate_notify_threads' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.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-1+token_ring.15.cil.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-1+token_ring.15.cil.c:497-497)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1763-1763)
  on line 1768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1768-1768)
  on line 1773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1773-1773)
  on line 1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1778-1778)
  on line 1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1783-1783)
  on line 1788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1788-1788)
  on line 1793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1793-1793)
  on line 1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1798-1798)
  on line 1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1803-1803)
  on line 1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1808-1808)
  on line 1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1813-1813)
  on line 1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1818-1818)
  on line 1823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1823-1823)
  on line 1828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1828-1828)
  on line 1833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1833-1833)
  on line 1838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1838-1838)
  on line 1843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1843-1843)
  on line 1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1848-1848)
  on line 1853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1853-1853)
  on line 1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1858-1858)
  on line 1863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1863-1863)
  on line 1868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1868-1868)
  on line 1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1873-1873)
  on line 1878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1878-1878)
  on line 1883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1883-1883)
  on line 1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1888-1888)
  on line 1893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1893-1893)
  on line 1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1898-1898)
[Warning][Deadcode] Function 'init_threads1' has dead code:
  on line 248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:248-248)
  on line 253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:253-253)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 1388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1388-1388)
  on line 1393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1393-1393)
  on line 1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1398-1398)
  on line 1403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1403-1403)
  on line 1408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1408-1408)
  on line 1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1413-1413)
  on line 1418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1418-1418)
  on line 1423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1423-1423)
  on line 1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1428-1428)
  on line 1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1433-1433)
  on line 1438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1438-1438)
  on line 1443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1443-1443)
  on line 1448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1448-1448)
  on line 1453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1453-1453)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1911-1911)
  on line 1916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1916-1916)
  on line 1921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1921-1921)
  on line 1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1926-1926)
  on line 1931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1931-1931)
  on line 1936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1936-1936)
  on line 1941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1941-1941)
  on line 1946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1946-1946)
  on line 1951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1951-1951)
  on line 1956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1956-1956)
  on line 1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1961-1961)
  on line 1966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1966-1966)
  on line 1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1971-1971)
  on line 1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1976-1976)
  on line 1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1981-1981)
  on line 1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1986-1986)
  on line 1991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1991-1991)
  on line 1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1996-1996)
  on line 2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2001-2001)
  on line 2006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2006-2006)
  on line 2011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2011-2011)
  on line 2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2016-2016)
  on line 2021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2021-2021)
  on line 2026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2026-2026)
  on line 2031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2031-2031)
  on line 2036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2036-2036)
  on line 2041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2041-2041)
  on line 2046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2046-2046)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 2217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2217-2217)
  on line 2222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2222-2222)
  on line 2227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2227-2227)
  on line 2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2232-2232)
  on line 2237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2237-2237)
  on line 2242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2242-2242)
  on line 2247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2247-2247)
  on line 2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2252-2252)
  on line 2257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2257-2257)
  on line 2262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2262-2262)
  on line 2267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2267-2267)
  on line 2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2272-2272)
  on line 2277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2277-2277)
  on line 2282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2282-2282)
  on line 2287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2287-2287)
  on line 2292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2292-2292)
  on line 2297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2297-2297)
  on line 2302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2302-2302)
  on line 2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2307-2307)
  on line 2312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2312-2312)
  on line 2317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2317-2317)
  on line 2322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2322-2322)
  on line 2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2327-2327)
  on line 2332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2332-2332)
  on line 2337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2337-2337)
  on line 2342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2342-2342)
  on line 2347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2347-2347)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 733
  dead: 108 (7 in uncalled functions)
  total lines: 841
[Warning][Deadcode][CWE-571] condition 'p_dw_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:245:7-245:24)
[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-1+token_ring.15.cil.c:603:10-603: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-1+token_ring.15.cil.c:870:10-870:11)
[Warning][Deadcode][CWE-571] condition 'c_dr_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:250:7-250:24)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:625:17-625:29)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:898:9-898: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-1+token_ring.15.cil.c:906:10-906:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2211:7-2211:15)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:646:9-646:19)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2216:7-2216:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2221:7-2221: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-1+token_ring.15.cil.c:654:10-654:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2226:7-2226:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1762:7-1762: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-1+token_ring.15.cil.c:1014:10-1014:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2231:7-2231:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1767:7-1767:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2236:7-2236:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1772:7-1772: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-1+token_ring.15.cil.c:762:10-762:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2241:7-2241:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1777:7-1777:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2246:7-2246:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1782:7-1782: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-1+token_ring.15.cil.c:347:10-347:11)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2251:7-2251:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1787:7-1787:16)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1385:7-1385:15)
[Warning][Deadcode][CWE-571] condition 't12_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1042:9-1042:20)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2256:7-2256:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1792:7-1792:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2261:7-2261:17)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1797:7-1797:16)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1390:7-1390: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-1+token_ring.15.cil.c:1050:10-1050:11)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2266:7-2266:17)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1802:7-1802:16)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:790:9-790:19)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1395:7-1395:16)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2271:7-2271:17)
[Warning][Deadcode][CWE-570] condition 'T9_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1807:7-1807: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-1+token_ring.15.cil.c:798:10-798:11)
[Warning][Deadcode][CWE-570] condition 'T13_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2276:7-2276:17)
[Warning][Deadcode][CWE-570] condition 'T10_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1812:7-1812:17)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1400:7-1400:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2281:7-2281:15)
[Warning][Deadcode][CWE-570] condition 'T11_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1817:7-1817:17)
[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-1+token_ring.15.cil.c:347:10-347:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2286:7-2286:15)
[Warning][Deadcode][CWE-570] condition 'T12_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1822:7-1822:17)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1405:7-1405:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2291:7-2291:15)
[Warning][Deadcode][CWE-570] condition 'T13_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1827:7-1827:17)
[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-1+token_ring.15.cil.c:906:10-906:11)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1410:7-1410:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2296:7-2296:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1832:7-1832:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2301:7-2301:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1837:7-1837:15)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1415:7-1415:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2306:7-2306:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1842:7-1842: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-1+token_ring.15.cil.c:654:10-654:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2311:7-2311:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1847:7-1847:15)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1420:7-1420:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2316:7-2316:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1852:7-1852:15)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1425:7-1425:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2321:7-2321:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1857:7-1857:15)
[Warning][Deadcode][CWE-571] condition 't9_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:934:9-934: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-1+token_ring.15.cil.c:347:10-347:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2326:7-2326:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1862:7-1862: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-1+token_ring.15.cil.c:139:9-139:27)
[Warning][Deadcode][CWE-571] condition 't9_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1430:7-1430: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-1+token_ring.15.cil.c:942:10-942:11)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2331:7-2331:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1867:7-1867:15)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:682:9-682:19)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2336:7-2336:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1872:7-1872:15)
[Warning][Deadcode][CWE-571] condition 't10_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1435:7-1435:17)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2341:7-2341:16)
[Warning][Deadcode][CWE-570] condition 'E_9 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1877:7-1877: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-1+token_ring.15.cil.c:690:10-690:11)
[Warning][Deadcode][CWE-571] condition 't11_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1440:7-1440:17)
[Warning][Deadcode][CWE-570] condition 'E_13 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2346:7-2346:16)
[Warning][Deadcode][CWE-570] condition 'E_10 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1882:7-1882: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-1+token_ring.15.cil.c:1050:10-1050:11)
[Warning][Deadcode][CWE-570] condition 'E_11 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1887:7-1887:16)
[Warning][Deadcode][CWE-571] condition 't12_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1445:7-1445:17)
[Warning][Deadcode][CWE-570] condition 'E_12 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1892:7-1892: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-1+token_ring.15.cil.c:798:10-798:11)
[Warning][Deadcode][CWE-570] condition 'E_13 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1897:7-1897:16)
[Warning][Deadcode][CWE-571] condition 't13_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1450:7-1450:17)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1910:7-1910:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1915:7-1915:16)
[Warning][Deadcode][CWE-571] condition 't13_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1078:9-1078:20)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1920:7-1920: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-1+token_ring.15.cil.c:1086:10-1086:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1925:7-1925:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1930:7-1930:16)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:826:9-826: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-1+token_ring.15.cil.c:427:10-427:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1935:7-1935: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-1+token_ring.15.cil.c:834:10-834:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1940:7-1940:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1945:7-1945: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-1+token_ring.15.cil.c:2411:10-2411:11)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1950:7-1950:16)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1955:7-1955: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-1+token_ring.15.cil.c:942:10-942: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-1+token_ring.15.cil.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-1+token_ring.15.cil.c:147:10-147:11)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1960:7-1960:17)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1965:7-1965:17)
[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-1+token_ring.15.cil.c:690:10-690:11)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1970:7-1970:17)
[Warning][Deadcode][CWE-570] condition 'T13_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1975:7-1975:17)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1980:7-1980:15)
[Warning][Deadcode][CWE-571] condition 't10_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:970:9-970:20)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1985:7-1985: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-1+token_ring.15.cil.c:427:10-427:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1990:7-1990: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-1+token_ring.15.cil.c:978:10-978: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-1+token_ring.15.cil.c:2411:10-2411:11)
[Warning][Deadcode][CWE-571] condition 'c_dr_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:180:9-180:27)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1995:7-1995:15)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:718:9-718:19)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2000:7-2000: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-1+token_ring.15.cil.c:726:10-726:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2005:7-2005: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-1+token_ring.15.cil.c:1086:10-1086:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2010:7-2010:15)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2015:7-2015: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-1+token_ring.15.cil.c:1545:10-1545:11)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2020:7-2020: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-1+token_ring.15.cil.c:834:10-834:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2025:7-2025:15)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2030:7-2030:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2035:7-2035:16)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2040:7-2040:16)
[Warning][Deadcode][CWE-570] condition 'E_13 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:2045:7-2045:16)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:862:9-862: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-1+token_ring.15.cil.c:870:10-870:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:595:9-595:18)
[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-1+token_ring.15.cil.c:603:10-603: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-1+token_ring.15.cil.c:978:10-978: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-1+token_ring.15.cil.c:188:10-188:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:726:10-726:11)
[Warning][Deadcode][CWE-571] condition 't11_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:1006:9-1006: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-1+token_ring.15.cil.c:1014:10-1014:11)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.15.cil.c:754:9-754: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-1+token_ring.15.cil.c:762:10-762: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
