./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/float-benchs/zonotope_3.c.v+lhb-reducer.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 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] __return_main, abort, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, main__x, main__i, main__t, main__u, main__v, main____CPAchecker_TMP_0___7, main____CPAchecker_TMP_0___8, main____CPAchecker_TMP_0, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:103:6-103:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:103:6-103:20)
[Warning][Float][CWE-1339] The result of this operation is not exact, even though the inputs were exact (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:105:6-105:46)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:105:6-105:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:105:6-105:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:115:3-115:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:115:3-115:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:122:3-122:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:122:3-122:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:145:6-145:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:145:6-145:20)
[Warning][Float][CWE-1339] The result of this operation is not exact, even though the inputs were exact (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:147:6-147:46)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:147:6-147:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:147:6-147:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:157:3-157:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:157:3-157:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:164:3-164:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:164:3-164:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:187:6-187:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:187:6-187:20)
[Warning][Float][CWE-1339] The result of this operation is not exact, even though the inputs were exact (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:189:6-189:46)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:189:6-189:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:189:6-189:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:199:3-199:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:199:3-199:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:206:3-206:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:206:3-206:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:229:6-229:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:229:6-229:20)
[Warning][Float][CWE-1339] The result of this operation is not exact, even though the inputs were exact (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:231:6-231:46)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:231:6-231:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:231:6-231:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:241:3-241:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:241:3-241:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:248:3-248:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:248:3-248:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:271:6-271:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:271:6-271:20)
[Warning][Float][CWE-1339] The result of this operation is not exact, even though the inputs were exact (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:273:6-273:46)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:273:6-273:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:273:6-273:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:283:3-283:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:283:3-283:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:290:3-290:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:290:3-290:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:313:6-313:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:313:6-313:20)
[Warning][Float][CWE-1339] The result of this operation is not exact, even though the inputs were exact (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:315:6-315:46)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:315:6-315:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:315:6-315:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:325:3-325:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:325:3-325:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:332:3-332:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:332:3-332:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:355:6-355:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:355:6-355:20)
[Warning][Float][CWE-1339] The result of this operation is not exact, even though the inputs were exact (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:357:6-357:46)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:357:6-357:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:357:6-357:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:367:3-367:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:367:3-367:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:374:3-374:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:374:3-374:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:397:6-397:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:397:6-397:20)
[Warning][Float][CWE-1339] The result of this operation is not exact, even though the inputs were exact (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:399:6-399:46)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:399:6-399:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:399:6-399:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:409:3-409:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:409:3-409:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:416:3-416:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:416:3-416:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:439:6-439:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:439:6-439:20)
[Warning][Float][CWE-1339] The result of this operation is not exact, even though the inputs were exact (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:441:6-441:46)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:441:6-441:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:441:6-441:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:451:3-451:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:451:3-451:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:458:3-458:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:458:3-458:34)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:499:3-499:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:499:3-499:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:506:3-506:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:506:3-506:34)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:513:3-513:39)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:513:3-513:39)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:521:3-521:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:521:3-521:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:523:2-523:42)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:486:6-486:20)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:486:6-486:20)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:488:6-488:46)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:488:6-488:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:552:2-552:37)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:552:2-552:37)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:554:6-554:34)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:554:6-554:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:556:6-556:34)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:556:6-556:34)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:7:1-9:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:568-568)
  on line 596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:596-596)
  on line 611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:611-611)
  on line 620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:620-620)
  on line 635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:635-635)
  on line 644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:644-644)
  on line 659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:659-659)
  on line 668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:668-668)
  on line 683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:683-683)
  on line 692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:692-692)
  on line 707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:707-707)
  on line 716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:716-716)
  on line 731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:731-731)
  on line 740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:740-740)
  on line 755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:755-755)
  on line 764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:764-764)
  on line 779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:779-779)
  on line 788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:788-788)
  on line 803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:803-803)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 297
  dead: 21 (2 in uncalled functions)
  total lines: 318
[Warning][Deadcode][CWE-571] condition 'main__i <= 100000' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:183:6-183:23)
[Warning][Deadcode][CWE-571] condition 'main__i <= 100000' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:393:6-393:23)
[Warning][Deadcode][CWE-571] condition 'main____CPAchecker_TMP_0___1 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:192:6-192:35)
[Warning][Deadcode][CWE-571] condition 'main____CPAchecker_TMP_0___6 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:402:6-402:35)
[Warning][Deadcode][CWE-571] condition 'main__i <= 100000' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:225:6-225:23)
[Warning][Deadcode][CWE-571] condition 'main__i <= 100000' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:435:6-435:23)
[Warning][Deadcode][CWE-571] condition 'main____CPAchecker_TMP_0___2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:234:6-234:35)
[Warning][Deadcode][CWE-571] condition 'main____CPAchecker_TMP_0___7 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:444:6-444:35)
[Warning][Deadcode][CWE-571] condition 'main__i <= 100000' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:267:6-267:23)
[Warning][Deadcode][CWE-571] condition 'main____CPAchecker_TMP_0___3 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:276:6-276:35)
[Warning][Deadcode][CWE-571] condition 'main__i <= 100000' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:99:6-99:23)
[Warning][Deadcode][CWE-571] condition 'main____CPAchecker_TMP_0 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:108:6-108:35)
[Warning][Deadcode][CWE-571] condition 'main__i <= 100000' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:309:6-309:23)
[Warning][Deadcode][CWE-571] condition 'main____CPAchecker_TMP_0___4 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:318:6-318:35)
[Warning][Deadcode][CWE-571] condition 'main__i <= 100000' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:141:6-141:23)
[Warning][Deadcode][CWE-571] condition 'main__i <= 100000' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:351:6-351:23)
[Warning][Deadcode][CWE-571] condition 'main____CPAchecker_TMP_0___0 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:150:6-150:35)
[Warning][Deadcode][CWE-571] condition 'main____CPAchecker_TMP_0___5 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-benchs/zonotope_3.c.v+lhb-reducer.c:360:6-360:35)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
