./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_1.cil-2+token_ring.12.cil-1.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_1.cil-2+token_ring.12.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_1.cil-2+token_ring.12.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_1.cil-2+token_ring.12.cil-1.c:125:3-145:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:168:3-203:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:255:3-295:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:331:3-343:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:491:3-524:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:547:3-560:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:583:3-596:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:619:3-632:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:655:3-668:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:691:3-704:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:727:3-740:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:763:3-776:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:799:3-812:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:835:3-848:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:871:3-884:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:907:3-920:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:943:3-956:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2185:3-2222:3 with factor 1
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:139:5-139:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:184:5-184:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:505:9-505:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:555:5-555:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:591:5-591:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:627:5-627:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:663:5-663:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:699:5-699:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:735:5-735:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:771:5-771:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:807:5-807:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:843:5-843:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:879:5-879:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:915:5-915:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:951:5-951:15)
[Warning][Deadcode] Function 'error1' has dead code:
  on line 28 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:28-28)
[Warning][Deadcode] Function 'error2' has dead code:
  on line 391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:391-391)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1577-1577)
  on line 1582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1582-1582)
  on line 1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1587-1587)
  on line 1592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1592-1592)
  on line 1597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1597-1597)
  on line 1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1602-1602)
  on line 1607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1607-1607)
  on line 1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1612-1612)
  on line 1617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1617-1617)
  on line 1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1622-1622)
  on line 1627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1627-1627)
  on line 1632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1632-1632)
  on line 1637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1637-1637)
  on line 1642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1642-1642)
  on line 1647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1647-1647)
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1652-1652)
  on line 1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1657-1657)
  on line 1662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1662-1662)
  on line 1667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1667-1667)
  on line 1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1672-1672)
  on line 1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1677-1677)
  on line 1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1682-1682)
  on line 1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1687-1687)
  on line 1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1692-1692)
  on line 1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1697-1697)
  on line 1702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1702-1702)
