./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/hardness_fillercode_fillercodesize_ps-cn-250_file-73.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/hardness_fillercode_fillercodesize_ps-cn-250_file-73.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/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i


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


[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/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:465:2-471:2 with factor 3
[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] function step uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]   "up":
[Info]     main
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] var_1_38, var_1_37, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, tmp, tmp___7, tmp___12, tmp___19, tmp___6, tmp___14, tmp___18, tmp___0, tmp___1, tmp, tmp___0, tmp___1, tmp___2, tmp___3, tmp___6, tmp___7, tmp___8, tmp___0, tmp___4, tmp___10, tmp___11, tmp___19, tmp___22, tmp___23, tmp___33, cond, cond
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:343:2-343:130)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:343:2-343:130)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:343:2-343:130)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:343:2-343:130)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:343:2-343:130)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:343:2-343:130)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:343:2-343:130)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:343:2-343:130)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:345:2-345:130)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:345:2-345:130)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:345:2-345:130)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:345:2-345:130)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:345:2-345:130)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:345:2-345:130)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:345:2-345:130)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:345:2-345:130)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:347:2-347:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:347:2-347:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:347:2-347:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:347:2-347:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:347:2-347:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:347:2-347:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:347:2-347:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:347:2-347:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:348:2-348:38)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:348:2-348:38)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:350:2-350:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:350:2-350:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:350:2-350:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:350:2-350:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:350:2-350:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:350:2-350:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:350:2-350:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:350:2-350:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:351:2-351:38)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:351:2-351:38)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:356:2-356:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:356:2-356:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:356:2-356:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:356:2-356:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:356:2-356:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:356:2-356:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:356:2-356:152)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:356:2-356:152)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:385:2-385:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:385:2-385:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:385:2-385:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:385:2-385:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:385:2-385:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:385:2-385:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:385:2-385:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:385:2-385:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:387:2-387:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:387:2-387:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:387:2-387:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:387:2-387:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:387:2-387:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:387:2-387:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:387:2-387:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:387:2-387:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:389:2-389:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:389:2-389:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:389:2-389:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:389:2-389:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:389:2-389:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:389:2-389:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:389:2-389:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:389:2-389:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:421:2-421:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:421:2-421:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:421:2-421:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:421:2-421:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:421:2-421:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:421:2-421:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:421:2-421:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:421:2-421:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:423:2-423:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:423:2-423:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:423:2-423:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:423:2-423:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:423:2-423:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:423:2-423:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:423:2-423:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:423:2-423:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:425:2-425:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:425:2-425:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:425:2-425:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:425:2-425:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:425:2-425:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:425:2-425:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:425:2-425:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:425:2-425:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:427:2-427:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:427:2-427:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:427:2-427:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:427:2-427:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:427:2-427:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:427:2-427:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:427:2-427:156)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:427:2-427:156)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:450:2-450:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:450:2-450:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:450:2-450:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:450:2-450:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:450:2-450:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:450:2-450:134)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:450:2-450:134)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:450:2-450:134)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:126:11-126:109)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:126:11-126:109)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:126:11-126:109)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:126:11-126:109)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:126:11-126:109)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:126:11-126:109)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:126:11-126:109)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:126:11-126:109)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:126:11-126:109)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:127:3-127:95)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:131:7-131:93)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:139:3-139:35)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:185:6-185:26)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:185:6-185:26)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:185:6-185:26)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:196:3-196:62)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:196:3-196:62)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:196:3-196:62)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:198:3-198:115)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:198:3-198:115)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:198:3-198:115)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:198:3-198:115)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:198:3-198:115)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:198:3-198:115)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:198:3-198:115)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:198:3-198:115)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:201:7-201:26)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:201:7-201:26)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:201:7-201:26)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:204:4-204:150)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:204:4-204:150)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:204:4-204:150)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:204:4-204:150)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:204:4-204:150)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:204:4-204:150)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:204:4-204:150)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:204:4-204:150)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:204:4-204:150)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:208:4-208:36)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:208:4-208:36)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:218:6-218:25)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:218:6-218:25)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:218:6-218:25)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:242:6-242:21)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:242:6-242:21)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:245:2-245:61)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:268:3-268:35)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:268:3-268:35)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:275:5-275:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:286:2-286:21)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:289:3-289:22)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:298:3-298:62)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:298:3-298:62)
[Warning][Float][CWE-189][CWE-739] Operand of unary expression could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:298:3-298:62)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:305:6-305:92)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:305:6-305:92)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:305:6-305:92)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:305:6-305:92)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:305:6-305:92)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:305:6-305:92)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:305:6-305:92)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:305:6-305:92)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:314:6-314:44)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:314:6-314:44)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:314:6-314:44)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:314:6-314:44)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:318:6-318:23)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:318:6-318:23)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:318:6-318:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:324:18-324:52)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:328:6-328:35)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:328:6-328:35)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:328:6-328:35)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:328:6-328:35)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:328:6-328:35)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] Second operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:302:11-302:121)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:314:6-314:44)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:472-472)
[Warning][Deadcode] Function 'step' has dead code:
  on line 135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:135-135)
  on lines 142..143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:142-143)
  on line 149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:149-149)
  on line 151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:151-151)
  on lines 235..236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:235-236)
  on line 238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:238-238)
  on line 247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:247-247)
  on line 251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:251-251)
  on line 295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:295-295)
  on line 335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:335-335)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 267
  dead: 13
  total lines: 280
