./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.06.cil-1.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.06.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.06.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.06.cil-1.c:85:3-118:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:141:3-154:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:177:3-190:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:213:3-226:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:249:3-262:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:285:3-298:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:321:3-334:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:1065:3-1102: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] Enabled congruence domain.
[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.06.cil-1.c:99:9-99:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:149:5-149:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:185:5-185:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:221:5-221:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:257:5-257:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:293:5-293:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:329:5-329:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:697-697)
  on line 702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:702-702)
  on line 707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:707-707)
  on line 712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:712-712)
  on line 717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:717-717)
  on line 722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:722-722)
  on line 727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:727-727)
  on line 732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:732-732)
  on line 737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:737-737)
  on line 742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:742-742)
  on line 747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:747-747)
  on line 752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:752-752)
  on line 757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:757-757)
  on line 762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:762-762)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:490-490)
  on line 495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:495-495)
  on line 500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:500-500)
  on line 505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:505-505)
  on line 510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:510-510)
  on line 515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:515-515)
  on line 520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:520-520)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:775-775)
  on line 780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:780-780)
  on line 785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:785-785)
  on line 790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:790-790)
  on line 795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:795-795)
  on line 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:800-800)
  on line 805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:805-805)
  on line 810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:810-810)
  on line 815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:815-815)
  on line 820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:820-820)
  on line 825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:825-825)
  on line 830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:830-830)
  on line 835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:835-835)
  on line 840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:840-840)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:948-948)
  on line 953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:953-953)
  on line 958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:958-958)
  on line 963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:963-963)
  on line 968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:968-968)
  on line 973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:973-973)
  on line 978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:978-978)
  on line 983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:983-983)
  on line 988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:988-988)
  on line 993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:993-993)
  on line 998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:998-998)
  on line 1003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:1003-1003)
  on line 1008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:1008-1008)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 331
  dead: 49
  total lines: 380
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:957:7-957:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:711:7-711:16)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:497:7-497:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:962:7-962:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:716:7-716:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:967:7-967:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:721:7-721:16)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:502:7-502:16)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:112:17-112:29)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:972:7-972:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:726:7-726:16)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:507:7-507:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:977:7-977:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:731:7-731:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:982:7-982:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:736:7-736:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:177:10-177:11)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:512:7-512:16)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:133:9-133:19)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:987:7-987:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:741:7-741:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:141:10-141:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:992:7-992:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:746:7-746:15)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:517:7-517:16)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:997:7-997:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:751:7-751:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:1002:7-1002:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:756:7-756:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:1007:7-1007:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:761:7-761:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:249:10-249:11)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:205:9-205:19)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:774:7-774:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:213:10-213:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:779:7-779:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:784:7-784:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:789:7-789:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:794:7-794:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:321:10-321:11)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:277:9-277:19)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:799:7-799:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:804:7-804:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:285:10-285:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:809:7-809:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:814:7-814:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:1065:10-1065:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:819:7-819:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:577:10-577:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:77:9-77:18)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:824:7-824:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:829:7-829:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:85:10-85:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:834:7-834:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:141:10-141:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:839:7-839:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:1065:10-1065:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:213:10-213:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:169:9-169:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:177:10-177:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:285:10-285:11)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:241:9-241:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:249:10-249:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:85:10-85:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:942:7-942:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:696:7-696:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:487:7-487:15)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:313:9-313:19)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:947:7-947:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:701:7-701:16)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:492:7-492:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:321:10-321:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:952:7-952:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.06.cil-1.c:706:7-706: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
