./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.03.cil-1.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.03.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.03.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.03.cil-1.c:67:3-100:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:123:3-136:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:159:3-172:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:195:3-208:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:364:3-430:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:690:3-727: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, tmp_ndt_1, tmp_ndt_2, tmp_ndt_3, tmp_ndt_4, __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.03.cil-1.c:81:9-81:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:131:5-131:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:167:5-167:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:203:5-203:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:442-442)
  on line 447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:447-447)
  on line 452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:452-452)
  on line 457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:457-457)
  on line 462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:462-462)
  on line 467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:467-467)
  on line 472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:472-472)
  on line 477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:477-477)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:307-307)
  on line 312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:312-312)
  on line 317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:317-317)
  on line 322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:322-322)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:490-490)
  on line 495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:495-495)
  on line 500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:500-500)
  on line 505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:505-505)
  on line 510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:510-510)
  on line 515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:515-515)
  on line 520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:520-520)
  on line 525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:525-525)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:606-606)
  on line 611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:611-611)
  on line 616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:616-616)
  on line 621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:621-621)
  on line 626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:626-626)
  on line 631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:631-631)
  on line 636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:636-636)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 223
  dead: 28
  total lines: 251
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:446:7-446:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:451:7-451:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:456:7-456:16)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:304:7-304:15)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:94:17-94:29)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:461:7-461:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:466:7-466:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:309:7-309:16)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:471:7-471:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:159:10-159:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:115:9-115:19)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:476:7-476:15)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:314:7-314:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:690:10-690:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:123:10-123:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:489:7-489:15)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:319:7-319:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:494:7-494:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:499:7-499:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:504:7-504:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:187:9-187:19)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:509:7-509:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:514:7-514:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:195:10-195:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:519:7-519:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:524:7-524:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:364:10-364:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:59:9-59:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:67:10-67:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:123:10-123:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:600:7-600:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:605:7-605:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:610:7-610:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:615:7-615:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:620:7-620:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:364:10-364:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:195:10-195:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:625:7-625:15)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:151:9-151:19)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:630:7-630:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:159:10-159:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:635:7-635:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:67:10-67:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:690:10-690:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.03.cil-1.c:441:7-441: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