[Warning][Deadcode][CWE-570] condition 'var_1_40 < -10000000L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:141:6-141:26)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:465:9-465:10)
[Warning][Deadcode][CWE-570] condition '(int )var_1_37 < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:174:5-174:151)
[Warning][Deadcode][CWE-571] condition 'var_1_55' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:288:6-288:14)
[Warning][Deadcode][CWE-571] condition '(int )var_1_32 < tmp___41' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:174:5-174:151)
[Error][Analyzer][Unsound] both branches over condition '(long )(5 % (int )var_1_37) < var_1_46' are dead (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:148:9-148:33)
[Warning][Deadcode][CWE-571] condition '(int )var_1_44 < (int )var_1_37' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:215:3-215:69)
[Warning][Deadcode][CWE-571] condition 'var_1_55' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:292:7-292:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:465:9-465:10)
[Warning][Deadcode][CWE-570] condition '(int )var_1_37 < -1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:160:3-160:259)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:465:9-465:10)
[Warning][Deadcode][CWE-571] condition 'tmp___10 - (int )var_1_32 < tmp___11' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:160:3-160:259)
[Warning][Deadcode][CWE-570] condition '(int )var_1_37 < -1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:160:3-160:259)
[Warning][Deadcode][CWE-571] condition 'var_1_55' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:232:7-232:15)
[Warning][Deadcode][CWE-570] condition '! var_1_53' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:191:3-191:40)
[Warning][Deadcode][CWE-571] condition '(long )(~ ((int )var_1_37)) < var_1_47' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:193:3-193:71)
[Warning][Deadcode][CWE-570] condition '(int )var_1_39 < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:162:3-162:349)
[Warning][Deadcode][CWE-570] condition 'var_1_54' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:193:3-193:71)
[Warning][Deadcode][CWE-570] condition '! var_1_55' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:193:3-193:71)
[Warning][Deadcode][CWE-570] condition '(int )var_1_18 < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:317:2-317:61)
[Warning][Deadcode][CWE-570] condition '(int )var_1_39 < 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:162:3-162:349)
[Warning][Deadcode][CWE-571] condition 'var_1_53' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:243:3-243:64)
[Warning][Deadcode][CWE-570] condition 'var_1_54' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:243:3-243:64)
[Warning][Deadcode][CWE-571] condition 'var_1_55' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:243:3-243:64)
[Warning][Deadcode][CWE-570] condition 'var_1_68' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:243:3-243:64)
[Warning][Deadcode][CWE-570] condition 'tmp___50 < 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:195:13-195:200)
[Warning][Deadcode][CWE-570] condition '(int )var_1_39 < 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:162:3-162:349)
[Warning][Deadcode][CWE-570] condition '2UL >= tmp___12' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Deadcode][CWE-570] condition '(int )var_1_37 < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:245:2-245:61)
[Warning][Deadcode][CWE-570] condition '(int )var_1_39 < 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:162:3-162:349)
[Warning][Deadcode][CWE-570] condition '(int )var_1_18 < 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:459:18-460:1)
[Warning][Deadcode][CWE-570] condition 'var_1_54' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:246:6-246:14)
[Warning][Deadcode][CWE-570] condition 'var_1_52' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:250:8-250:16)
[Warning][Deadcode][CWE-570] condition '(int )var_1_74 - (int )var_1_71 < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:253:5-253:97)
[Warning][Deadcode][CWE-570] condition '200 < (int )var_1_38' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:167:5-167:361)
[Warning][Deadcode][CWE-570] condition 'tmp___38 < 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:167:5-167:361)
[Warning][Deadcode][CWE-570] condition '24.6 < (double )0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:202:4-202:141)
[Warning][Deadcode][CWE-570] condition 'tmp___54 < (double )0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:202:4-202:141)
[Warning][Deadcode][CWE-570] condition '200 < (int )var_1_38' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:167:5-167:361)
[Warning][Deadcode][CWE-571] condition '(int )var_1_32 != (int )var_1_37' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:132:7-132:27)
[Warning][Deadcode][CWE-570] condition '(int )var_1_38 < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:133:4-133:177)
[Warning][Deadcode][CWE-570] condition '(int )var_1_78 - (int )var_1_37 < (int )var_1_44' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:266:2-266:94)
[Warning][Deadcode][CWE-570] condition '2UL >= tmp___71' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:334:7-334:66)
[Warning][Deadcode][CWE-570] condition '(int )var_1_37 < tmp___37' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:167:5-167:361)
[Warning][Deadcode][CWE-570] condition '24.6 < (double )0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:202:4-202:141)
[Warning][Deadcode][CWE-570] condition 'tmp___4 < 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:133:4-133:177)
[Warning][Deadcode][CWE-570] condition '200 < (int )var_1_38' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:167:5-167:361)
[Warning][Deadcode][CWE-570] condition 'tmp___33 < 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:167:5-167:361)
[Warning][Deadcode][CWE-570] condition '(int )var_1_38 < 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:133:4-133:177)
[Warning][Deadcode][CWE-571] condition 'var_1_55' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:271:7-271:15)
[Warning][Deadcode][CWE-570] condition '0 > (int )var_1_39 + (int )var_1_71' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:273:5-273:83)
[Warning][Deadcode][CWE-570] condition '200 < (int )var_1_38' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:167:5-167:361)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.i:465:9-465:10)
[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
[Error][Analyzer][Unsound] Both branches dead
