./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/token_ring.09.cil-2.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/token_ring.09.cil-2.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.09.cil-2.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.09.cil-2.c:103:3-136:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:159:3-172:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:195:3-208:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:231:3-244:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:267:3-280:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:303:3-316:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:339:3-352:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:375:3-388:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:411:3-424:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:447:3-460:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1440:3-1477: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.09.cil-2.c:117:9-117:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:167:5-167:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:203:5-203:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:239:5-239:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:275:5-275:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:311:5-311:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:347:5-347:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:383:5-383:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:419:5-419:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:455:5-455:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:952-952)
  on line 957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:957-957)
  on line 962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:962-962)
  on line 967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:967-967)
  on line 972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:972-972)
  on line 977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:977-977)
  on line 982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:982-982)
  on line 987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:987-987)
  on line 992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:992-992)
  on line 997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:997-997)
  on line 1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1002-1002)
  on line 1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1007-1007)
  on line 1012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1012-1012)
  on line 1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1017-1017)
  on line 1022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1022-1022)
  on line 1027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1027-1027)
  on line 1032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1032-1032)
  on line 1037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1037-1037)
  on line 1042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1042-1042)
  on line 1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1047-1047)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:673-673)
  on line 678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:678-678)
  on line 683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:683-683)
  on line 688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:688-688)
  on line 693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:693-693)
  on line 698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:698-698)
  on line 703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:703-703)
  on line 708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:708-708)
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:713-713)
  on line 718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:718-718)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 1060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1060-1060)
  on line 1065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1065-1065)
  on line 1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1070-1070)
  on line 1075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1075-1075)
  on line 1080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1080-1080)
  on line 1085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1085-1085)
  on line 1090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1090-1090)
  on line 1095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1095-1095)
  on line 1100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1100-1100)
  on line 1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1105-1105)
  on line 1110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1110-1110)
  on line 1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1115-1115)
  on line 1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1120-1120)
  on line 1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1125-1125)
  on line 1130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1130-1130)
  on line 1135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1135-1135)
  on line 1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1140-1140)
  on line 1145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1145-1145)
  on line 1150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1150-1150)
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1155-1155)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1290-1290)
  on line 1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1295-1295)
  on line 1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1300-1300)
  on line 1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1305-1305)
  on line 1310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1310-1310)
  on line 1315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1315-1315)
  on line 1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1320-1320)
  on line 1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1325-1325)
  on line 1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1330-1330)
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1335-1335)
  on line 1340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1340-1340)
  on line 1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1345-1345)
  on line 1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1350-1350)
  on line 1355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1355-1355)
  on line 1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1360-1360)
  on line 1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1365-1365)
  on line 1370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1370-1370)
  on line 1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1375-1375)
  on line 1380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1380-1380)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 439
  dead: 70
  total lines: 509
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1129:7-1129:15)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1374:7-1374:15)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:695:7-695:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1134:7-1134:15)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1379:7-1379:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1139:7-1139:15)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:700:7-700:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1144:7-1144:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:447:10-447:11)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:130:17-130:29)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:403:9-403:19)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1149:7-1149:15)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:705:7-705:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:411:10-411:11)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1154:7-1154:15)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:710:7-710:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:195:10-195:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:151:9-151:19)
[Warning][Deadcode][CWE-571] condition 't9_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:715:7-715:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:159:10-159:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:951:7-951:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:956:7-956:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:961:7-961:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:267:10-267:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:966:7-966:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:223:9-223:19)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:971:7-971:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1440:10-1440:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:231:10-231:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:976:7-976:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:981:7-981:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:986:7-986:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:991:7-991:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:339:10-339:11)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:295:9-295:19)
[Warning][Deadcode][CWE-570] condition 'T9_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:996:7-996:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:303:10-303:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1001:7-1001:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1006:7-1006:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1011:7-1011:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1440:10-1440:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1016:7-1016:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:411:10-411:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:95:9-95:18)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:367:9-367:19)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1021:7-1021:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:103:10-103:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1026:7-1026:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:375:10-375:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1031:7-1031:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:159:10-159:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:790:10-790:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1284:7-1284:15)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1036:7-1036:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1289:7-1289:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1041:7-1041:15)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1294:7-1294:16)
[Warning][Deadcode][CWE-570] condition 'E_9 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1046:7-1046:15)
[Warning][Deadcode][CWE-571] condition 't9_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:439:9-439:19)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1299:7-1299:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1059:7-1059:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:447:10-447:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1304:7-1304:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1064:7-1064:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:231:10-231:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:187:9-187:19)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1309:7-1309:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1069:7-1069:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1314:7-1314:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:195:10-195:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1074:7-1074:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1319:7-1319:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1079:7-1079:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1324:7-1324:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1084:7-1084:16)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1329:7-1329:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1089:7-1089:16)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:670:7-670:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:303:10-303:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1334:7-1334:15)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:259:9-259:19)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1094:7-1094:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1339:7-1339:15)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1099:7-1099:16)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:675:7-675:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:267:10-267:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1344:7-1344:15)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1104:7-1104:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1349:7-1349:15)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:680:7-680:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1109:7-1109:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1354:7-1354:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:103:10-103:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1114:7-1114:15)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:685:7-685:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1359:7-1359:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:375:10-375:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1119:7-1119:15)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:331:9-331:19)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1364:7-1364:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1124:7-1124:15)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:690:7-690:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:339:10-339:11)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.09.cil-2.c:1369:7-1369:15)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
