./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/token_ring.12.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/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/systemc/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/systemc/token_ring.12.cil-1.c:121:3-154:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:177:3-190:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:213:3-226:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:249:3-262:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:285:3-298:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:321:3-334:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:357:3-370:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:393:3-406:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:429:3-442:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:465:3-478:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:501:3-514:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:537:3-550:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:573:3-586:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1815:3-1852: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/systemc/token_ring.12.cil-1.c:135:9-135:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:185:5-185:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:221:5-221:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:257:5-257:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:293:5-293:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:329:5-329:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:365:5-365:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:401:5-401:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:437:5-437:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:473:5-473:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:509:5-509:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:545:5-545:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:581:5-581:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 1207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1207-1207)
  on line 1212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1212-1212)
  on line 1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1217-1217)
  on line 1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1222-1222)
  on line 1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1227-1227)
  on line 1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1232-1232)
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1237-1237)
  on line 1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1242-1242)
  on line 1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1247-1247)
  on line 1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1252-1252)
  on line 1257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1257-1257)
  on line 1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1262-1262)
  on line 1267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1267-1267)
  on line 1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1272-1272)
  on line 1277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1277-1277)
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1282-1282)
  on line 1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1287-1287)
  on line 1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1292-1292)
  on line 1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1297-1297)
  on line 1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1302-1302)
  on line 1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1307-1307)
  on line 1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1312-1312)
  on line 1317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1317-1317)
  on line 1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1322-1322)
  on line 1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1327-1327)
  on line 1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1332-1332)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:856-856)
  on line 861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:861-861)
  on line 866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:866-866)
  on line 871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:871-871)
  on line 876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:876-876)
  on line 881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:881-881)
  on line 886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:886-886)
  on line 891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:891-891)
  on line 896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:896-896)
  on line 901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:901-901)
  on line 906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:906-906)
  on line 911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:911-911)
  on line 916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:916-916)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1345-1345)
  on line 1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1350-1350)
  on line 1355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1355-1355)
  on line 1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1360-1360)
  on line 1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1365-1365)
  on line 1370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1370-1370)
  on line 1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1375-1375)
  on line 1380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1380-1380)
  on line 1385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1385-1385)
  on line 1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1390-1390)
  on line 1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1395-1395)
  on line 1400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1400-1400)
  on line 1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1405-1405)
  on line 1410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1410-1410)
  on line 1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1415-1415)
  on line 1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1420-1420)
  on line 1425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1425-1425)
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1430-1430)
  on line 1435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1435-1435)
  on line 1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1440-1440)
  on line 1445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1445-1445)
  on line 1450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1450-1450)
  on line 1455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1455-1455)
  on line 1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1460-1460)
  on line 1465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1465-1465)
  on line 1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1470-1470)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 1632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1632-1632)
  on line 1637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1637-1637)
  on line 1642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1642-1642)
  on line 1647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1647-1647)
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1652-1652)
  on line 1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1657-1657)
  on line 1662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1662-1662)
  on line 1667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1667-1667)
  on line 1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1672-1672)
  on line 1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1677-1677)
  on line 1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1682-1682)
  on line 1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1687-1687)
  on line 1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1692-1692)
  on line 1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1697-1697)
  on line 1702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1702-1702)
  on line 1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1707-1707)
  on line 1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1712-1712)
  on line 1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1717-1717)
  on line 1722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1722-1722)
  on line 1727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1727-1727)
  on line 1732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1732-1732)
  on line 1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1737-1737)
  on line 1742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1742-1742)
  on line 1747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1747-1747)
  on line 1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1752-1752)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 547
  dead: 91
  total lines: 638
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:465:10-465:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:213:10-213:11)
[Warning][Deadcode][CWE-571] condition 't10_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:493:9-493:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:501:10-501:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1626:7-1626:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1631:7-1631:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:241:9-241:19)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1636:7-1636:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:249:10-249:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1641:7-1641:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1646:7-1646:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1651:7-1651:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1656:7-1656:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:357:10-357:11)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1661:7-1661:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1666:7-1666:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1206:7-1206:15)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1671:7-1671:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1211:7-1211:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1676:7-1676:17)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1216:7-1216:16)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1681:7-1681:17)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:113:9-113:18)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1221:7-1221:16)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:385:9-385:19)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1686:7-1686:17)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1226:7-1226:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:121:10-121:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1691:7-1691:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:393:10-393:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1231:7-1231:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1696:7-1696:15)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1236:7-1236:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1701:7-1701:15)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1241:7-1241:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1706:7-1706:15)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1246:7-1246:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:501:10-501:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1711:7-1711:15)
[Warning][Deadcode][CWE-570] condition 'T9_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1251:7-1251:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1716:7-1716:15)
[Warning][Deadcode][CWE-570] condition 'T10_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1256:7-1256:17)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1721:7-1721:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:853:7-853:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:249:10-249:11)
[Warning][Deadcode][CWE-570] condition 'T11_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1261:7-1261:17)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1726:7-1726:15)
[Warning][Deadcode][CWE-570] condition 'T12_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1266:7-1266:17)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1731:7-1731:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:858:7-858:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1271:7-1271:15)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1736:7-1736:15)
[Warning][Deadcode][CWE-571] condition 't11_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:529:9-529:20)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1276:7-1276:15)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:863:7-863:16)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1741:7-1741:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1281:7-1281:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:537:10-537:11)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1746:7-1746:16)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:868:7-868:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1286:7-1286:15)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1751:7-1751:16)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:277:9-277:19)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1291:7-1291:15)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:873:7-873:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:285:10-285:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1296:7-1296:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1301:7-1301:15)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:878:7-878:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1306:7-1306:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:121:10-121:11)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:883:7-883:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1311:7-1311:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:393:10-393:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1316:7-1316:15)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:888:7-888:16)
[Warning][Deadcode][CWE-570] condition 'E_10 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1321:7-1321:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1326:7-1326:16)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:893:7-893:16)
[Warning][Deadcode][CWE-570] condition 'E_12 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1331:7-1331:16)
[Warning][Deadcode][CWE-571] condition 't9_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:898:7-898:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1344:7-1344:15)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:148:17-148:29)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:421:9-421:19)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1349:7-1349:16)
[Warning][Deadcode][CWE-571] condition 't10_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:903:7-903:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1815:10-1815:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1354:7-1354:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:429:10-429:11)
[Warning][Deadcode][CWE-571] condition 't11_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:908:7-908:17)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1359:7-1359:16)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:169:9-169:19)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1364:7-1364:16)
[Warning][Deadcode][CWE-571] condition 't12_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:913:7-913:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:177:10-177:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1369:7-1369:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:537:10-537:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1374:7-1374:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1379:7-1379:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1384:7-1384:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:285:10-285:11)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1389:7-1389:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1394:7-1394:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1815:10-1815:11)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1399:7-1399:17)
[Warning][Deadcode][CWE-571] condition 't12_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:565:9-565:20)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1404:7-1404:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:573:10-573:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1409:7-1409:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1414:7-1414:15)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:313:9-313:19)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1419:7-1419:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:321:10-321:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1424:7-1424:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1429:7-1429:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1434:7-1434:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1439:7-1439:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:429:10-429:11)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1444:7-1444:15)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1449:7-1449:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:177:10-177:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1454:7-1454:15)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1459:7-1459:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1464:7-1464:16)
[Warning][Deadcode][CWE-571] condition 't9_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:457:9-457:19)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1469:7-1469:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:1003:10-1003:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:465:10-465:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:205:9-205:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:213:10-213:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:573:10-573:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:321:10-321:11)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:349:9-349:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.12.cil-1.c:357:10-357: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
