./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.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.02.cil-2.c:61:3-94:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:117:3-130:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:153:3-166:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:293:3-345:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:565:3-602: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] Setting "ana.int.interval" to true
[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, tmp_ndt_1, tmp_ndt_2, tmp_ndt_3, __retres1, __retres1, __retres1, __retres1, tmp_var, tmp
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:75:9-75:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:125:5-125:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:161:5-161:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:357-357)
  on line 362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:362-362)
  on line 367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:367-367)
  on line 372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:372-372)
  on line 377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:377-377)
  on line 382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:382-382)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:246-246)
  on line 251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:251-251)
  on line 256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:256-256)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:395-395)
  on line 400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:400-400)
  on line 405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:405-405)
  on line 410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:410-410)
  on line 415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:415-415)
  on line 420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:420-420)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:492-492)
  on line 497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:497-497)
  on line 502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:502-502)
  on line 507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:507-507)
  on line 512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:512-512)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 187
  dead: 21
  total lines: 208
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:88:17-88:29)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:153:10-153:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:109:9-109:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:565:10-565:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:117:10-117:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:356:7-356:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:361:7-361:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:366:7-366:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:371:7-371:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:376:7-376:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:381:7-381:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:394:7-394:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:399:7-399:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:404:7-404:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:409:7-409:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:414:7-414:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:419:7-419:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:243:7-243:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:248:7-248:16)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:53:9-53:18)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:253:7-253:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:61:10-61:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:117:10-117:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:486:7-486:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:491:7-491:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:496:7-496:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:293:10-293:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:145:9-145:19)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:501:7-501:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:153:10-153:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:506:7-506:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:511:7-511:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:61:10-61:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:293:10-293:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.02.cil-2.c:565:10-565:11)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
