./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_3.cil+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_3.cil+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_3.cil+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_3.cil+token_ring.15.cil.c:172:3-195:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:218:3-255:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:418:3-458:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:499:3-536:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:706:3-734:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:757:3-770:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:793:3-806:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:829:3-842:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:865:3-878:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:901:3-914:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:937:3-950:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:973:3-986:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1009:3-1022:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1045:3-1058:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1081:3-1094:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1117:3-1130:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1153:3-1166:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1189:3-1202:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2514:3-2551:3 with factor 1
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:191:5-191:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:720:9-720:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:765:5-765:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:801:5-801:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:837:5-837:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:873:5-873:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:909:5-909:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:945:5-945:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:981:5-981:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1017:5-1017:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1053:5-1053:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1089:5-1089:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1125:5-1125:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1161:5-1161:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1197:5-1197:15)
[Warning][Deadcode] Function 'error1' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:23:1-30:1)
[Warning][Deadcode] Function 'immediate_notify_threads' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:128:1-152:1)
[Warning][Deadcode] Function 'do_read_c' has dead code:
  on lines 225..229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:225-229)
  on line 233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:233-233)
  on lines 237..243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:237-243)
  on line 247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:247-247)
  on line 252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:252-252)
[Warning][Deadcode] Function 'error2' has dead code:
  on line 600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:600-600)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1866-1866)
  on line 1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1871-1871)
  on line 1876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1876-1876)
  on line 1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1881-1881)
  on line 1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1886-1886)
  on line 1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1891-1891)
  on line 1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1896-1896)
  on line 1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1901-1901)
  on line 1906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1906-1906)
  on line 1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1911-1911)
  on line 1916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1916-1916)
  on line 1921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1921-1921)
  on line 1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1926-1926)
  on line 1931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1931-1931)
  on line 1936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1936-1936)
  on line 1941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1941-1941)
  on line 1946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1946-1946)
  on line 1951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1951-1951)
  on line 1956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1956-1956)
  on line 1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1961-1961)
  on line 1966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1966-1966)
  on line 1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1971-1971)
  on line 1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1976-1976)
  on line 1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1981-1981)
  on line 1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1986-1986)
  on line 1991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1991-1991)
  on line 1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1996-1996)
  on line 2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2001-2001)
[Warning][Deadcode] Function 'init_threads1' has dead code:
  on line 284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:284-284)
  on line 289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:289-289)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1491-1491)
  on line 1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1496-1496)
  on line 1501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1501-1501)
  on line 1506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1506-1506)
  on line 1511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1511-1511)
  on line 1516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1516-1516)
  on line 1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1521-1521)
  on line 1526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1526-1526)
  on line 1531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1531-1531)
  on line 1536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1536-1536)
  on line 1541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1541-1541)
  on line 1546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1546-1546)
  on line 1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1551-1551)
  on line 1556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1556-1556)
