./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pc_sfifo_3.cil+token_ring.14.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pc_sfifo_3.cil+token_ring.14.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.14.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.14.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.14.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.14.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.14.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.14.cil.c:700:3-728:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:751:3-764:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:787:3-800:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:823:3-836:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:859:3-872:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:895:3-908:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:931:3-944:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:967:3-980:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1003:3-1016:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1039:3-1052:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1075:3-1088:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1111:3-1124:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1147:3-1160:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2389:3-2426: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.14.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.14.cil.c:714:9-714:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:759:5-759:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:795:5-795:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:831:5-831:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:867:5-867:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:903:5-903:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:939:5-939:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:975:5-975:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1011:5-1011:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1047:5-1047:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1083:5-1083:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1119:5-1119:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1155:5-1155:15)
[Warning][Deadcode] Function 'error1' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.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.14.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.14.cil.c:225-229)
  on line 233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:233-233)
  on lines 237..243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:237-243)
  on line 247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:247-247)
  on line 252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.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.14.cil.c:600-600)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1781-1781)
  on line 1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1786-1786)
  on line 1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1791-1791)
  on line 1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1796-1796)
  on line 1801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1801-1801)
  on line 1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1806-1806)
  on line 1811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1811-1811)
  on line 1816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1816-1816)
  on line 1821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1821-1821)
  on line 1826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1826-1826)
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1831-1831)
  on line 1836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1836-1836)
  on line 1841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1841-1841)
  on line 1846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1846-1846)
  on line 1851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1851-1851)
  on line 1856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1856-1856)
  on line 1861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1861-1861)
  on line 1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1866-1866)
  on line 1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1871-1871)
  on line 1876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1876-1876)
  on line 1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1881-1881)
  on line 1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1886-1886)
  on line 1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1891-1891)
  on line 1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1896-1896)
  on line 1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1901-1901)
  on line 1906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1906-1906)
[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.14.cil.c:284-284)
  on line 289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:289-289)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1430-1430)
  on line 1435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1435-1435)
  on line 1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1440-1440)
  on line 1445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1445-1445)
  on line 1450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1450-1450)
  on line 1455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1455-1455)
  on line 1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1460-1460)
  on line 1465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1465-1465)
  on line 1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1470-1470)
  on line 1475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1475-1475)
  on line 1480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1480-1480)
  on line 1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1485-1485)
  on line 1490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1490-1490)
[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.14.cil.c:114-115)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1919-1919)
  on line 1924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1924-1924)
  on line 1929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1929-1929)
  on line 1934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1934-1934)
  on line 1939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1939-1939)
  on line 1944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1944-1944)
  on line 1949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1949-1949)
  on line 1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1954-1954)
  on line 1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1959-1959)
  on line 1964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1964-1964)
  on line 1969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1969-1969)
  on line 1974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1974-1974)
  on line 1979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1979-1979)
  on line 1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1984-1984)
  on line 1989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1989-1989)
  on line 1994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1994-1994)
  on line 1999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:1999-1999)
  on line 2004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2004-2004)
  on line 2009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2009-2009)
  on line 2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2014-2014)
  on line 2019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2019-2019)
  on line 2024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2024-2024)
  on line 2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2029-2029)
  on line 2034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2034-2034)
  on line 2039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2039-2039)
  on line 2044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2044-2044)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2206-2206)
  on line 2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2211-2211)
  on line 2216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2216-2216)
  on line 2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2221-2221)
  on line 2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2226-2226)
  on line 2231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2231-2231)
  on line 2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2236-2236)
  on line 2241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2241-2241)
  on line 2246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2246-2246)
  on line 2251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2251-2251)
  on line 2256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2256-2256)
  on line 2261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2261-2261)
  on line 2266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2266-2266)
  on line 2271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2271-2271)
  on line 2276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2276-2276)
  on line 2281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2281-2281)
  on line 2286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2286-2286)
  on line 2291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2291-2291)
  on line 2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2296-2296)
  on line 2301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2301-2301)
  on line 2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2306-2306)
  on line 2311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2311-2311)
  on line 2316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2316-2316)
  on line 2321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2321-2321)
  on line 2326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.14.cil.c:2326-2326)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 713
  dead: 119 (9 in uncalled functions)
  total lines: 832