[Warning][Deadcode] Function 'init_threads1' has dead code:
  on line 217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:217-217)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:222-222)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1226-1226)
  on line 1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1231-1231)
  on line 1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1236-1236)
  on line 1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1241-1241)
  on line 1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1246-1246)
  on line 1251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1251-1251)
  on line 1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1256-1256)
  on line 1261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1261-1261)
  on line 1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1266-1266)
  on line 1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1271-1271)
  on line 1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1276-1276)
  on line 1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1281-1281)
  on line 1286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1286-1286)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1715-1715)
  on line 1720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1720-1720)
  on line 1725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1725-1725)
  on line 1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1730-1730)
  on line 1735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1735-1735)
  on line 1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1740-1740)
  on line 1745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1745-1745)
  on line 1750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1750-1750)
  on line 1755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1755-1755)
  on line 1760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1760-1760)
  on line 1765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1765-1765)
  on line 1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1770-1770)
  on line 1775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1775-1775)
  on line 1780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1780-1780)
  on line 1785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1785-1785)
  on line 1790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1790-1790)
  on line 1795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1795-1795)
  on line 1800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1800-1800)
  on line 1805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1805-1805)
  on line 1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1810-1810)
  on line 1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1815-1815)
  on line 1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1820-1820)
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1825-1825)
  on line 1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1830-1830)
  on line 1835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1835-1835)
  on line 1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1840-1840)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2002-2002)
  on line 2007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2007-2007)
  on line 2012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2012-2012)
  on line 2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2017-2017)
  on line 2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2022-2022)
  on line 2027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2027-2027)
  on line 2032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2032-2032)
  on line 2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2037-2037)
  on line 2042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2042-2042)
  on line 2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2047-2047)
  on line 2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2052-2052)
  on line 2057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2057-2057)
  on line 2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2062-2062)
  on line 2067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2067-2067)
  on line 2072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2072-2072)
  on line 2077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2077-2077)
  on line 2082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2082-2082)
  on line 2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2087-2087)
  on line 2092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2092-2092)
  on line 2097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2097-2097)
  on line 2102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2102-2102)
  on line 2107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2107-2107)
  on line 2112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2112-2112)
  on line 2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2117-2117)
  on line 2122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2122-2122)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 669
  dead: 94
  total lines: 763
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1759:7-1759:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1764:7-1764:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:255:10-255:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2185:10-2185:11)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1769:7-1769:17)
[Warning][Deadcode][CWE-571] condition 't12_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:935:9-935:20)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1774:7-1774:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:943:10-943:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1779:7-1779:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1784:7-1784:15)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:683:9-683:19)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1789:7-1789:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:691:10-691:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1794:7-1794:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1799:7-1799:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1804:7-1804:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:255:10-255:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1809:7-1809:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:799:10-799:11)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1814:7-1814:15)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1819:7-1819:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:547:10-547:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1824:7-1824:15)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1829:7-1829:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1834:7-1834:16)
[Warning][Deadcode][CWE-571] condition 't9_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:827:9-827:19)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1839:7-1839:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1373:10-1373:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:835:10-835:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:575:9-575:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:583:10-583:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:943:10-943:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:691:10-691:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:719:9-719:19)
[Warning][Deadcode][CWE-571] condition 'p_dw_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:117:9-117:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:727:10-727:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:835:10-835:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:583:10-583:11)
[Warning][Deadcode][CWE-571] condition 't10_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:863:9-863:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:331:10-331:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:871:10-871:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1996:7-1996:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2001:7-2001:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:611:9-611:19)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2006:7-2006:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:619:10-619:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:125:10-125:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2011:7-2011:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2016:7-2016:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2021:7-2021:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2026:7-2026:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:727:10-727:11)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2031:7-2031:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2036:7-2036:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1576:7-1576:15)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2041:7-2041:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1581:7-1581:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2046:7-2046:17)
[Warning][Deadcode][CWE-571] condition 'c_dr_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:160:9-160:27)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1586:7-1586:16)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2051:7-2051:17)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:483:9-483:18)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1591:7-1591:16)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:755:9-755:19)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2056:7-2056:17)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1596:7-1596:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:491:10-491:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2061:7-2061:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:763:10-763:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1601:7-1601:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2066:7-2066:15)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1606:7-1606:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2071:7-2071:15)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1611:7-1611:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2076:7-2076:15)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1616:7-1616:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:871:10-871:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2081:7-2081:15)
[Warning][Deadcode][CWE-570] condition 'T9_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1621:7-1621:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2086:7-2086:15)
[Warning][Deadcode][CWE-570] condition 'T10_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1626:7-1626:17)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2091:7-2091:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1223:7-1223:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:619:10-619:11)
[Warning][Deadcode][CWE-570] condition 'T11_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1631:7-1631:17)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2096:7-2096:15)
[Warning][Deadcode][CWE-570] condition 'T12_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1636:7-1636:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:168:10-168:11)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2101:7-2101:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1228:7-1228:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1641:7-1641:15)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2106:7-2106:15)
[Warning][Deadcode][CWE-571] condition 't11_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:899:9-899:20)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1646:7-1646:15)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1233:7-1233:16)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2111:7-2111:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1651:7-1651:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:907:10-907:11)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2116:7-2116:16)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1238:7-1238:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1656:7-1656:15)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2121:7-2121:16)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:647:9-647:19)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1661:7-1661:15)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1243:7-1243:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:655:10-655:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1666:7-1666:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1671:7-1671:15)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1248:7-1248:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1676:7-1676:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:491:10-491:11)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1253:7-1253:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1681:7-1681:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:763:10-763:11)
[Warning][Deadcode][CWE-571] condition 'p_dw_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:214:7-214:24)
[Warning][Deadcode][CWE-570] condition 'E_9 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1686:7-1686:15)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1258:7-1258:16)
[Warning][Deadcode][CWE-570] condition 'E_10 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1691:7-1691:16)
[Warning][Deadcode][CWE-571] condition 'c_dr_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:219:7-219:24)
[Warning][Deadcode][CWE-570] condition 'E_11 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1696:7-1696:16)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1263:7-1263:16)
[Warning][Deadcode][CWE-570] condition 'E_12 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1701:7-1701:16)
[Warning][Deadcode][CWE-571] condition 't9_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1268:7-1268:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1714:7-1714:15)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:518:17-518:29)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:791:9-791:19)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1719:7-1719:16)
[Warning][Deadcode][CWE-571] condition 't10_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1273:7-1273:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:2185:10-2185:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1724:7-1724:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:799:10-799:11)
[Warning][Deadcode][CWE-571] condition 't11_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1278:7-1278:17)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1729:7-1729:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:255:10-255:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:539:9-539:19)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1734:7-1734:16)
[Warning][Deadcode][CWE-571] condition 't12_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1283:7-1283:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:547:10-547:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1739:7-1739:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:907:10-907:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1744:7-1744:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1749:7-1749:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:1754:7-1754:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_1.cil-2+token_ring.12.cil-1.c:655:10-655:11)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
