./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.07.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.07.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.07.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.07.cil-2.c:91:3-124:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:147:3-160:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:183:3-196:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:219:3-232:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:255:3-268:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:291:3-304:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:327:3-340:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:363:3-376:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1190:3-1227: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.07.cil-2.c:105:9-105:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:155:5-155:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:191:5-191:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:227:5-227:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:263:5-263:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:299:5-299:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:335:5-335:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:371:5-371:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:782-782)
  on line 787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:787-787)
  on line 792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:792-792)
  on line 797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:797-797)
  on line 802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:802-802)
  on line 807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:807-807)
  on line 812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:812-812)
  on line 817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:817-817)
  on line 822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:822-822)
  on line 827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:827-827)
  on line 832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:832-832)
  on line 837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:837-837)
  on line 842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:842-842)
  on line 847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:847-847)
  on line 852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:852-852)
  on line 857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:857-857)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:551-551)
  on line 556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:556-556)
  on line 561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:561-561)
  on line 566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:566-566)
  on line 571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:571-571)
  on line 576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:576-576)
  on line 581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:581-581)
  on line 586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:586-586)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:870-870)
  on line 875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:875-875)
  on line 880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:880-880)
  on line 885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:885-885)
  on line 890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:890-890)
  on line 895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:895-895)
  on line 900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:900-900)
  on line 905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:905-905)
  on line 910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:910-910)
  on line 915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:915-915)
  on line 920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:920-920)
  on line 925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:925-925)
  on line 930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:930-930)
  on line 935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:935-935)
  on line 940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:940-940)
  on line 945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:945-945)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 1062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1062-1062)
  on line 1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1067-1067)
  on line 1072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1072-1072)
  on line 1077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1077-1077)
  on line 1082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1082-1082)
  on line 1087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1087-1087)
  on line 1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1092-1092)
  on line 1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1097-1097)
  on line 1102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1102-1102)
  on line 1107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1107-1107)
  on line 1112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1112-1112)
  on line 1117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1117-1117)
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1122-1122)
  on line 1127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1127-1127)
  on line 1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1132-1132)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 367
  dead: 56
  total lines: 423
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:846:7-846:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1096:7-1096:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:851:7-851:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1101:7-1101:15)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:856:7-856:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1106:7-1106:15)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:118:17-118:29)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:869:7-869:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1111:7-1111:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:874:7-874:16)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1116:7-1116:15)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:879:7-879:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1121:7-1121:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:183:10-183:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:139:9-139:19)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:884:7-884:16)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1126:7-1126:15)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:889:7-889:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:147:10-147:11)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1131:7-1131:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:648:10-648:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:894:7-894:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:899:7-899:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:904:7-904:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:255:10-255:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:909:7-909:15)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:211:9-211:19)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:914:7-914:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:219:10-219:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:919:7-919:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:924:7-924:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:929:7-929:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:934:7-934:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:327:10-327:11)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:283:9-283:19)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:939:7-939:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1190:10-1190:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:291:10-291:11)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:944:7-944:15)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:83:9-83:18)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:355:9-355:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:91:10-91:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:363:10-363:11)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:548:7-548:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:147:10-147:11)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:553:7-553:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1190:10-1190:11)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:558:7-558:16)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:563:7-563:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:781:7-781:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:219:10-219:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:175:9-175:19)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:786:7-786:16)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:568:7-568:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:183:10-183:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:791:7-791:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:796:7-796:16)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:573:7-573:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:801:7-801:16)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:578:7-578:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:806:7-806:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:291:10-291:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1056:7-1056:15)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:247:9-247:19)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:811:7-811:16)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:583:7-583:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1061:7-1061:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:816:7-816:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:255:10-255:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1066:7-1066:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:821:7-821:15)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1071:7-1071:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:826:7-826:15)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1076:7-1076:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:91:10-91:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:831:7-831:15)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1081:7-1081:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:363:10-363:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:836:7-836:15)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:319:9-319:19)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1086:7-1086:16)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:841:7-841:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:327:10-327:11)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.07.cil-2.c:1091:7-1091: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
