./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/float_req_bl_0870a.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/float_req_bl_0870a.yml/witness.yml --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/float-newlib/float_req_bl_0870a.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 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:22:3-26:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:27:3-31:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:43:5-44:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:49:5-50:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:67:3-76:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:84:3-87:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:90:5-94:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:99:5-103:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:116:3-120:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:133:5-134:15 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:147:3-156:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:170:3-174:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:179:3-183:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:184:3-188:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:189:3-193:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:205:3-209:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:218:5-222:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:231:5-235:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:245:3-249:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:254:3-258:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:259:3-263:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:303:3-307:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:308:3-312:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:387:5-391:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:392:5-396:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:405:7-409:18 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:424:5-428:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:433:5-437:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:438:5-442:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:443:5-447:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:458:5-462:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:463:5-467:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:472:5-476:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:477:5-481:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:488:5-492:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:493:5-497:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:503:3-507:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:508:3-512:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:516:3-520:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:541:5-545:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:552:3-556:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:557:3-561:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:571:3-575:14 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:580:5-584:16 with factor 12
[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] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] math function -> enabling tmpSpecial analysis and floating-point domain
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:603:7-603:16)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:603:7-603:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:306:6-306:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:311:6-311:21)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:330:7-330:28)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:330:7-330:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:331:7-331:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:331:7-331:25)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:332:12-332:32)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:332:12-332:32)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:343:15-343:38)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:347:14-347:25)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:352:12-352:17)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:352:12-352:17)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:119:6-119:21)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:121:3-121:23)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:124:12-124:21)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:124:12-124:21)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:129:13-129:29)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:129:13-129:29)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:131:3-131:17)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:134:7-134:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:133:9-133:45)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:135:5-135:15)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:137:3-137:11)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:138:3-138:40)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:140:5-140:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:141:3-141:10)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:143:3-143:11)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:154:5-154:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:154:5-154:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:154:5-154:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:154:5-154:13)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:148:5-148:14)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:148:5-148:14)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:148:5-148:14)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:150:7-150:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:150:7-150:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:150:7-150:16)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:151:7-151:14)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:152:7-152:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:152:7-152:13)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:152:7-152:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:154:5-154:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:155:5-155:12)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:160:9-160:22)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:162:11-162:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:163:9-163:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:165:9-165:21)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:168:3-168:30)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:168:3-168:30)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:169:3-169:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:172:5-172:21)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:363:7-363:22)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:366:9-366:30)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:366:9-366:30)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:368:9-368:15)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:373:10-373:51)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:373:10-373:51)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:374:13-374:29)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:374:13-374:29)
[Warning][Float][CWE-1339] The result of this operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:378:15-378:66)
[Warning][Float][CWE-1339] The result of this operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:380:15-380:66)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:382:5-382:15)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:383:5-383:79)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:383:5-383:79)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:384:5-384:24)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:385:5-385:40)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:385:5-385:40)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:386:5-386:15)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:386:5-386:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:390:8-390:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:394:7-394:36)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:397:5-397:22)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:397:5-397:22)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:403:7-403:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:408:10-408:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:411:5-411:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:411:5-411:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:422:7-422:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:426:7-426:23)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:429:5-429:23)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:430:5-430:35)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:430:5-430:35)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:431:5-431:14)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:431:5-431:14)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:436:8-436:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:440:7-440:36)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:445:7-445:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:445:7-445:69)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:445:7-445:69)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:448:5-448:33)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:448:5-448:33)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:449:5-449:44)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:449:5-449:44)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:450:5-450:15)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:450:5-450:15)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:451:5-454:77)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:451:5-454:77)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:455:5-455:25)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:455:5-455:25)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:456:5-456:19)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:456:5-456:19)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:457:5-457:30)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:457:5-457:30)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:461:8-461:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:465:7-465:36)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:468:5-468:40)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:468:5-468:40)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:469:5-469:18)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:469:5-469:18)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:470:5-470:28)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:470:5-470:28)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:471:5-471:16)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:471:5-471:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:475:8-475:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:479:7-479:36)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:482:5-482:24)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:482:5-482:24)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:483:5-483:25)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:484:5-484:50)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:484:5-484:50)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:487:5-487:43)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:487:5-487:43)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:491:8-491:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:495:7-495:36)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:498:5-498:48)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:498:5-498:48)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:501:10-501:57)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:501:10-501:57)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:506:6-506:21)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:510:5-510:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:513:3-513:31)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:513:3-513:31)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:513:3-513:31)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:514:3-514:16)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:514:3-514:16)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:515:3-515:16)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:515:3-515:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:519:6-519:20)
[Warning][Float][CWE-1339] The result of this operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:524:14-524:37)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:526:11-526: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-newlib/float_req_bl_0870a.c:526:11-526:34)
[Warning][Float][CWE-189][CWE-739] First operand of comparison is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:526:11-526:34)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:526:11-526:34)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:532:11-532:25)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:532:11-532:25)
[Warning][Float][CWE-189][CWE-739] First operand of comparison is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:532:11-532:25)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:532:11-532:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:536:3-536:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:536:3-536:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:539:5-539:36)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:540:5-540:40)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:540:5-540:40)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:543:7-543:43)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:543:7-543:43)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:546:5-546:52)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:546:5-546:52)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:548:7-548:13)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:549:5-549:13)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:549:5-549:13)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:551:3-551:16)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:551:3-551:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:555:6-555:21)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:559:5-559: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-newlib/float_req_bl_0870a.c:562:3-562:20)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:563:3-563:50)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:563:3-563:50)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:563:3-563:50)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:564:3-564:12)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:564:3-564:12)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:565:3-565:18)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:565:3-565:18)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:565:3-565:18)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:566:3-566:12)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:566:3-566:12)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:567:3-568:78)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:567:3-568:78)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:569:3-569:46)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:569:3-569:46)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:570:3-570:24)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:570:3-570:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:574:6-574:20)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:576:3-576:17)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:577:8-577:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:208:6-208:21)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:210:3-210:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:211:3-211:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:211:3-211:15)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:215:12-215:17)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:215:12-215:17)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:217:5-217:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:221:8-221:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:223:5-223:39)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:223:5-223:39)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation is Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:225:14-225:29)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:227:3-227:12)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:229:12-229:56)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:233:7-233:50)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:240:14-240:58)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:242:14-242:58)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:247:5-247:48)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:250:10-250:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:582:7-582:22)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:585:10-585:15)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:589:35-589:41)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:589:35-589:41)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:589:35-589:41)
[Warning][Deadcode] Function 'fmod_float' is uncalled: 59 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:19:1-107:1)
[Warning][Deadcode] Function '__ieee754_powf' has dead code:
  on line 527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:527-527)
  on line 533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:533-533)
