./goblint --conf conf/svcomp23.json --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/loops/vogal-2.i


--------------------------------------------------------------------------------


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:29:3-30:49 with factor 8
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:35:3-36:17 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:6-44:3 with factor 12
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:5-52:5 with factor 12
Collected factors:
functions: 33
functionCalls: 35
loops: 12
loopBreaks: 0
controlFlowStatements: 272
expressions: 1446
instructions: 226
integralVars: (4,42)
arrayVars: (2,2)
pointerVars: (0,14)

Complexity estimates:
File: 3751
no thread creation -> disabeling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn"
Total: 13398
Congruence: 1003
Enabled congruence domain.
Octagon: 3000
Enabled octagon domain for:
__VERIFIER_nondet_char, abort, j, i, n_caracter, cont, cont_aux, top, i, key, count, a, tmp, j, count, k, size, a, b, c, i, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val
Widening: 5644
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:42:12-42:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:42:12-42:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:42:12-42:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:42:12-42:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:42:12-42:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:42:12-42:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:42:12-42:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:42:12-42:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:51:12-51:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:53:5-53:8)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 28
  dead: 0
  total: 28
[Warning][Deadcode][CWE-571] condition 'i < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:29:6-29:19)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'j < 8U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:9-40:21)
[Warning][Deadcode][CWE-571] condition 'i < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:29:6-29:19)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'j < 8U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:9-40:21)
[Warning][Deadcode][CWE-571] condition 'i < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:29:6-29:19)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'i < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:29:6-29:19)
[Warning][Deadcode][CWE-571] condition 'j < 8U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:9-40:21)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'j < 8U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:9-40:21)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'j < 8U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:9-40:21)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'j < 8U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:9-40:21)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-570] condition 'j < 8U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:9-40:21)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:12:73-12:74)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'j < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'i < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:29:6-29:19)
[Warning][Deadcode][CWE-570] condition 'j < 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:48:8-48:21)
[Warning][Deadcode][CWE-571] condition 'i < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:29:6-29:19)
[Warning][Deadcode][CWE-570] condition '(int )string_entrada[n_caracter] != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:35:9-35:41)
[Warning][Deadcode][CWE-571] condition 'i < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:29:6-29:19)
[Warning][Deadcode][CWE-571] condition 'j < 8U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:9-40:21)
[Warning][Deadcode][CWE-571] condition 'i < 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:29:6-29:19)
[Warning][Deadcode][CWE-571] condition 'j < 8U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-2.i:40:9-40:21)
SV-COMP result: unknown
