./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/ludcmp.c


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


--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/ludcmp.c:96:4-101:4 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:125:8-126:32 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:132:8-133:34 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:141:6-142:27 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:149:6-150:27 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
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
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
Collected factors:
functions: 35
functionCalls: 28
loops: 17
loopBreaks: 0
controlFlowStatements: 270
expressions: 1825
instructions: 269
integralVars: (4,45)
arrayVars: (5,1)
pointerVars: (0,14)

Complexity estimates:
File: 5982
no thread creation -> disabeling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn"
Total: 16235
Congruence: 1218
Enabled congruence domain.
Octagon: 3000
Enabled octagon domain for:
a, x, j, w, i, k, n, y, eps, tmp, j, i, n, w, nmax, eps, n, f, top, i, key, count, a___0, tmp, j, count, k, size, a___0, b___0, 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: 6035
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Deadcode] Function 'fabs' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:76:1-83:1)
[Warning][Deadcode] Function 'ludcmp' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:111:1-155:1)
[Warning][Deadcode] Function '__VERIFIER_assert' has dead code:
  on line 9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:9-9)
[Warning][Deadcode] Function 'main' has dead code:
  on line 103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:103-103)
  on line 106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:106-106)
  on line 108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:108-108)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 14
  dead: 34 (30 in uncalled functions)
  total: 48
[Warning][Deadcode][CWE-570] condition 'i == j' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:99:9-99:15)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:96:7-96:26)
[Warning][Deadcode][CWE-570] condition 'i == j' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:99:9-99:15)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:96:7-96:26)
[Warning][Deadcode][CWE-570] condition 'i == j' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:99:9-99:15)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:96:7-96:26)
[Warning][Deadcode][CWE-570] condition 'i == j' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:99:9-99:15)
[Warning][Deadcode][CWE-570] condition 'j <= n' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:96:7-96:26)
[Warning][Deadcode][CWE-571] condition '! cond' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:6:7-6:14)
[Warning][Deadcode][CWE-571] condition 'i <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:93:5-93:24)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:96:7-96:26)
[Warning][Deadcode][CWE-571] condition 'i == j' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:99:9-99:15)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:96:7-96:26)
[Warning][Deadcode][CWE-570] condition 'i == j' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:99:9-99:15)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/ludcmp.c:96:7-96:26)
SV-COMP result: unknown
