./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.10.cil-1.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.10.cil-1.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.10.cil-1.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.10.cil-1.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.10.cil-1.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.10.cil-1.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.10.cil-1.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.10.cil-1.c:688:3-721:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:744:3-757:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:780:3-793:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:816:3-829:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:852:3-865:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:888:3-901:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:924:3-937:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:960:3-973:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:996:3-1009:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1032:3-1045:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1068:3-1081:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2144:3-2181: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.10.cil-1.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.10.cil-1.c:702:9-702:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:752:5-752:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:788:5-788:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:824:5-824:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:860:5-860:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:896:5-896:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:932:5-932:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:968:5-968:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1004:5-1004:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1040:5-1040:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1076:5-1076:15)
[Warning][Deadcode] Function 'error1' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.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.10.cil-1.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.10.cil-1.c:225-229)
  on line 233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:233-233)
  on lines 237..243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:237-243)
  on line 247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:247-247)
  on line 252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.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.10.cil-1.c:600-600)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1616-1616)
  on line 1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1621-1621)
  on line 1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1626-1626)
  on line 1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1631-1631)
  on line 1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1636-1636)
  on line 1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1641-1641)
  on line 1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1646-1646)
  on line 1651 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1651-1651)
  on line 1656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1656-1656)
  on line 1661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1661-1661)
  on line 1666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1666-1666)
  on line 1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1671-1671)
  on line 1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1676-1676)
  on line 1681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1681-1681)
  on line 1686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1686-1686)
  on line 1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1691-1691)
  on line 1696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1696-1696)
  on line 1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1701-1701)
  on line 1706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1706-1706)
  on line 1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1711-1711)
  on line 1716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1716-1716)
  on line 1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1721-1721)
[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.10.cil-1.c:284-284)
  on line 289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:289-289)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1313-1313)
  on line 1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1318-1318)
  on line 1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1323-1323)
  on line 1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1328-1328)
  on line 1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1333-1333)
  on line 1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1338-1338)
  on line 1343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1343-1343)
  on line 1348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1348-1348)
  on line 1353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1353-1353)
  on line 1358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1358-1358)
  on line 1363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1363-1363)
[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.10.cil-1.c:114-115)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1734-1734)
  on line 1739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1739-1739)
  on line 1744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1744-1744)
  on line 1749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1749-1749)
  on line 1754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1754-1754)
  on line 1759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1759-1759)
  on line 1764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1764-1764)
  on line 1769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1769-1769)
  on line 1774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1774-1774)
  on line 1779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1779-1779)
  on line 1784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1784-1784)
  on line 1789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1789-1789)
  on line 1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1794-1794)
  on line 1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1799-1799)
  on line 1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1804-1804)
  on line 1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1809-1809)
  on line 1814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1814-1814)
  on line 1819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1819-1819)
  on line 1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1824-1824)
  on line 1829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1829-1829)
  on line 1834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1834-1834)
  on line 1839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1839-1839)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1983-1983)
  on line 1988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1988-1988)
  on line 1993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1993-1993)
  on line 1998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:1998-1998)
  on line 2003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2003-2003)
  on line 2008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2008-2008)
  on line 2013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2013-2013)
  on line 2018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2018-2018)
  on line 2023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2023-2023)
  on line 2028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2028-2028)
  on line 2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2033-2033)
  on line 2038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2038-2038)
  on line 2043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2043-2043)
  on line 2048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2048-2048)
  on line 2053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2053-2053)
  on line 2058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2058-2058)
  on line 2063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2063-2063)
  on line 2068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2068-2068)
  on line 2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2073-2073)
  on line 2078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2078-2078)
  on line 2083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2083-2083)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 643
  dead: 105 (9 in uncalled functions)
  total lines: 748