[Warning][Deadcode] Function 'is_do_read_c_triggered' has dead code:
  on lines 114..115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:114-115)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2014-2014)
  on line 2019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2019-2019)
  on line 2024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2024-2024)
  on line 2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2029-2029)
  on line 2034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2034-2034)
  on line 2039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2039-2039)
  on line 2044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2044-2044)
  on line 2049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2049-2049)
  on line 2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2054-2054)
  on line 2059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2059-2059)
  on line 2064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2064-2064)
  on line 2069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2069-2069)
  on line 2074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2074-2074)
  on line 2079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2079-2079)
  on line 2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2084-2084)
  on line 2089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2089-2089)
  on line 2094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2094-2094)
  on line 2099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2099-2099)
  on line 2104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2104-2104)
  on line 2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2109-2109)
  on line 2114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2114-2114)
  on line 2119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2119-2119)
  on line 2124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2124-2124)
  on line 2129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2129-2129)
  on line 2134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2134-2134)
  on line 2139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2139-2139)
  on line 2144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2144-2144)
  on line 2149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2149-2149)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 2320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2320-2320)
  on line 2325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2325-2325)
  on line 2330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2330-2330)
  on line 2335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2335-2335)
  on line 2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2340-2340)
  on line 2345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2345-2345)
  on line 2350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2350-2350)
  on line 2355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2355-2355)
  on line 2360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2360-2360)
  on line 2365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2365-2365)
  on line 2370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2370-2370)
  on line 2375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2375-2375)
  on line 2380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2380-2380)
  on line 2385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2385-2385)
  on line 2390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2390-2390)
  on line 2395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2395-2395)
  on line 2400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2400-2400)
  on line 2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2405-2405)
  on line 2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2410-2410)
  on line 2415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2415-2415)
  on line 2420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2420-2420)
  on line 2425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2425-2425)
  on line 2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2430-2430)
  on line 2435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2435-2435)
  on line 2440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2440-2440)
  on line 2445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2445-2445)
  on line 2450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2450-2450)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 749
  dead: 126 (9 in uncalled functions)
  total lines: 875
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1117:10-1117:11)
[Warning][Deadcode][CWE-571] condition 'c_dr_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:286:7-286:24)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:857:9-857:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:865:10-865:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:706:10-706:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:973:10-973:11)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:728:17-728:29)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1001:9-1001:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1009:10-1009:11)
[Warning][Deadcode][CWE-571] condition 'fast_clk_edge == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:373:7-373:31)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2314:7-2314:15)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:749:9-749:19)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2319:7-2319:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2324:7-2324:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:757:10-757:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2329:7-2329:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1865:7-1865:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1117:10-1117:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2334:7-2334:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1870:7-1870:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2339:7-2339:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1875:7-1875:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:865:10-865:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2344:7-2344:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1880:7-1880:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:418:10-418:11)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2349:7-2349:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1885:7-1885:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2354:7-2354:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1890:7-1890:16)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1488:7-1488:15)
[Warning][Deadcode][CWE-571] condition 't12_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1145:9-1145:20)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2359:7-2359:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1895:7-1895:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2364:7-2364:17)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1900:7-1900:16)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1493:7-1493:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1153:10-1153:11)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2369:7-2369:17)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1905:7-1905:16)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:893:9-893:19)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1498:7-1498:16)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2374:7-2374:17)
[Warning][Deadcode][CWE-570] condition 'T9_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1910:7-1910:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:901:10-901:11)
[Warning][Deadcode][CWE-570] condition 'T13_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2379:7-2379:17)
[Warning][Deadcode][CWE-570] condition 'T10_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1915:7-1915:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:418:10-418:11)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1503:7-1503:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2384:7-2384:15)
[Warning][Deadcode][CWE-570] condition 'T11_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1920:7-1920:17)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2389:7-2389:15)
[Warning][Deadcode][CWE-570] condition 'T12_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1925:7-1925:17)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1508:7-1508:16)
[Warning][Deadcode][CWE-570] condition 'c_dr_pc == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:113:7-113:25)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2394:7-2394:15)
[Warning][Deadcode][CWE-570] condition 'T13_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1930:7-1930:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1009:10-1009:11)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1513:7-1513:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2399:7-2399:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1935:7-1935:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2404:7-2404:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1940:7-1940:15)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1518:7-1518:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2409:7-2409:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1945:7-1945:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:757:10-757:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2414:7-2414:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1950:7-1950:15)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1523:7-1523:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2419:7-2419:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1955:7-1955:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:418:10-418:11)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1528:7-1528:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2424:7-2424:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1960:7-1960:15)
[Warning][Deadcode][CWE-571] condition 't9_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1037:9-1037:19)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2429:7-2429:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1965:7-1965:15)
[Warning][Deadcode][CWE-571] condition 'p_dw_pc == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:163:11-163:29)
[Warning][Deadcode][CWE-571] condition 't9_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1533:7-1533:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1045:10-1045:11)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2434:7-2434:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1970:7-1970:15)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:785:9-785:19)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2439:7-2439:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1975:7-1975:15)
[Warning][Deadcode][CWE-571] condition 't10_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1538:7-1538:17)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2444:7-2444:16)
[Warning][Deadcode][CWE-570] condition 'E_9 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1980:7-1980:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:793:10-793:11)
[Warning][Deadcode][CWE-571] condition 't11_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1543:7-1543:17)
[Warning][Deadcode][CWE-570] condition 'E_13 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2449:7-2449:16)
[Warning][Deadcode][CWE-570] condition 'E_10 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1985:7-1985:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1153:10-1153:11)
[Warning][Deadcode][CWE-570] condition 'E_11 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1990:7-1990:16)
[Warning][Deadcode][CWE-571] condition 't12_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1548:7-1548:17)
[Warning][Deadcode][CWE-570] condition 'E_12 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1995:7-1995:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:901:10-901:11)
[Warning][Deadcode][CWE-570] condition 'E_13 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2000:7-2000:16)
[Warning][Deadcode][CWE-571] condition 't13_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1553:7-1553:17)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2013:7-2013:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2018:7-2018:16)
[Warning][Deadcode][CWE-571] condition 't13_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1181:9-1181:20)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2023:7-2023:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1189:10-1189:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2028:7-2028:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:499:10-499:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2033:7-2033:16)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:929:9-929:19)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2038:7-2038:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:937:10-937:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2043:7-2043:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:172:10-172:11)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2048:7-2048:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2514:10-2514:11)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2053:7-2053:16)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2058:7-2058:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1045:10-1045:11)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2063:7-2063:17)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2068:7-2068:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:793:10-793:11)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2073:7-2073:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:499:10-499:11)
[Warning][Deadcode][CWE-570] condition 'T13_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2078:7-2078:17)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2083:7-2083:15)
[Warning][Deadcode][CWE-570] condition 'c_dr_pc == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:210:9-210:27)
[Warning][Deadcode][CWE-571] condition 't10_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1073:9-1073:20)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2088:7-2088:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:218:10-218:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2093:7-2093:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1081:10-1081:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2514:10-2514:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2098:7-2098:15)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:821:9-821:19)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2103:7-2103:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:829:10-829:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2108:7-2108:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1189:10-1189:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2113:7-2113:15)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2118:7-2118:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1648:10-1648:11)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2123:7-2123:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:937:10-937:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2128:7-2128:15)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2133:7-2133:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2138:7-2138:16)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2143:7-2143:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:218:10-218:11)
[Warning][Deadcode][CWE-570] condition 'E_13 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:2148:7-2148:16)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:965:9-965:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:973:10-973:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:698:9-698:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:706:10-706:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1081:10-1081:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:829:10-829:11)
[Warning][Deadcode][CWE-571] condition 't11_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:1109:9-1109:20)
[Warning][Deadcode][CWE-571] condition 'p_dw_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.15.cil.c:281:7-281:24)
[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