[Warning][Deadcode] Function 'main' has dead code:
  on line 610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:610-610)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 309
  dead: 62 (59 in uncalled functions)
  total lines: 371
[Warning][Deadcode][CWE-570] condition 'p_l + (float )ovt_pow > z - p_h' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:526:11-526:34)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:507:12-507:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:183:12-183:14)
[Warning][Deadcode][CWE-570] condition 'p_l <= z - p_h' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:532:11-532:25)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:307:12-307:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:545:14-545:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:249:12-249:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:391:14-391:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:120:12-120:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:575:12-575:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:447:14-447:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:428:14-428:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:193:12-193:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:497:14-497:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:476:14-476:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:520:12-520:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:174:12-174:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:235:14-235:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:263:12-263:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:561:12-561:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:409:16-409:18)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:442:14-442:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:467:14-467:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:512:12-512:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:188:12-188:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:492:14-492:16)
[Warning][Deadcode][CWE-571] condition 'r != 0U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:147:10-147:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:222:14-222:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:312:12-312:14)
[Warning][Deadcode][CWE-571] condition 'r != 0U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:147:10-147:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:396:14-396:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:258:12-258:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:556:12-556:14)
[Warning][Deadcode][CWE-571] condition 'r != 0U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:147:10-147:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:584:14-584:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:209:12-209:14)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:481:14-481:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:437:14-437:16)
[Warning][Deadcode][CWE-571] condition 'r != 0U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:147:10-147:16)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/float-newlib/float_req_bl_0870a.c:462:14-462:16)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
