./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.08.cil-2.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.08.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.08.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.08.cil-2.c:97:3-130:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:153:3-166:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:189:3-202:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:225:3-238:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:261:3-274:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:297:3-310:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:333:3-346:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:369:3-382:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:405:3-418:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1315:3-1352: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.08.cil-2.c:111:9-111:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:161:5-161:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:197:5-197:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:233:5-233:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:269:5-269:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:305:5-305:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:341:5-341:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:377:5-377:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:413:5-413:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:867-867)
  on line 872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:872-872)
  on line 877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:877-877)
  on line 882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:882-882)
  on line 887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:887-887)
  on line 892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:892-892)
  on line 897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:897-897)
  on line 902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:902-902)
  on line 907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:907-907)
  on line 912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:912-912)
  on line 917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:917-917)
  on line 922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:922-922)
  on line 927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:927-927)
  on line 932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:932-932)
  on line 937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:937-937)
  on line 942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:942-942)
  on line 947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:947-947)
  on line 952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:952-952)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:612-612)
  on line 617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:617-617)
  on line 622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:622-622)
  on line 627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:627-627)
  on line 632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:632-632)
  on line 637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:637-637)
  on line 642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:642-642)
  on line 647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:647-647)
  on line 652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:652-652)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:965-965)
  on line 970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:970-970)
  on line 975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:975-975)
  on line 980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:980-980)
  on line 985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:985-985)
  on line 990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:990-990)
  on line 995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:995-995)
  on line 1000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1000-1000)
  on line 1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1005-1005)
  on line 1010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1010-1010)
  on line 1015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1015-1015)
  on line 1020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1020-1020)
  on line 1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1025-1025)
  on line 1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1030-1030)
  on line 1035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1035-1035)
  on line 1040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1040-1040)
  on line 1045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1045-1045)
  on line 1050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1050-1050)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1176-1176)
  on line 1181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1181-1181)
  on line 1186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1186-1186)
  on line 1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1191-1191)
  on line 1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1196-1196)
  on line 1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1201-1201)
  on line 1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1206-1206)
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1211-1211)
  on line 1216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1216-1216)
  on line 1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1221-1221)
  on line 1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1226-1226)
  on line 1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1231-1231)
  on line 1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1236-1236)
  on line 1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1241-1241)
  on line 1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1246-1246)
  on line 1251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1251-1251)
  on line 1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1256-1256)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 403
  dead: 63
  total lines: 466
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1235:7-1235:15)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:994:7-994:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1240:7-1240:15)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:999:7-999:16)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1245:7-1245:15)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1004:7-1004:16)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:124:17-124:29)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:397:9-397:19)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1250:7-1250:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1009:7-1009:15)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1255:7-1255:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1014:7-1014:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:405:10-405:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1019:7-1019:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:189:10-189:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:145:9-145:19)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1024:7-1024:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:153:10-153:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1029:7-1029:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:609:7-609:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1034:7-1034:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1039:7-1039:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:614:7-614:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1044:7-1044:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:261:10-261:11)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:217:9-217:19)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1049:7-1049:15)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:619:7-619:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:225:10-225:11)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:624:7-624:16)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:629:7-629:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1315:10-1315:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:333:10-333:11)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:634:7-634:16)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:289:9-289:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:297:10-297:11)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:639:7-639:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:866:7-866:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:871:7-871:16)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:644:7-644:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:876:7-876:16)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:649:7-649:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:405:10-405:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:89:9-89:18)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:881:7-881:16)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:361:9-361:19)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:886:7-886:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:97:10-97:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:369:10-369:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1315:10-1315:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:891:7-891:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:153:10-153:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:896:7-896:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:901:7-901:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:906:7-906:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:911:7-911:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:916:7-916:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:225:10-225:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:921:7-921:15)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:181:9-181:19)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1170:7-1170:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:926:7-926:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1175:7-1175:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:189:10-189:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:931:7-931:15)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1180:7-1180:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:936:7-936:15)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1185:7-1185:16)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:941:7-941:15)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1190:7-1190:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:946:7-946:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:297:10-297:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1195:7-1195:16)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:253:9-253:19)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:951:7-951:15)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1200:7-1200:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:261:10-261:11)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1205:7-1205:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:964:7-964:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:719:10-719:11)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1210:7-1210:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:969:7-969:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1215:7-1215:15)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:974:7-974:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:97:10-97:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1220:7-1220:15)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:979:7-979:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:369:10-369:11)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:325:9-325:19)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1225:7-1225:15)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:984:7-984:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:333:10-333:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:1230:7-1230:15)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.08.cil-2.c:989:7-989:16)
[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
