./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.04.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.04.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.04.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.04.cil-2.c:73:3-106:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:129:3-142:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:165:3-178:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:201:3-214:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:237:3-250:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:435:3-515:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:815:3-852: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, E_M, 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, tmp_ndt_1, tmp_ndt_2, tmp_ndt_3, tmp_ndt_4, tmp_ndt_5, __retres1, __retres1, __retres1, __retres1, __retres1, __retres1, tmp_var, tmp
[Info] Enabled widening thresholds
[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.04.cil-2.c:87:9-87:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:137:5-137:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:173:5-173:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:209:5-209:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:245:5-245:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:527-527)
  on line 532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:532-532)
  on line 537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:537-537)
  on line 542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:542-542)
  on line 547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:547-547)
  on line 552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:552-552)
  on line 557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:557-557)
  on line 562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:562-562)
  on line 567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:567-567)
  on line 572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:572-572)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:368-368)
  on line 373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:373-373)
  on line 378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:378-378)
  on line 383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:383-383)
  on line 388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:388-388)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:585-585)
  on line 590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:590-590)
  on line 595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:595-595)
  on line 600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:600-600)
  on line 605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:605-605)
  on line 610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:610-610)
  on line 615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:615-615)
  on line 620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:620-620)
  on line 625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:625-625)
  on line 630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:630-630)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:720-720)
  on line 725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:725-725)
  on line 730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:730-730)
  on line 735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:735-735)
  on line 740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:740-740)
  on line 745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:745-745)
  on line 750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:750-750)
  on line 755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:755-755)
  on line 760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:760-760)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 259
  dead: 35
  total lines: 294
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:571:7-571:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:584:7-584:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:589:7-589:16)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:100:17-100:29)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:594:7-594:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:435:10-435:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:599:7-599:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:604:7-604:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:165:10-165:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:121:9-121:19)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:609:7-609:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:815:10-815:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:614:7-614:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:129:10-129:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:619:7-619:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:624:7-624:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:629:7-629:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:237:10-237:11)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:193:9-193:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:201:10-201:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:435:10-435:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:65:9-65:18)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:714:7-714:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:73:10-73:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:719:7-719:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:724:7-724:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:129:10-129:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:729:7-729:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:734:7-734:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:739:7-739:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:744:7-744:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:749:7-749:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:365:7-365:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:201:10-201:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:157:9-157:19)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:754:7-754:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:759:7-759:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:370:7-370:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:165:10-165:11)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:375:7-375:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:526:7-526:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:531:7-531:16)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:380:7-380:16)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:229:9-229:19)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:536:7-536:16)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:385:7-385:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:541:7-541:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:237:10-237:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:546:7-546:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:551:7-551:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:73:10-73:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:556:7-556:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:815:10-815:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:561:7-561:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.04.cil-2.c:566:7-566: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
