./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.05.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.05.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.05.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.05.cil-2.c:79:3-112:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:135:3-148:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:171:3-184:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:207:3-220:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:243:3-256:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:279:3-292:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:940:3-977: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] Enabled octagon domain ONLY for:
[Info] token, immediate_notify, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, __retres1, tmp, tmp___0, tmp, __retres2, tmp, tmp___0, tmp___1, tmp___2, tmp___3, tmp___4, tmp, tmp_ndt_1, tmp_ndt_2, tmp_ndt_3, tmp_ndt_4, tmp_ndt_5, tmp_ndt_6, __retres1, __retres1, __retres1, __retres1, __retres1, __retres1, __retres1, tmp_var, tmp
[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.05.cil-2.c:93:9-93:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:143:5-143:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:179:5-179:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:215:5-215:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:251:5-251:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:287:5-287:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:612-612)
  on line 617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:617-617)
  on line 622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:622-622)
  on line 627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:627-627)
  on line 632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:632-632)
  on line 637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:637-637)
  on line 642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:642-642)
  on line 647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:647-647)
  on line 652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:652-652)
  on line 657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:657-657)
  on line 662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:662-662)
  on line 667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:667-667)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:429-429)
  on line 434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:434-434)
  on line 439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:439-439)
  on line 444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:444-444)
  on line 449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:449-449)
  on line 454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:454-454)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:680-680)
  on line 685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:685-685)
  on line 690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:690-690)
  on line 695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:695-695)
  on line 700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:700-700)
  on line 705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:705-705)
  on line 710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:710-710)
  on line 715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:715-715)
  on line 720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:720-720)
  on line 725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:725-725)
  on line 730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:730-730)
  on line 735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:735-735)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:834-834)
  on line 839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:839-839)
  on line 844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:844-844)
  on line 849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:849-849)
  on line 854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:854-854)
  on line 859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:859-859)
  on line 864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:864-864)
  on line 869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:869-869)
  on line 874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:874-874)
  on line 879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:879-879)
  on line 884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:884-884)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 295
  dead: 42
  total lines: 337
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:828:7-828:15)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:106:17-106:29)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:833:7-833:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:838:7-838:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:843:7-843:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:171:10-171:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:127:9-127:19)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:848:7-848:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:135:10-135:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:853:7-853:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:611:7-611:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:858:7-858:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:616:7-616:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:863:7-863:15)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:621:7-621:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:868:7-868:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:243:10-243:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:626:7-626:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:199:9-199:19)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:873:7-873:15)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:631:7-631:16)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:878:7-878:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:207:10-207:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:636:7-636:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:883:7-883:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:426:7-426:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:641:7-641:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:646:7-646:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:431:7-431:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:651:7-651:15)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:271:9-271:19)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:436:7-436:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:656:7-656:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:279:10-279:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:661:7-661:15)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:441:7-441:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:666:7-666:15)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:446:7-446:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:679:7-679:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:684:7-684:16)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:71:9-71:18)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:451:7-451:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:689:7-689:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:79:10-79:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:940:10-940:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:694:7-694:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:135:10-135:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:699:7-699:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:704:7-704:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:709:7-709:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:714:7-714:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:719:7-719:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:724:7-724:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:207:10-207:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:163:9-163:19)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:729:7-729:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:171:10-171:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:734:7-734:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:940:10-940:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:506:10-506:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:279:10-279:11)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:235:9-235:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:243:10-243:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.05.cil-2.c:79:10-79:11)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
