./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.01.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.01.cil-2.c:55:3-88:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:111:3-124:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:222:3-260:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:440:3-477: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, pthreadMutexType"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] token, m_st, 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, tmp_ndt_1, tmp_ndt_2, __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.01.cil-2.c:69:9-69:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:119:5-119:15)
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:21-21)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:272-272)
  on line 277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:277-277)
  on line 282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:282-282)
  on line 287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:287-287)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:185-185)
  on line 190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:190-190)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:300-300)
  on line 305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:305-305)
  on line 310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:310-310)
  on line 315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:315-315)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:378-378)
  on line 383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:383-383)
  on line 388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:388-388)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 151
  dead: 14
  total lines: 165
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:222:10-222:11)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:82:17-82:29)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:440:10-440:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:103:9-103:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:222:10-222:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:111:10-111:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:440:10-440:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:222:10-222:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:47:9-47:18)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:271:7-271:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:55:10-55:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:276:7-276:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:111:10-111:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:281:7-281:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:286:7-286:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:299:7-299:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:304:7-304:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:309:7-309:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:314:7-314:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:182:7-182:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:187:7-187:16)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:372:7-372:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:377:7-377:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:382:7-382:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:55:10-55:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/token_ring.01.cil-2.c:387:7-387:15)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