[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.14.cil.c:1855:7-1855: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.14.cil.c:1111:10-1111:11)
[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.14.cil.c:2320:7-2320:16)
[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.14.cil.c:286:7-286:24)
[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.14.cil.c:1442:7-1442:16)
[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.14.cil.c:1860:7-1860:15)
[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.14.cil.c:2325:7-2325:16)
[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.14.cil.c:851:9-851:19)
[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.14.cil.c:1865:7-1865:15)
[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.14.cil.c:1447:7-1447: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.14.cil.c:859:10-859:11)
[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.14.cil.c:1870:7-1870: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.14.cil.c:1875:7-1875:15)
[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.14.cil.c:1452:7-1452: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.14.cil.c:1880:7-1880: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.14.cil.c:1457:7-1457: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.14.cil.c:1885:7-1885: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.14.cil.c:700:10-700: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.14.cil.c:967:10-967:11)
[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.14.cil.c:1890:7-1890: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.14.cil.c:1462:7-1462: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.14.cil.c:1895:7-1895:16)
[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.14.cil.c:1900:7-1900:16)
[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.14.cil.c:1467:7-1467:16)
[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.14.cil.c:1905:7-1905:16)
[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.14.cil.c:1472:7-1472:16)
[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.14.cil.c:1918:7-1918:15)
[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.14.cil.c:722:17-722: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.14.cil.c:995:9-995: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.14.cil.c:1923:7-1923:16)
[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.14.cil.c:1477:7-1477: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.14.cil.c:2389:10-2389:11)
[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.14.cil.c:1928:7-1928: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.14.cil.c:1003:10-1003: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.14.cil.c:373:7-373:31)
[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.14.cil.c:1482:7-1482:17)
[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.14.cil.c:1933:7-1933:16)
[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.14.cil.c:743:9-743:19)
[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.14.cil.c:1938:7-1938: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.14.cil.c:1487:7-1487: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.14.cil.c:751:10-751:11)
[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.14.cil.c:1943:7-1943: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.14.cil.c:1111:10-1111: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.14.cil.c:1948:7-1948:16)
[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.14.cil.c:1953:7-1953: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.14.cil.c:1958:7-1958: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.14.cil.c:859:10-859: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.14.cil.c:418:10-418:11)
[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.14.cil.c:1963:7-1963: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.14.cil.c:1968:7-1968: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.14.cil.c:2389:10-2389: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.14.cil.c:1973:7-1973:17)
[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.14.cil.c:1139:9-1139:20)
[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.14.cil.c:1978:7-1978: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.14.cil.c:1147:10-1147:11)
[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.14.cil.c:1983:7-1983:15)
[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.14.cil.c:1988:7-1988:15)
[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.14.cil.c:887:9-887:19)
[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.14.cil.c:1993:7-1993: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.14.cil.c:895:10-895: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.14.cil.c:418:10-418: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.14.cil.c:1998:7-1998: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.14.cil.c:2003:7-2003:15)
[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.14.cil.c:2008:7-2008: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.14.cil.c:113:7-113:25)
[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.14.cil.c:2013:7-2013: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.14.cil.c:1003:10-1003:11)
[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.14.cil.c:2018:7-2018:15)
[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.14.cil.c:2023:7-2023: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.14.cil.c:751:10-751: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.14.cil.c:2028:7-2028: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.14.cil.c:2033:7-2033: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.14.cil.c:418:10-418:11)
[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.14.cil.c:2038:7-2038:16)
[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.14.cil.c:1031:9-1031:19)
[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.14.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.14.cil.c:1577:10-1577:11)
[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.14.cil.c:163:11-163:29)
[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.14.cil.c:1039:10-1039:11)
[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.14.cil.c:779:9-779: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.14.cil.c:787:10-787: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.14.cil.c:1147:10-1147: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.14.cil.c:895:10-895: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.14.cil.c:499:10-499:11)
[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.14.cil.c:923:9-923: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.14.cil.c:931:10-931: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.14.cil.c:172:10-172: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.14.cil.c:1039:10-1039: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.14.cil.c:787:10-787: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.14.cil.c:499:10-499:11)
[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.14.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.14.cil.c:1067:9-1067:20)
[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.14.cil.c:218:10-218: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.14.cil.c:1075:10-1075:11)
[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.14.cil.c:2200:7-2200: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.14.cil.c:2205:7-2205:16)
[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.14.cil.c:815:9-815:19)
[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.14.cil.c:2210:7-2210: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.14.cil.c:823:10-823: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.14.cil.c:2215:7-2215:16)
[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.14.cil.c:2220:7-2220: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.14.cil.c:2225:7-2225:16)
[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.14.cil.c:2230:7-2230: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.14.cil.c:931:10-931: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.14.cil.c:2235:7-2235: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.14.cil.c:2240:7-2240: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.14.cil.c:1780:7-1780:15)
[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.14.cil.c:2245:7-2245: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.14.cil.c:1785:7-1785: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.14.cil.c:2250:7-2250: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.14.cil.c:218:10-218:11)
[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.14.cil.c:1790:7-1790:16)
[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.14.cil.c:2255:7-2255:17)
[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.14.cil.c:1795:7-1795: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.14.cil.c:959:9-959:19)
[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.14.cil.c:2260:7-2260:17)
[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.14.cil.c:1800:7-1800: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.14.cil.c:2265:7-2265: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.14.cil.c:967:10-967: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.14.cil.c:692:9-692:18)
[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.14.cil.c:1805:7-1805:16)
[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.14.cil.c:2270:7-2270:15)
[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.14.cil.c:1810:7-1810: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.14.cil.c:700:10-700: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.14.cil.c:2275:7-2275:15)
[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.14.cil.c:1815:7-1815: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.14.cil.c:2280:7-2280:15)
[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.14.cil.c:1820:7-1820: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.14.cil.c:1075:10-1075:11)
[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.14.cil.c:2285:7-2285:15)
[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.14.cil.c:1825:7-1825: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.14.cil.c:2290:7-2290:15)
[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.14.cil.c:1830:7-1830:17)
[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.14.cil.c:2295:7-2295:15)
[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.14.cil.c:1427:7-1427: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.14.cil.c:823:10-823:11)
[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.14.cil.c:1835:7-1835:17)
[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.14.cil.c:2300:7-2300: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.14.cil.c:1840:7-1840:17)
[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.14.cil.c:2305:7-2305:15)
[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.14.cil.c:1432:7-1432:16)
[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.14.cil.c:1845:7-1845:15)
[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.14.cil.c:2310:7-2310:15)
[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.14.cil.c:1103:9-1103: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.14.cil.c:281:7-281:24)
[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.14.cil.c:1850:7-1850:15)
[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.14.cil.c:1437:7-1437:16)
[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.14.cil.c:2315:7-2315:16)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
