./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/lu.cmp.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/lu.cmp.c:96:4-101:4 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:125:8-126:32 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:132:8-133:34 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:141:6-142:27 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.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][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:133:10-133:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:126:10-126:32)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:126:10-126:32)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:126:10-126:32)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:126:10-126:32)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:126:10-126:32)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:126:10-126:32)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:126:10-126:32)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:126:10-126:32)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:127:6-127:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:127:6-127:27)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:120:7-120:27)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:120:7-120:27)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:80:7-80:13)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:80:7-80:13)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:81:8-81:14)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:142:8-142:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:145:2-145:23)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:145:2-145:23)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:150:8-150:27)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:151:6-151:25)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:151:6-151:25)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:3:1-3:72)
[Warning][Deadcode] Function '__VERIFIER_assert' has dead code:
  on line 7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:7-7)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 48
  dead: 2 (1 in uncalled functions)
  total: 50
[Warning][Deadcode][CWE-570] condition 'j < i' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:141:9-141:27)
[Warning][Deadcode][CWE-570] condition 'k < i' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:125:11-125:29)
[Warning][Deadcode][CWE-570] condition 'k <= i' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:132:11-132:30)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:96:7-96:26)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:96:7-96:26)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:96:7-96:26)
[Warning][Deadcode][CWE-570] condition 'j <= n' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:96:7-96:26)
[Warning][Deadcode][CWE-570] condition 'n > 99' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:117:5-117:25)
[Warning][Deadcode][CWE-570] condition 'eps <= 0.0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:117:5-117:25)
[Warning][Deadcode][CWE-570] condition '! cond' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:6:7-6:14)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:149:9-149:30)
[Warning][Deadcode][CWE-571] condition 'j < i' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:141:9-141:27)
[Warning][Deadcode][CWE-571] condition 'k <= i' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:132:11-132:30)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:96:7-96:26)
[Warning][Deadcode][CWE-571] condition 'k < i' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:125:11-125:29)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:96:7-96:26)
[Warning][Deadcode][CWE-570] condition 'j <= n' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:149:9-149:30)
[Warning][Deadcode][CWE-571] condition 'j <= n' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/lu.cmp.c:96:7-96:26)
SV-COMP result: true
