./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-1.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-1.i:33:3-34:47 with factor 8
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:38:3-39:17 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:43:6-47: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-1.i:51:5-55:5 with factor 12
Collected factors:
functions: 34
functionCalls: 36
loops: 12
loopBreaks: 0
controlFlowStatements: 276
expressions: 1453
instructions: 226
integralVars: (4,43)
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: 13489
Congruence: 1026
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: 5712
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-1.i:45:12-45:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:45:12-45:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:54:12-54:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:54:12-54:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:56:5-56:8)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:15:1-17:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 28
  dead: 2 (2 in uncalled functions)
  total: 30
[Warning][Deadcode][CWE-571] condition 'j < 2U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:43:9-43:23)
[Warning][Deadcode][CWE-571] condition 'i < 5U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:33:6-33:18)
[Warning][Deadcode][CWE-571] condition 'j < 2U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:51:8-51:22)
[Warning][Deadcode][CWE-570] condition 'j < 2U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:43:9-43:23)
[Warning][Deadcode][CWE-570] condition 'i < 5U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:33:6-33:18)
[Warning][Deadcode][CWE-571] condition 'j < 2U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:51:8-51:22)
[Warning][Deadcode][CWE-570] condition 'j < 2U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:51:8-51:22)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:12:73-12:74)
[Warning][Deadcode][CWE-570] condition '(int )input_string[n_caracter] != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:38:9-38:39)
[Warning][Deadcode][CWE-571] condition 'i < 5U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:33:6-33:18)
[Warning][Deadcode][CWE-571] condition 'i < 5U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:33:6-33:18)
[Warning][Deadcode][CWE-571] condition 'i < 5U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:33:6-33:18)
[Warning][Deadcode][CWE-571] condition 'j < 2U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:43:9-43:23)
[Warning][Deadcode][CWE-571] condition 'i < 5U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/vogal-1.i:33:6-33:18)
SV-COMP result: unknown
