./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.11.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.11.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.11.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.11.cil-1.c:115:3-148:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:171:3-184:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:207:3-220:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:243:3-256:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:279:3-292:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:315:3-328:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:351:3-364:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:387:3-400:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:423:3-436:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:459:3-472:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:495:3-508:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:531:3-544:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1690:3-1727: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.11.cil-1.c:129:9-129:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:179:5-179:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:215:5-215:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:251:5-251:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:287:5-287:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:323:5-323:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:359:5-359:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:395:5-395:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:431:5-431:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:467:5-467:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:503:5-503:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:539:5-539:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1122-1122)
  on line 1127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1127-1127)
  on line 1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1132-1132)
  on line 1137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1137-1137)
  on line 1142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1142-1142)
  on line 1147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1147-1147)
  on line 1152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1152-1152)
  on line 1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1157-1157)
  on line 1162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1162-1162)
  on line 1167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1167-1167)
  on line 1172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1172-1172)
  on line 1177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1177-1177)
  on line 1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1182-1182)
  on line 1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1187-1187)
  on line 1192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1192-1192)
  on line 1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1197-1197)
  on line 1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1202-1202)
  on line 1207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1207-1207)
  on line 1212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1212-1212)
  on line 1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1217-1217)
  on line 1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1222-1222)
  on line 1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1227-1227)
  on line 1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1232-1232)
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1237-1237)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:795-795)
  on line 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:800-800)
  on line 805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:805-805)
  on line 810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:810-810)
  on line 815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:815-815)
  on line 820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:820-820)
  on line 825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:825-825)
  on line 830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:830-830)
  on line 835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:835-835)
  on line 840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:840-840)
  on line 845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:845-845)
  on line 850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:850-850)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1250-1250)
  on line 1255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1255-1255)
  on line 1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1260-1260)
  on line 1265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1265-1265)
  on line 1270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1270-1270)
  on line 1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1275-1275)
  on line 1280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1280-1280)
  on line 1285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1285-1285)
  on line 1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1290-1290)
  on line 1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1295-1295)
  on line 1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1300-1300)
  on line 1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1305-1305)
  on line 1310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1310-1310)
  on line 1315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1315-1315)
  on line 1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1320-1320)
  on line 1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1325-1325)
  on line 1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1330-1330)
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1335-1335)
  on line 1340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1340-1340)
  on line 1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1345-1345)
  on line 1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1350-1350)
  on line 1355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1355-1355)
  on line 1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1360-1360)
  on line 1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1365-1365)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 1518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1518-1518)
  on line 1523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1523-1523)
  on line 1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1528-1528)
  on line 1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1533-1533)
  on line 1538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1538-1538)
  on line 1543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1543-1543)
  on line 1548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1548-1548)
  on line 1553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1553-1553)
  on line 1558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1558-1558)
  on line 1563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1563-1563)
  on line 1568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1568-1568)
  on line 1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1573-1573)
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1578-1578)
  on line 1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1583-1583)
  on line 1588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1588-1588)
  on line 1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1593-1593)
  on line 1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1598-1598)
  on line 1603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1603-1603)
  on line 1608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1608-1608)
  on line 1613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1613-1613)
  on line 1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1618-1618)
  on line 1623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1623-1623)
  on line 1628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1628-1628)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 511
  dead: 84
  total lines: 595
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1186:7-1186:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1191:7-1191:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1196:7-1196:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1201:7-1201:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:792:7-792:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:459:10-459:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1206:7-1206:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:797:7-797:16)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1211:7-1211:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:207:10-207:11)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1216:7-1216:15)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:802:7-802:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1221:7-1221:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1690:10-1690:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1226:7-1226:15)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:807:7-807:16)
[Warning][Deadcode][CWE-571] condition 't10_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:487:9-487:20)
[Warning][Deadcode][CWE-570] condition 'E_10 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1231:7-1231:16)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:812:7-812:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1236:7-1236:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:495:10-495:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1249:7-1249:15)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:817:7-817:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:235:9-235:19)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1254:7-1254:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:243:10-243:11)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:822:7-822:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1259:7-1259:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1264:7-1264:16)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:827:7-827:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1269:7-1269:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1690:10-1690:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1274:7-1274:16)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:832:7-832:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:351:10-351:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1279:7-1279:16)
[Warning][Deadcode][CWE-571] condition 't9_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:837:7-837:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1284:7-1284:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1289:7-1289:16)
[Warning][Deadcode][CWE-571] condition 't10_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:842:7-842:17)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1294:7-1294:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1299:7-1299:17)
[Warning][Deadcode][CWE-571] condition 't11_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:847:7-847:17)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:107:9-107:18)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:379:9-379:19)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1304:7-1304:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:115:10-115:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1309:7-1309:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:387:10-387:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1314:7-1314:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1319:7-1319:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1324:7-1324:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:495:10-495:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1329:7-1329:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1334:7-1334:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1339:7-1339:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:243:10-243:11)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1344:7-1344:15)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1349:7-1349:15)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1354:7-1354:15)
[Warning][Deadcode][CWE-571] condition 't11_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:523:9-523:20)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1359:7-1359:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:531:10-531:11)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1364:7-1364:16)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:271:9-271:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:279:10-279:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:115:10-115:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:387:10-387:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:932:10-932:11)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:142:17-142:29)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:415:9-415:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:423:10-423:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:163:9-163:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:171:10-171:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:531:10-531:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:279:10-279:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1512:7-1512:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1517:7-1517:16)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:307:9-307:19)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1522:7-1522:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:315:10-315:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1527:7-1527:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1532:7-1532:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1537:7-1537:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1542:7-1542:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:423:10-423:11)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1547:7-1547:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1552:7-1552:16)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1557:7-1557:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:171:10-171:11)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1562:7-1562:17)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1567:7-1567:17)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1572:7-1572:15)
[Warning][Deadcode][CWE-571] condition 't9_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:451:9-451:19)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1577:7-1577:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:459:10-459:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1582:7-1582:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1121:7-1121:15)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:199:9-199:19)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1587:7-1587:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1126:7-1126:16)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1592:7-1592:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:207:10-207:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1131:7-1131:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1597:7-1597:15)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1136:7-1136:16)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1602:7-1602:15)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1141:7-1141:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1607:7-1607:15)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1146:7-1146:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:315:10-315:11)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1612:7-1612:15)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1151:7-1151:16)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1617:7-1617:15)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1156:7-1156:16)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1622:7-1622:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1161:7-1161:16)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1627:7-1627:16)
[Warning][Deadcode][CWE-570] condition 'T9_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1166:7-1166:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1171:7-1171:17)
[Warning][Deadcode][CWE-570] condition 'T11_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1176:7-1176:17)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:343:9-343:19)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:1181:7-1181:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.11.cil-1.c:351:10-351: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