[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.10.cil-1.c:2037:7-2037:15)
[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.10.cil-1.c:286:7-286:24)
[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.10.cil-1.c:2042:7-2042:15)
[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.10.cil-1.c:2047:7-2047: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.10.cil-1.c:2052:7-2052:15)
[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.10.cil-1.c:844:9-844:19)
[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.10.cil-1.c:2057:7-2057: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.10.cil-1.c:852:10-852: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.10.cil-1.c:2062:7-2062: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.10.cil-1.c:2067:7-2067: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.10.cil-1.c:2072:7-2072: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.10.cil-1.c:688:10-688: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.10.cil-1.c:2077:7-2077:15)
[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.10.cil-1.c:1615:7-1615: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.10.cil-1.c:960:10-960: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.10.cil-1.c:2082:7-2082: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.10.cil-1.c:1620:7-1620: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.10.cil-1.c:1625:7-1625: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.10.cil-1.c:1630:7-1630: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.10.cil-1.c:1635:7-1635: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.10.cil-1.c:1640:7-1640:16)
[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.10.cil-1.c:715:17-715:29)
[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.10.cil-1.c:373:7-373:31)
[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.10.cil-1.c:988:9-988:19)
[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.10.cil-1.c:1645:7-1645:16)
[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.10.cil-1.c:1650:7-1650: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.10.cil-1.c:996:10-996:11)
[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.10.cil-1.c:1655:7-1655: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.10.cil-1.c:736:9-736:19)
[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.10.cil-1.c:1660:7-1660: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.10.cil-1.c:744:10-744:11)
[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.10.cil-1.c:1665:7-1665:17)
[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.10.cil-1.c:1670:7-1670:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:418:10-418:11)
[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.10.cil-1.c:1675:7-1675:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:2144:10-2144:11)
[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.10.cil-1.c:1680:7-1680: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.10.cil-1.c:852:10-852:11)
[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.10.cil-1.c:1685:7-1685: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.10.cil-1.c:1690:7-1690: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.10.cil-1.c:1695:7-1695: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.10.cil-1.c:1700:7-1700:15)
[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.10.cil-1.c:1705:7-1705: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.10.cil-1.c:418:10-418:11)
[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.10.cil-1.c:1710:7-1710: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.10.cil-1.c:880:9-880:19)
[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.10.cil-1.c:1715:7-1715: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.10.cil-1.c:888:10-888: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.10.cil-1.c:2144:10-2144:11)
[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.10.cil-1.c:1720:7-1720: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.10.cil-1.c:113:7-113:25)
[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.10.cil-1.c:1310:7-1310:15)
[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.10.cil-1.c:1733:7-1733: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.10.cil-1.c:1315:7-1315:16)
[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.10.cil-1.c:1738:7-1738: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.10.cil-1.c:996:10-996: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.10.cil-1.c:1743:7-1743:16)
[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.10.cil-1.c:1320:7-1320:16)
[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.10.cil-1.c:1748:7-1748: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.10.cil-1.c:1753:7-1753:16)
[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.10.cil-1.c:1325:7-1325: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.10.cil-1.c:744:10-744: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.10.cil-1.c:418:10-418: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.10.cil-1.c:1758:7-1758:16)
[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.10.cil-1.c:1330:7-1330: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.10.cil-1.c:1763:7-1763:16)
[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.10.cil-1.c:163:11-163:29)
[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.10.cil-1.c:1768:7-1768:16)
[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.10.cil-1.c:1335:7-1335: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.10.cil-1.c:1024:9-1024:19)
[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.10.cil-1.c:1773:7-1773: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.10.cil-1.c:1032:10-1032: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.10.cil-1.c:1778:7-1778:16)
[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.10.cil-1.c:1340:7-1340: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.10.cil-1.c:1783:7-1783:17)
[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.10.cil-1.c:772:9-772:19)
[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.10.cil-1.c:1345:7-1345: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.10.cil-1.c:1788:7-1788:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.10.cil-1.c:780:10-780:11)
[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.10.cil-1.c:1793:7-1793:15)
[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.10.cil-1.c:1350:7-1350:16)
[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.10.cil-1.c:1798:7-1798:15)
[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.10.cil-1.c:1803:7-1803:15)
[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.10.cil-1.c:1355:7-1355:16)
[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.10.cil-1.c:1808:7-1808: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.10.cil-1.c:888:10-888:11)
[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.10.cil-1.c:1360:7-1360:17)
[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.10.cil-1.c:1813:7-1813:15)
[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.10.cil-1.c:1818:7-1818: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.10.cil-1.c:1823:7-1823: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.10.cil-1.c:499:10-499: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.10.cil-1.c:1828:7-1828: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.10.cil-1.c:1833:7-1833:15)
[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.10.cil-1.c:916:9-916:19)
[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.10.cil-1.c:1838:7-1838: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.10.cil-1.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.10.cil-1.c:924:10-924: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.10.cil-1.c:1032:10-1032: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.10.cil-1.c:499:10-499: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.10.cil-1.c:780:10-780: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.10.cil-1.c:210:9-210:27)
[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.10.cil-1.c:218:10-218:11)
[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.10.cil-1.c:1060:9-1060: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.10.cil-1.c:1068:10-1068:11)
[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.10.cil-1.c:808:9-808: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.10.cil-1.c:1440:10-1440: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.10.cil-1.c:816:10-816: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.10.cil-1.c:924:10-924: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.10.cil-1.c:218:10-218: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.10.cil-1.c:1977:7-1977: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.10.cil-1.c:1982:7-1982:16)
[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.10.cil-1.c:680:9-680:18)
[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.10.cil-1.c:952:9-952: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.10.cil-1.c:1987:7-1987: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.10.cil-1.c:688:10-688: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.10.cil-1.c:1992:7-1992: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.10.cil-1.c:960:10-960: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.10.cil-1.c:1997:7-1997: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.10.cil-1.c:2002:7-2002: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.10.cil-1.c:2007:7-2007: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.10.cil-1.c:1068:10-1068: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.10.cil-1.c:2012:7-2012: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.10.cil-1.c:2017:7-2017: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.10.cil-1.c:2022:7-2022: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.10.cil-1.c:816:10-816: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.10.cil-1.c:2027:7-2027:17)
[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.10.cil-1.c:281:7-281:24)
[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.10.cil-1.c:2032:7-2032:15)
[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
