Tool ESBMC version 6.0.0 64-bit x86_64 linux CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon004; apollon069; apollon137; apollon154] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 02:16:29 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i 1 25     25     93 350    .85 0   1 51    49    350 0     0   1 35     29     680   .68 0   1 3.6  2.1  250 0   0    1 .60   .60   20    .053 .0041 - -
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i 1 33     33     93 440    .85 0   1 12    10    350 0     0   0 97     91     700   1.8  0   1 3.7  2.1  250 0   0    1 .58   .58   20    .053 0      - -
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i 1 41     41     92 520    1.0  0   1 41    39    350 0     0   1 70     65     700   .68 0   1 3.8  2.2  250 0   0    1 .57   .57   20    .053 0      - -
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i 1 8.8   8.8   92 120    1.0  0   1 12    9.8  350 0     0   0 97     91     700   1.7  0   1 3.6  2.1  250 0   0    1 .60   .60   20    .053 0      - -
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i 1 39     39     91 460    1.0  0   1 11    9.5  350 0     0   1 26     21     680   .71 0   1 3.5  2.0  250 0   0    1 .58   .58   20    .053 0      - -
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i 1 130     130     190 1700    1.0  0   -32 4.6  2.6  250 0     0   0 97     91     790   2.3  0   1 3.6  2.2  240 0   0    1 .57   .57   20    .053 0      - -
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i 1 120     120     190 1400    .85 0   -32 4.1  2.3  250 0     0   0 97     90     800   1.9  0   1 3.6  2.1  250 0   0    1 .58   .58   20    .053 0      - -
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i 1 61     61     190 730    1.0  0   -32 4.0  2.2  250 0     0   1 38     32     820   .68 0   1 3.6  2.1  250 0   0    1 .59   .59   20    .053 0      - -
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i 1 100     100     290 1400    .85 0   -32 4.3  2.4  250 0     0   0 97     91     880   1.7  0   1 3.7  2.1  250 0   0    1 .61   .61   20    .053 0      - -
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i 1 120     120     280 1500    1.0  0   -32 4.3  2.4  250 0     0   1 55     49     910   .68 0   1 3.6  2.1  250 0   0    1 .57   .57   20    .053 0      - -
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i 1 130     130     300 1600    1.0  0   -32 4.5  2.5  250 0     0   0 97     90     930   1.9  0   1 3.6  2.1  250 0   0    1 .61   .61   20    .053 0      - -
floats-cdfpl/sine_1_false-unreach-call_true-termination.i 1 20     20     64 280    1.0  0   -32 4.0  2.2  250 0     0   0 97     91     590   1.0  0   1 3.5  2.1  250 0   0    1 .58   .58   20    .049 0      - -
floats-cdfpl/sine_2_false-unreach-call_true-termination.i 1 20     20     64 300    .85 0   -32 3.5  2.0  250 0     0   0 97     92     580   .98 0   1 3.5  2.0  250 0   0    1 .57   .57   20    .049 0      - -
floats-cdfpl/sine_3_false-unreach-call_true-termination.i 1 19     19     64 240    1.0  0   -32 4.2  2.4  250 0     0   0 97     92     600   2.1  0   1 3.6  2.1  250 0   0    1 .57   .57   20    .049 .0041 - -
floats-cdfpl/square_1_false-unreach-call_true-termination.i 1 4.7   4.7   57 55    .85 0   -32 3.7  2.1  250 0     0   0 96     90     460   .68 0   1 3.4  2.0  250 0   0    1 .61   .61   20    .049 .0041 - -
floats-cdfpl/square_2_false-unreach-call_true-termination.i 1 6.8   6.8   55 78    1.0  0   -32 4.0  2.2  250 0     0   0 97     91     440   1.7  0   1 3.5  2.1  240 0   0    1 .57   .57   20    .049 0      - -
floats-cdfpl/square_3_false-unreach-call_true-termination.i 1 7.5   7.5   55 95    1.0  0   -32 3.9  2.1  250 0     0   0 97     91     470   1.6  0   1 3.6  2.1  250 0   0    1 .57   .57   20    .049 0      - -
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i 2 36     36     93 480    1.0  0   - - - - 0 900    900    580 0   0     0 960     950     950   .75 0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i 2 39     39     94 570    1.0  0   - - - - 0 900    900    580 0   0     0 960     950     780   .72 0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i 2 44     44     93 650    1.0  0   - - - - 0 900    900    570 0   0     0 960     950     970   .73 0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i 2 160     160     190 1900    1.0  0   - - - - 0 900    900    520 0   0     0 960     950     900   .70 0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i 2 170     170     190 2000    1.0  0   - - - - 0 900    900    810 0   0     0 960     950     970   .74 0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i 2 160     160     190 1800    1.0  0   - - - - 0 900    900    520 0   0     0 960     950     990   .78 0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i 2 160     160     190 2100    .85 0   - - - - 0 900    900    580 0   0     0 960     950     1000   .73 0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i 2 180     180     190 2100    1.0  0   - - - - 0 900    900    530 0   0     0 960     950     880   .73 0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i 2 450     450     290 5100    .85 0   - - - - 0 900    900    590 0   0     0 960     950     1100   2.0  0     
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i 2 700     700     300 11000    1.0  0   - - - - 0 900    900    560 0   0     0 960     950     1000   1.6  0     
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i 2 460     460     300 6500    .85 0   - - - - 0 900    900    680 0   0     0 960     950     1100   .72 0     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i 2 630     630     300 7000    .85 0   - - - - 0 900    900    700 0   0     0 960     950     1000   .72 0     
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i 2 620     620     310 6000    1.0  0   - - - - 0 900    900    560 0   0     0 960     950     1000   1.9  0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i 2 34     34     64 450    1.0  0   - - - - 0 900    900    500 0   0     0 960     950     790   .81 0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i 2 17     17     64 220    1.0  0   - - - - 0 900    900    490 0   0     0 960     950     830   .73 0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i 2 20     20     64 300    1.0  0   - - - - 0 900    900    650 0   0     0 960     950     820   1.8  0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i 2 14     14     64 150    1.0  0   - - - - 2 790    790    590 0   0     0 960     950     850   .71 0     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i 2 17     17     63 220    1.0  0   - - - - 2 570    570    540 0   0     0 960     950     810   .74 0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i 2 29     29     57 330    .85 0   - - - - 2 680    680    570 0   0     0 960     950     670   1.8  0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i 2 13     13     59 180    .85 0   - - - - 2 530    530    510 0   0     0 960     950     760   1.4  0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i 2 12     12     55 180    1.0  0   - - - - 2 290    280    500 0   0     0 960     950     760   1.7  0     
floats-cdfpl/square_7_true-unreach-call_true-termination.i 2 7.1   7.1   61 110    1.0  0   - - - - 0 900    900    480 0   0     2 620     620     780   .71 0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i 2 5.5   5.5   62 71    1.0  0   - - - - 2 67    65    360 0   0     2 83     78     610   .71 0     
floats-cbmc-regression/float-div1_true-unreach-call.i 2 3.2   3.2   68 42    1.0  0   - - - - 2 5.9  3.7  320 0   0     2 44     38     950   .68 0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 2 .14  .14  28 1.5  1.0  0   - - - - 2 11    8.8  780 0   0     0 14     8.0   290   .75 0     
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i 2 .075 .076 26 .90 1.0  0   - - - - 2 3.7  2.1  250 0   0     2 15     9.1   300   .75 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 2 1.8   1.8   36 27    1.0  0   - - - - 2 19    17    300 0   0     2 57     48     530   .71 0     
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i 2 .080 .082 26 1.1  1.0  0   - - - - 2 3.9  2.2  250 0   0     2 13     7.4   300   .75 0     
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 2 .14  .14  27 1.4  1.0  0   - - - - 2 5.1  2.8  270 0   0     2 20     11     450   .75 0     
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i 2 .10  .10  26 .79 .85 0   - - - - 2 3.9  2.1  250 0   0     2 17     10     300   .75 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i 2 .085 .085 26 .74 1.0  0   - - - - 2 4.4  2.5  250 0   0     2 16     9.7   300   .75 0     
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 .087 .087 26 .88 1.0  0   - - - - 2 4.3  2.4  250 0   .033 0 16     8.8   290   .75 0     
floats-cbmc-regression/float-rounding1_true-unreach-call.i 2 .14  .14  27 1.6  1.0  0   - - - - 0 4.8  2.6  260 0   0     0 6.4   3.5   280   .65 0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i 2 .28  .28  27 3.1  .85 0   - - - - 2 5.3  3.0  260 0   0     2 36     28     460   .71 0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i 2 .094 .097 26 .71 .85 0   - - - - 2 3.5  2.0  250 0   0     2 12     7.2   300   .75 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i 2 .085 .087 26 .86 1.0  0   - - - - 2 4.6  2.6  250 0   0     2 19     11     300   .75 0     
floats-cbmc-regression/float11_true-unreach-call_true-termination.i 2 .095 .096 26 .97 1.0  0   - - - - 2 3.3  1.9  250 0   0     2 15     8.9   300   .75 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i 2 .20  .20  26 2.6  1.0  0   - - - - 2 4.1  2.3  250 0   0     2 20     14     300   .75 0     
floats-cbmc-regression/float13_true-unreach-call_true-termination.i 2 .081 .082 26 .80 1.0  0   - - - - 2 4.6  2.6  250 0   0     2 16     9.6   300   .75 0     
floats-cbmc-regression/float14_true-unreach-call.i 2 .092 .092 26 .96 .85 0   - - - - 2 5.5  3.1  260 0   0     2 16     9.0   390   .68 0     
floats-cbmc-regression/float18_true-unreach-call.i 2 270     270     1200 3100    1.0  0   - - - - 2 48    41    610 0   0     0 11     6.7   290   .75 0     
floats-cbmc-regression/float19_true-unreach-call.i 2 .16  .16  26 1.8  1.0  0   - - - - 2 5.4  3.0  260 0   0     2 18     11     390   .75 0     
floats-cbmc-regression/float1_true-unreach-call_true-termination.i 2 .081 .081 26 .78 1.0  0   - - - - 2 4.2  2.3  250 0   0     2 14     8.6   300   .75 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i 2 .13  .13  30 1.4  1.0  0   - - - - 2 4.5  2.5  250 0   0     2 25     18     380   .75 0     
floats-cbmc-regression/float21_true-unreach-call.i 2 .32  .33  27 3.5  1.0  0   - - - - 2 9.3  6.9  290 0   0     2 68     60     580   .71 0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i 2 .19  .19  26 1.9  1.0  0   - - - - 2 5.2  2.9  270 0   0     2 220     200     740   .68 0     
floats-cbmc-regression/float2_true-unreach-call_true-termination.i 2 .10  .10  26 1.1  .85 0   - - - - 2 3.8  2.1  250 0   0     2 15     8.5   310   .68 0     
floats-cbmc-regression/float3_true-unreach-call_true-termination.i 2 .10  .11  26 .81 .85 0   - - - - 2 4.8  2.7  270 0   0     2 16     11     320   .75 0     
floats-cbmc-regression/float4_true-unreach-call.i 2 .83  .83  31 10    1.0  0   - - - - 2 88    85    330 0   0     2 93     85     570   .71 0     
floats-cbmc-regression/float5_true-unreach-call_true-termination.i 2 .28  .28  27 3.5  1.0  0   - - - - 2 4.2  2.4  260 0   0     2 29     24     300   .75 0     
floats-cbmc-regression/float6_true-unreach-call_true-termination.i 2 .096 .096 26 1.0  1.0  0   - - - - 2 3.8  2.2  260 0   0     2 15     8.9   310   .75 0     
floats-cbmc-regression/float8_true-unreach-call.i 2 .11  .11  26 1.0  1.0  0   - - - - 2 9.4  7.0  270 0   0     2 19     11     390   .75 0     
floats-cbmc-regression/float_lib1_true-unreach-call.i 2 .54  .54  27 7.0  .85 0   - - - - 2 5.8  3.1  260 0   0     0 13     7.7   290   .75 0     
floats-cbmc-regression/float_lib2_true-unreach-call.i 2 .097 .098 27 1.1  1.0  0   - - - - 2 5.3  2.9  250 0   0     2 22     12     420   .71 0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c 1 .094 .095 26 1.0  .85 0   -32 4.1  2.2  250 0     0   1 18     11     300   .68 0   0 3.4  1.9  250 0   0    0 .58   .58   20    .037 0      - -
float-benchs/cast_union_loose_false-unreach-call_true-termination.c 1 .17  .17  26 1.6  1.0  0   -32 4.0  2.3  250 0     0   1 14     8.7   310   .68 0   0 3.6  2.1  250 0   0    1 .57   .57   20    .053 0      - -
float-benchs/cast_union_tight_false-unreach-call_true-termination.c 1 .15  .16  27 1.7  .85 0   -32 4.3  2.3  250 0     0   1 14     8.6   320   .68 0   0 4.7  2.6  250 0   0    1 .60   .60   20    .049 0      - -
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c 1 .36  .36  28 5.4  1.0  0   1 4.2  2.4  260 0     0   1 14     8.4   300   .71 0   1 3.6  2.1  240 0   0    1 .57   .57   20    .049 0      - -
float-benchs/inv_Newton_false-unreach-call.c 0 900     900     300 7600    1.0  0   0 .75 .46 41 0     0   0 .025 .026 5.6 0    0   0 .94 .61 48 0   0    0 .0056 .0073 .53 0     0      - -
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c -32 450     450     530 4300    .85 0   0 19    16    530 .016 0   0 97     89     780   1.9  0   0 1.0  .66 50 0   0    0 .079  .079  11    0     0      - -
float-benchs/inv_square_false-unreach-call_true-termination.c 1 .30  .30  28 3.9  1.0  0   1 4.6  2.6  260 0     0   1 14     8.8   300   .71 0   1 4.3  2.6  240 0   0    1 .58   .58   20    .049 0      - -
float-benchs/nan_double_false-unreach-call_true-termination.c 1 .083 .085 26 .97 1.0  0   1 4.0  2.3  250 0     0   1 13     7.7   300   .71 0   0 3.5  2.0  250 0   0    0 .55   .55   20    .037 0      - -
float-benchs/nan_float_false-unreach-call_true-termination.c 1 .076 .077 26 .93 1.0  0   1 4.4  2.4  260 0     0   1 13     8.2   300   .71 0   0 3.5  2.1  250 0   0    0 .55   .55   20    .037 0      - -
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c 1 9.2   9.2   100 120    .85 0   1 6.3  4.0  310 0     0   1 33     24     1000   .68 0   1 4.0  2.3  250 0   0    1 .59   .59   20    .082 0      - -
float-benchs/sqrt_poly2_false-unreach-call.c 1 58     58     150 800    1.0  0   -32 4.6  2.5  270 0     0   1 24     18     600   .68 0   0 4.2  2.3  250 0   0    1 .60   .59   20    .057 0      - -
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c 2 .10  .10  26 .81 1.0  0   - - - - 0 900    900    1500 0   0     0 960     900     2500   1.5  0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c 2 21     21     260 280    1.0  0   - - - - 0 900    900    1600 0   0     0 960     900     4400   .70 0     
float-benchs/Rump_double_true-unreach-call_true-termination.c 2 .087 .087 26 .90 1.0  0   - - - - 2 4.0  2.3  250 0   0     2 33     27     1000   .71 0     
float-benchs/Rump_float_true-unreach-call_true-termination.c 2 .10  .11  26 .83 .85 0   - - - - 2 4.4  2.4  250 0   0     2 18     12     430   .75 0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c 2 .085 .086 26 .98 .85 0   - - - - 2 4.3  2.4  250 0   0     2 16     10     290   .75 0     
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c 2 .098 .10  26 1.5  1.0  0   - - - - 2 4.1  2.3  250 0   0     2 15     8.9   300   .75 0     
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c 2 .075 .076 26 .75 .85 0   - - - - 2 4.6  2.5  250 0   0     2 14     7.8   300   .75 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c 2 250     250     490 3100    1.0  0   - - - - 2 33    31    500 0   0     0 130     120     2600   .71 0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c 0 900     900     330 12000    1.0  0   - - - - 0 .66 .41 41 0   0     0 .028 .030 5.6 0    0     
float-benchs/cast_float_union_true-unreach-call.c 2 .11  .11  26 .78 1.0  0   - - - - 2 4.4  2.4  250 0   0     2 9.1   5.2   310   .66 0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c 2 120     120     240 1400    .85 0   - - - - 0 900    900    1300 0   0     0 960     950     2900   .72 0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c 0 900     900     5200 10000    1.0  0   - - - - 0 .81 .51 41 0   0     0 .023 .024 5.7 0    0     
float-benchs/divmul_diverge_true-unreach-call_true-termination.c 0 900     900     8300 11000    1.0  0   - - - - 0 .82 .51 41 0   0     0 .025 .026 5.6 0    0     
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c 2 .42  .42  30 5.2  .85 0   - - - - 2 28    25    410 0   0     2 350     330     650   .71 0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c 2 .43  .43  29 4.9  .85 0   - - - - 2 29    26    410 0   0     2 300     280     610   .71 0     
float-benchs/exp_loop_true-unreach-call.c 2 12     12     67 170    1.0  0   - - - - 0 820    800    7000 0   0     0 960     950     1300   1.8  0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c 0 900     900     8400 8900    .85 0   - - - - 0 .64 .38 41 0   0     0 .027 .029 5.7 0    0     
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c 0 900     900     1100 10000    1.0  0   - - - - 0 .72 .44 40 0   0     0 .022 .024 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c 2 56     56     140 780    .85 0   - - - - 2 13    11    450 0   0     2 600     590     930   .68 0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c 2 59     59     140 740    1.0  0   - - - - 2 13    11    450 0   0     2 760     750     970   .71 0     
float-benchs/filter1_true-unreach-call_true-termination.c 2 50     50     100 760    1.0  0   - - - - 2 9.2  6.8  400 0   0     2 110     99     610   .71 0     
float-benchs/filter2_alt_true-unreach-call.c 0 900     900     250 10000    .86 0   - - - - 0 .58 .38 40 0   0     0 .027 .027 5.6 0    0     
float-benchs/filter2_iterated_true-unreach-call.c 0 900     900     1100 12000    1.0  0   - - - - 0 .77 .47 40 0   0     0 .021 .023 5.6 0    0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c 0 900     900     400 12000    1.0  0   - - - - 0 .82 .50 42 0   0     0 .021 .022 5.6 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c 0 900     900     380 8800    1.0  0   - - - - 0 .75 .45 42 0   0     0 .021 .022 5.6 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c 0 900     900     350 12000    .86 0   - - - - 0 .75 .47 40 0   0     0 .028 .029 5.6 0    0     
float-benchs/filter_iir_true-unreach-call.c 0 900     900     560 12000    .86 0   - - - - 0 .71 .43 40 0   0     0 .026 .027 5.6 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c 2 .076 .077 26 .68 1.0  0   - - - - 2 4.4  2.4  250 0   0     2 14     8.3   290   .75 0     
float-benchs/image_filter_true-unreach-call.c 0 900     900     1900 9300    1.0  0   - - - - 0 .74 .44 40 0   0     0 .024 .025 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c 2 3.0   3.0   49 39    .85 0   - - - - 0 900    900    640 0   0     0 960     950     1500   .74 0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c 2 3.1   3.1   50 48    .85 0   - - - - 2 84    80    570 0   0     0 960     950     1600   .74 0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c 2 2.6   2.6   59 32    1.0  0   - - - - 2 42    40    450 0   0     0 960     950     1600   .79 0     
float-benchs/interpolation2_true-unreach-call_true-termination.c 2 4.2   4.2   45 47    1.0  0   - - - - 2 48    45    560 0   0     0 960     950     1500   .71 0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c 2 2.0   2.0   41 29    1.0  0   - - - - 2 47    44    470 0   0     0 960     950     1400   .72 0     
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c 2 2.0   2.0   41 29    .85 0   - - - - 2 84    81    480 0   0     0 960     950     1500   .71 0     
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c 2 1.7   1.7   48 26    1.0  0   - - - - 2 31    28    400 0   0     0 960     950     1400   .72 0     
float-benchs/interpolation_true-unreach-call_true-termination.c 2 2.2   2.2   39 33    1.0  0   - - - - 2 27    24    470 0   0     0 960     950     1600   .72 0     
float-benchs/inv_Newton_true-unreach-call.c 0 900     900     300 10000    1.0  0   - - - - 0 .73 .43 41 0   0     0 .026 .028 5.6 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c 2 4.5   4.5   48 58    .85 0   - - - - 2 7.8  5.7  310 0   0     2 85     78     790   .71 0     
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c 2 1.1   1.1   40 14    1.0  0   - - - - 2 5.4  3.4  280 0   0     2 76     68     510   .71 0     
float-benchs/inv_square_int_true-unreach-call_true-termination.c 2 .36  .36  29 4.4  1.0  0   - - - - 2 4.4  2.5  260 0   0     2 36     29     320   .71 0     
float-benchs/inv_square_true-unreach-call_true-termination.c 2 .30  .30  28 4.3  .85 0   - - - - 2 3.5  2.0  260 0   0     2 69     62     340   .71 0     
float-benchs/loop_true-unreach-call.c 0 900     890     1800 13000    1.0  0   - - - - 0 .61 .37 40 0   0     0 .021 .022 5.7 0    0     
float-benchs/mea8000_true-unreach-call.c 0 900     900     1900 8200    1.0  0   - - - - 0 .59 .36 41 0   0     0 .026 .027 5.6 0    0     
float-benchs/nan_double_range_true-unreach-call_true-termination.c 2 .075 .075 26 .92 1.0  0   - - - - 2 3.7  2.1  250 0   0     2 16     9.5   300   .71 0     
float-benchs/nan_float_range_true-unreach-call_true-termination.c 2 .11  .11  26 .82 1.0  0   - - - - 2 3.9  2.2  250 0   0     2 15     9.0   300   .71 0     
float-benchs/rlim_exit_true-unreach-call_true-termination.c 0 900     900     12000 10000    1.0  0   - - - - 0 .74 .45 41 0   0     0 .026 .027 5.6 0    0     
float-benchs/rlim_invariant_true-unreach-call.c.p+cfa-reducer.c 0 900     900     1400 8900    1.0  0   - - - - 0 .67 .42 41 0   0     0 .021 .023 5.7 0    0     
float-benchs/rlim_invariant_true-unreach-call.c.v+lhb-reducer.c 2 590     590     680 6400    .85 0   - - - - 2 8.7  5.8  340 0   0     0 960     950     980   .72 0     
float-benchs/rlim_invariant_true-unreach-call.c.v+nlh-reducer.c 2 620     620     700 7200    1.0  0   - - - - 2 8.5  5.7  350 0   0     0 960     940     930   .72 0     
float-benchs/rlim_invariant_true-unreach-call_true-termination.c 2 4.1   4.1   39 53    1.0  0   - - - - 2 6.7  4.1  320 0   0     2 890     880     810   .71 0     
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c 0 900     900     480 12000    1.0  0   - - - - 0 .75 .45 40 0   0     0 .024 .024 5.6 0    0     
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c 0 900     900     490 9800    1.0  0   - - - - 0 .65 .40 41 0   0     0 .039 .039 5.6 0    0     
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c 2 230     230     110 2900    .85 0   - - - - 0 900    900    540 0   0     0 960     950     2200   1.7  0     
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 900     900     1700 9200    1.0  0   - - - - 0 .61 .37 41 0   0     0 .028 .028 5.6 0    0     
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 900     900     1200 11000    1.0  0   - - - - 0 .73 .46 41 0   0     0 .025 .026 5.6 0    0     
float-benchs/sqrt_Householder_constant_true-unreach-call.c 0 900     900     1400 11000    .86 0   - - - - 0 .71 .44 41 0   0     0 .024 .025 5.7 0    0     
float-benchs/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c 0 140     140     15000 1500    1.0  0   - - - - 0 .58 .36 40 0   0     0 .028 .030 5.6 0    0     
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 900     900     490 9700    .86 0   - - - - 0 .63 .37 43 0   0     0 .027 .027 5.6 0    0     
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 900     900     1200 8600    1.0  0   - - - - 0 .79 .48 40 0   0     0 .021 .021 5.6 0    0     
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 900     900     1200 9200    1.0  0   - - - - 0 .74 .46 41 0   0     0 .021 .021 5.6 0    0     
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 900     900     1300 10000    1.0  0   - - - - 0 .78 .47 41 0   0     0 .023 .024 5.8 0    0     
float-benchs/sqrt_poly_true-unreach-call_true-termination.c 2 17     17     150 200    .85 0   - - - - 2 41    39    490 0   0     2 130     120     1100   .71 0     
float-benchs/water_pid_true-unreach-call_true-termination.c 2 19     19     120 310    .85 0   - - - - 0 900    900    940 0   0     0 180     170     3000   .71 0     
float-benchs/zonotope_2_true-unreach-call_true-termination.c 0 900     900     5000 11000    1.0  0   - - - - 0 .61 .38 41 0   0     0 .034 .035 5.5 0    0     
float-benchs/zonotope_3_true-unreach-call.c.p+cfa-reducer.c 2 .30  .30  28 3.8  1.0  0   - - - - 2 13    11    610 0   0     0 960     810     3600   .63 0     
float-benchs/zonotope_3_true-unreach-call.c.v+lhb-reducer.c 2 1.7   1.7   54 25    1.0  0   - - - - 2 40    36    1800 0   0     0 960     810     4800   .64 0     
float-benchs/zonotope_3_true-unreach-call_true-termination.c 2 3.7   3.8   49 46    1.0  0   - - - - 2 7.9  5.4  380 0   0     0 960     830     4600   1.7  0     
float-benchs/zonotope_loose_true-unreach-call.c.v+cfa-reducer.c 2 5.7   5.7   66 73    1.0  0   - - - - 2 5.3  3.4  310 0   0     2 170     160     790   .71 0     
float-benchs/zonotope_loose_true-unreach-call_true-termination.c 2 2.8   2.8   57 33    .85 0   - - - - 2 5.8  3.7  310 0   0     2 130     120     930   .71 0     
float-benchs/zonotope_tight_true-unreach-call_true-termination.c 2 2.9   2.9   58 33    1.0  0   - - - - 2 5.6  3.6  310 0   0     2 130     120     1100   .68 0     
floats-esbmc-regression/Double_div_true-unreach-call.i 2 14     13     100 170    .85 0   - - - - 2 6.0  4.1  370 0   0     2 230     220     2600   .71 0     
floats-esbmc-regression/Float_div_true-unreach-call.i 2 1.1   1.1   32 12    1.0  0   - - - - 2 5.0  3.0  300 0   0     2 110     110     550   .71 0     
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 2 .63  .63  36 8.7  .85 0   - - - - 0 4.6  2.5  260 0   0     0 14     7.9   280   .75 0     
floats-esbmc-regression/ceil_true-unreach-call.i 2 .094 .095 26 1.1  1.0  0   - - - - 2 5.6  3.1  260 0   0     0 16     8.9   290   .75 0     
floats-esbmc-regression/copysign_true-unreach-call.i 2 .094 .095 27 1.0  1.0  0   - - - - 2 7.0  3.9  260 0   0     0 14     8.3   290   .71 0     
floats-esbmc-regression/digits_for_true-unreach-call.i 2 4.0   4.0   71 56    .85 0   - - - - 0 900    900    1300 0   0     0 960     950     2900   .72 0     
floats-esbmc-regression/digits_while_true-unreach-call.i 2 4.0   4.0   72 53    .85 0   - - - - 0 900    900    1200 0   0     0 960     950     2900   1.8  0     
floats-esbmc-regression/fabs_true-unreach-call.i 2 .091 .091 27 1.1  .85 0   - - - - 2 5.0  2.8  250 0   0     2 17     9.7   390   .75 0     
floats-esbmc-regression/fdim_true-unreach-call.i 2 .095 .096 26 1.0  .85 0   - - - - 2 5.7  3.1  260 0   0     2 19     11     410   .75 0     
floats-esbmc-regression/floor_nondet_true-unreach-call.i 2 .64  .64  36 7.9  .85 0   - - - - 0 5.8  3.1  260 0   0     0 14     8.2   290   .75 0     
floats-esbmc-regression/floor_true-unreach-call.i 2 .10  .10  27 2.0  1.0  0   - - - - 2 4.6  2.5  260 0   0     0 12     7.3   290   .75 0     
floats-esbmc-regression/fmax_true-unreach-call.i 2 .091 .092 26 1.0  1.0  0   - - - - 2 5.2  2.8  260 0   0     2 18     10     380   .75 0     
floats-esbmc-regression/fmin_true-unreach-call.i 2 .11  .11  26 1.0  1.0  0   - - - - 2 5.3  2.9  260 0   0     2 18     11     390   .68 0     
floats-esbmc-regression/fmod2_true-unreach-call.i 2 .11  .11  26 1.9  .85 0   - - - - 2 9.2  6.9  470 0   0     0 17     9.5   290   .75 0     
floats-esbmc-regression/fmod3_true-unreach-call.i 2 .096 .097 26 1.0  .85 0   - - - - 2 10    7.6  470 0   0     0 14     8.0   290   .75 0     
floats-esbmc-regression/fmod_true-unreach-call.i 2 .10  .10  26 2.0  1.0  0   - - - - 2 4.6  2.6  260 0   0     0 12     6.7   290   .75 0     
floats-esbmc-regression/isgreater_true-unreach-call.i 2 .085 .086 27 1.1  1.0  0   - - - - 2 4.8  2.6  260 0   0     2 19     11     390   .75 0     
floats-esbmc-regression/isgreaterequal_true-unreach-call.i 2 .087 .088 26 1.1  1.0  0   - - - - 2 4.4  2.4  260 0   0     2 19     11     400   .68 0     
floats-esbmc-regression/isless_true-unreach-call.i 2 .090 .094 27 1.1  1.0  0   - - - - 2 4.6  2.5  260 0   0     2 15     8.8   390   .75 0     
floats-esbmc-regression/islessequal_true-unreach-call.i 2 .095 .096 26 .97 .85 0   - - - - 2 5.6  3.0  260 0   0     2 15     8.4   390   .75 0     
floats-esbmc-regression/islessgreater_true-unreach-call.i 2 .089 .090 27 .93 .85 0   - - - - 2 5.6  3.1  250 0   0     2 17     9.9   400   .75 0     
floats-esbmc-regression/isunordered_true-unreach-call.i 2 .089 .090 26 1.0  1.0  0   - - - - 2 5.6  3.0  260 0   0     2 16     9.5   390   .75 0     
floats-esbmc-regression/lrint_true-unreach-call.i 2 .14  .14  27 1.2  1.0  0   - - - - 0 5.2  2.8  260 0   0     0 6.0   3.6   290   .66 0     
floats-esbmc-regression/modf_true-unreach-call.i 2 .13  .13  26 1.1  1.0  0   - - - - 2 5.4  2.9  260 0   0     0 8.0   4.5   280   .66 0     
floats-esbmc-regression/nan_true-unreach-call.i 2 .087 .087 26 .92 .85 0   - - - - 2 4.9  2.7  260 0   0     2 16     9.6   410   .71 0     
floats-esbmc-regression/nearbyint2_true-unreach-call.i 2 .12  .12  27 1.1  1.0  0   - - - - 0 4.7  2.5  260 0   0     0 6.4   3.8   280   .66 0     
floats-esbmc-regression/nearbyint_true-unreach-call.i 2 .16  .16  27 2.0  1.0  0   - - - - 0 5.4  2.9  280 0   0     0 8.0   4.6   290   .66 0     
floats-esbmc-regression/remainder_true-unreach-call.i 2 .13  .14  27 1.6  1.0  0   - - - - 2 6.1  3.3  260 0   0     0 15     8.4   290   .75 0     
floats-esbmc-regression/rint2_true-unreach-call.i 2 .11  .11  27 .94 .85 0   - - - - 0 4.7  2.6  260 0   0     0 6.5   3.5   290   .66 0     
floats-esbmc-regression/rint_true-unreach-call.i 2 .15  .15  27 1.9  .85 0   - - - - 0 6.0  3.3  280 0   0     0 7.8   4.6   290   .66 0     
floats-esbmc-regression/round_nondet_true-unreach-call.i 2 .95  .95  40 12    1.0  0   - - - - 0 4.5  2.5  260 0   0     0 12     7.2   290   .75 0     
floats-esbmc-regression/round_true-unreach-call.i 2 .14  .14  27 1.6  1.0  0   - - - - 2 5.7  3.1  260 0   0     0 12     6.7   280   .75 0     
floats-esbmc-regression/rounding_functions_true-unreach-call.i 2 .14  .14  27 1.7  1.0  0   - - - - 2 6.0  3.3  260 0   0     0 15     8.9   380   .71 0     
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 2 2.2   2.2   33 32    .85 0   - - - - 2 8.1  5.4  270 0   0     2 65     58     540   .71 0     
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 2 .58  .58  35 7.0  1.0  0   - - - - 0 5.9  3.2  260 0   0     0 16     8.7   290   .75 0     
floats-esbmc-regression/trunc_true-unreach-call.i 2 .10  .10  26 1.0  1.0  0   - - - - 2 5.5  3.0  260 0   0     0 13     7.5   280   .75 0     
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 1 44     43     370 600    1.0  0   1 19    9.9  540 0     0   0 97     90     1300   1.8  0   1 3.5  2.1  250 0   0    1 .57   .57   20    .045 0      - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 1 2.1   2.0   39 32    .85 0   1 7.9  4.2  260 0     0   0 97     90     500   2.1  0   1 3.6  2.1  250 0   0    1 .57   .57   20    .045 0      - -
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 1 6.8   6.8   73 85    1.0  0   0 4.0  2.2  250 0     0   -32 68     62     830   .68 0   1 3.5  2.0  250 0   0    -32 .57   .57   20    .045 0      - -
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 1 6.8   6.8   73 100    .85 0   0 3.9  2.2  250 0     0   0 97     90     1000   1.8  0   1 3.8  2.2  250 0   0    -32 .59   .59   20    .045 .0082 - -
floats-esbmc-regression/Double_div_true-unreach-call.i.p+cfa-reducer.c 2 14     13     120 210    1.0  0   - - - - 2 7.0  4.7  370 0   0     2 240     230     2800   .71 0     
floats-esbmc-regression/Float_div_true-unreach-call.i.p+cfa-reducer.c 2 3.8   3.8   59 47    1.0  0   - - - - 2 6.8  4.9  380 0   0     0 560     550     2700   .71 0     
floats-esbmc-regression/Double_div_bad_false-unreach-call.i.p+cfa-reducer.c 1 45     44     430 600    .85 0   1 18    9.9  450 0     0   0 97     90     1300   .68 0   1 3.5  2.0  250 0   0    1 .57   .57   20    .045 .0041 - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i.p+cfa-reducer.c 1 5.5   5.5   67 71    1.0  0   1 7.9  4.2  270 0     0   0 97     89     1200   2.1  0   1 3.4  2.0  240 0   0    1 .58   .58   20    .045 0      - -
float-newlib/double_req_bl_0210_true-unreach-call.c 2 .58  .58  84 6.4  .85 0   - - - - 2 20    16    1400 0   0     2 240     220     1400   .71 0     
float-newlib/double_req_bl_0220a_true-unreach-call.c 2 .51  .51  82 5.0  1.0  0   - - - - 2 22    18    1300 0   0     2 110     95     1200   .68 0     
float-newlib/double_req_bl_0220b_true-unreach-call.c 2 .52  .52  83 5.1  1.0  0   - - - - 2 22    18    1300 0   0     2 110     92     1200   .71 0     
float-newlib/double_req_bl_0240a_true-unreach-call.c 2 .56  .56  86 7.2  1.0  0   - - - - 2 19    16    1400 0   0     2 81     66     950   .68 0     
float-newlib/double_req_bl_0240b_true-unreach-call.c 2 .58  .58  86 6.4  1.0  0   - - - - 2 21    17    1400 0   0     2 90     72     950   .71 0     
float-newlib/double_req_bl_0250a_true-unreach-call.c 2 .30  .30  47 3.5  .85 0   - - - - 2 22    19    1300 0   0     2 140     130     2300   .71 0     
float-newlib/double_req_bl_0250b_true-unreach-call.c 2 .30  .30  47 3.2  1.0  0   - - - - 2 22    19    1300 0   0     2 92     80     2200   .71 0     
float-newlib/double_req_bl_0260_true-unreach-call.c 2 .27  .27  47 3.2  1.0  0   - - - - 2 25    22    1300 0   0     2 96     85     2200   .68 0     
float-newlib/double_req_bl_0270a_true-unreach-call.c 2 .28  .28  47 3.9  1.0  0   - - - - 2 19    17    1300 0   0     2 93     82     2100   .71 0     
float-newlib/double_req_bl_0270b_true-unreach-call.c 2 .31  .31  48 3.4  .85 0   - - - - 2 26    23    1300 0   0     2 95     85     2200   .68 0     
float-newlib/double_req_bl_0281_true-unreach-call.c 2 .52  .52  77 5.8  1.0  0   - - - - 2 23    20    1300 0   0     2 39     30     1500   .75 0     
float-newlib/double_req_bl_0310_true-unreach-call.c 2 .57  .57  84 6.5  1.0  0   - - - - 2 18    14    1300 0   0     2 370     340     1500   .71 0     
float-newlib/double_req_bl_0320_true-unreach-call.c 2 .92  .92  120 14    1.0  0   - - - - 2 20    16    1300 0   0     2 100     89     1200   .71 0     
float-newlib/double_req_bl_0330a_true-unreach-call.c 2 .61  .61  86 6.2  1.0  0   - - - - 2 17    14    1300 0   0     2 90     72     950   .71 0     
float-newlib/double_req_bl_0330b_true-unreach-call.c 2 .56  .56  86 6.5  1.0  0   - - - - 2 20    16    1300 0   0     2 89     72     950   .71 0     
float-newlib/double_req_bl_0460_true-unreach-call.c 2 21     21     1000 190    .85 0   - - - - 2 23    20    1200 0   0     2 130     120     2500   .71 0     
float-newlib/double_req_bl_0470_true-unreach-call.c 2 .14  .14  27 1.2  1.0  0   - - - - 2 19    16    1200 0   0     2 99     88     2200   .71 0     
float-newlib/double_req_bl_0480_true-unreach-call.c 2 .17  .17  28 1.7  1.0  0   - - - - 2 22    19    1200 0   0     2 99     88     2200   .71 0     
float-newlib/double_req_bl_0490a_true-unreach-call.c 2 .12  .12  28 1.3  .85 0   - - - - 2 20    17    1200 0   0     2 170     160     2500   .71 0     
float-newlib/double_req_bl_0490b_true-unreach-call.c 2 .13  .13  28 1.3  .85 0   - - - - 2 19    16    1200 0   0     2 100     92     2200   .71 0     
float-newlib/double_req_bl_0520_true-unreach-call.c 2 .69  .69  99 7.6  1.0  0   - - - - 2 33    29    2100 0   0     2 360     340     2500   .68 0     
float-newlib/double_req_bl_0530a_true-unreach-call.c 2 .61  .61  94 6.8  .85 0   - - - - 2 30    26    2100 0   0     2 140     120     2100   .71 0     
float-newlib/double_req_bl_0530b_true-unreach-call.c 2 .60  .61  94 7.1  .85 0   - - - - 2 29    26    2100 0   0     2 130     110     2200   .71 0     
float-newlib/double_req_bl_0550a_true-unreach-call.c 2 .67  .67  100 9.6  1.0  0   - - - - 2 31    27    2100 0   0     2 100     85     2200   .71 0     
float-newlib/double_req_bl_0550b_true-unreach-call.c 2 .72  .72  100 7.4  1.0  0   - - - - 2 31    27    2100 0   0     2 110     93     2200   .71 0     
float-newlib/double_req_bl_0620a_true-unreach-call.c 2 .17  .17  35 2.1  1.0  0   - - - - 2 14    12    1100 0   0     2 240     230     2100   .71 0     
float-newlib/double_req_bl_0620b_true-unreach-call.c 2 .17  .17  35 2.0  1.0  0   - - - - 2 16    13    1100 0   0     2 200     190     2000   .71 0     
float-newlib/double_req_bl_0621a_true-unreach-call.c 2 .18  .18  35 2.1  1.0  0   - - - - 2 15    13    1000 0   0     2 740     720     2400   .71 0     
float-newlib/double_req_bl_0621b_true-unreach-call.c 2 .17  .17  35 1.9  1.0  0   - - - - 2 16    13    1100 0   0     0 960     940     1800   .75 0     
float-newlib/double_req_bl_0660a_true-unreach-call.c 2 .44  .44  66 4.6  .85 0   - - - - 2 19    16    1200 0   0     2 99     84     1500   .71 0     
float-newlib/double_req_bl_0660b_true-unreach-call.c 2 .38  .39  66 4.5  1.0  0   - - - - 2 18    16    1300 0   0     2 87     74     1400   .71 0     
float-newlib/double_req_bl_0661a_true-unreach-call.c 2 .40  .41  66 5.2  1.0  0   - - - - 2 19    16    1300 0   0     2 260     250     2300   .71 0     
float-newlib/double_req_bl_0661b_true-unreach-call.c 2 .39  .40  67 5.9  1.0  0   - - - - 2 19    16    1300 0   0     2 280     260     2300   .71 0     
float-newlib/double_req_bl_0662a_true-unreach-call.c 2 .45  .45  75 4.7  1.0  0   - - - - 2 16    14    1300 0   0     2 170     150     1600   .71 0     
float-newlib/double_req_bl_0662b_true-unreach-call.c 2 .44  .44  75 4.5  .85 0   - - - - 2 18    15    1300 0   0     2 480     460     2300   .71 0     
float-newlib/double_req_bl_0663a_true-unreach-call.c 2 .44  .44  75 5.1  .85 0   - - - - 2 17    14    1300 0   0     2 110     96     1500   .71 0     
float-newlib/double_req_bl_0663b_true-unreach-call.c 2 .43  .43  75 4.9  .85 0   - - - - 2 18    16    1300 0   0     2 240     230     1900   .71 0     
float-newlib/double_req_bl_0670_true-unreach-call.c 2 8.2   8.2   550 110    1.0  0   - - - - 2 17    15    1400 0   0     2 190     180     1500   .71 0     
float-newlib/double_req_bl_0680a_true-unreach-call.c 2 .33  .33  62 3.7  .85 0   - - - - 2 16    14    1300 0   0     2 98     84     1400   .68 0     
float-newlib/double_req_bl_0680b_true-unreach-call.c 2 .34  .34  61 3.9  .85 0   - - - - 2 20    17    1300 0   0     2 85     71     1400   .71 0     
float-newlib/double_req_bl_0681a_true-unreach-call.c 2 .34  .34  61 3.7  .85 0   - - - - 2 22    19    1300 0   0     2 79     66     1400   .71 0     
float-newlib/double_req_bl_0681b_true-unreach-call.c 2 .37  .37  61 4.2  1.0  0   - - - - 2 16    13    1300 0   0     2 79     64     1400   .71 0     
float-newlib/double_req_bl_0682a_true-unreach-call.c 2 .58  .58  97 5.9  .85 0   - - - - 2 16    14    1200 0   0     2 150     130     1600   .71 0     
float-newlib/double_req_bl_0682b_true-unreach-call.c 2 .57  .57  97 7.7  .85 0   - - - - 2 19    16    1200 0   0     2 120     100     1500   .71 0     
float-newlib/double_req_bl_0683a_true-unreach-call.c 2 .56  .56  98 8.0  1.0  0   - - - - 2 19    16    1300 0   0     2 110     92     1500   .71 0     
float-newlib/double_req_bl_0683b_true-unreach-call.c 2 .59  .59  98 5.5  1.0  0   - - - - 2 17    14    1300 0   0     2 100     84     1500   .71 0     
float-newlib/double_req_bl_0684a_true-unreach-call.c 2 .41  .42  70 4.8  .85 0   - - - - 2 17    14    1200 0   0     0 960     940     2400   1.7  .0082
float-newlib/double_req_bl_0684b_true-unreach-call.c 2 .42  .42  69 4.7  1.0  0   - - - - 2 19    16    1200 0   0     0 960     930     1900   .68 0     
float-newlib/double_req_bl_0685a_true-unreach-call.c 2 .33  .33  62 4.2  1.0  0   - - - - 2 17    15    1300 0   0     2 180     160     2000   .71 0     
float-newlib/double_req_bl_0685b_true-unreach-call.c 2 .36  .36  61 3.7  1.0  0   - - - - 2 19    16    1300 0   0     2 180     170     2000   .71 0     
float-newlib/double_req_bl_0686a_true-unreach-call.c 2 .33  .34  62 4.0  .85 0   - - - - 2 19    16    1300 0   0     2 160     150     2000   .71 0     
float-newlib/double_req_bl_0686b_true-unreach-call.c 2 .33  .33  62 3.8  .85 0   - - - - 2 20    17    1300 0   0     2 100     90     1600   .71 0     
float-newlib/double_req_bl_0720_true-unreach-call.c 2 .11  .11  27 1.0  1.0  0   - - - - 2 5.8  3.2  280 0   0     2 140     130     1300   .71 0     
float-newlib/double_req_bl_0730a_true-unreach-call.c 2 .10  .10  27 1.1  1.0  0   - - - - 2 6.9  4.3  420 0   0     2 31     23     740   .75 0     
float-newlib/double_req_bl_0730b_true-unreach-call.c 2 .10  .10  27 1.0  1.0  0   - - - - 2 6.6  4.1  390 0   0     2 42     31     860   .71 0     
float-newlib/double_req_bl_0730c_true-unreach-call.c 2 .093 .094 27 .96 .85 0   - - - - 2 6.9  4.3  400 0   0     2 42     32     880   .75 0     
float-newlib/double_req_bl_0740_true-unreach-call.c 2 .096 .098 27 1.0  .85 0   - - - - 2 6.0  3.8  420 0   0     2 41     34     710   .75 0     
float-newlib/double_req_bl_0832_true-unreach-call.c 2 .35  .36  56 4.4  1.0  0   - - - - 2 11    9.1  860 0   0     2 160     150     1600   .71 0     
float-newlib/double_req_bl_0833_true-unreach-call.c 2 .14  .14  30 1.7  .85 0   - - - - 2 14    11    830 0   0     2 140     130     1600   .71 0     
float-newlib/double_req_bl_0834_true-unreach-call.c 2 .10  .10  27 1.2  1.0  0   - - - - 2 13    10    800 0   0     2 120     100     1500   .71 0     
float-newlib/double_req_bl_0870b_true-unreach-call.c 2 .89  .89  110 8.6  1.0  0   - - - - 2 38    34    2600 0   0     2 320     310     2900   .70 0     
float-newlib/double_req_bl_0872a_true-unreach-call.c 2 .91  .92  120 9.7  1.0  0   - - - - 2 33    29    2600 0   0     2 200     190     2800   .70 0     
float-newlib/double_req_bl_0872b_true-unreach-call.c 2 .97  .97  120 8.8  .85 0   - - - - 2 34    31    2600 0   0     2 590     580     3400   .71 0     
float-newlib/double_req_bl_0873a_true-unreach-call.c 2 .72  .72  98 9.4  1.0  0   - - - - 2 34    30    2600 0   0     2 230     210     2300   .68 0     
float-newlib/double_req_bl_0873b_true-unreach-call.c 2 .74  .74  98 8.8  1.0  0   - - - - 2 36    33    2600 0   0     2 260     240     2300   .71 0     
float-newlib/double_req_bl_0874_true-unreach-call.c 2 1.0   1.0   130 11    1.0  0   - - - - 2 36    33    2600 0   0     2 280     260     2200   .71 0     
float-newlib/double_req_bl_0876_true-unreach-call.c 2 .92  .92  110 13    1.0  0   - - - - 2 38    34    2600 0   .029 2 260     240     2200   .71 0     
float-newlib/double_req_bl_0882_true-unreach-call.c 2 .95  .95  110 10    1.0  0   - - - - 2 37    33    2600 0   0     0 340     330     2700   .71 0     
float-newlib/double_req_bl_0883_true-unreach-call.c 2 .87  .87  110 11    .85 0   - - - - 2 38    34    2600 0   0     2 790     770     2400   .71 0     
float-newlib/double_req_bl_0910a_true-unreach-call.c 2 .16  .17  34 1.8  1.0  0   - - - - 2 16    13    1100 0   0     2 430     410     1900   .71 0     
float-newlib/double_req_bl_0910b_true-unreach-call.c 2 .16  .16  34 2.0  1.0  0   - - - - 2 13    12    1100 0   0     2 84     74     1500   .71 0     
float-newlib/double_req_bl_0920a_true-unreach-call.c 2 8.6   8.6   400 98    1.0  0   - - - - 2 17    15    1100 0   0     2 99     89     1500   .71 0     
float-newlib/double_req_bl_0920b_true-unreach-call.c 2 .16  .16  34 2.1  1.0  0   - - - - 2 17    14    1100 0   0     2 86     76     1500   .71 0     
float-newlib/double_req_bl_0921_true-unreach-call.c 2 .21  .21  33 1.7  .85 0   - - - - 2 13    11    1100 0   0     2 120     110     1900   .71 0     
float-newlib/double_req_bl_0930_true-unreach-call.c 2 .16  .16  34 2.0  .85 0   - - - - 2 16    14    1100 0   0     2 130     120     1600   .71 0     
float-newlib/double_req_bl_0931_true-unreach-call.c 2 .16  .16  34 2.2  1.0  0   - - - - 2 20    17    1100 0   0     2 87     78     1700   .71 0     
float-newlib/double_req_bl_0960b_true-unreach-call.c 2 .21  .21  42 2.5  1.0  0   - - - - 2 19    17    1300 0   0     2 85     74     1400   .68 0     
float-newlib/double_req_bl_0970a_true-unreach-call.c 2 20     20     460 230    .85 0   - - - - 2 20    18    1400 0   0     2 86     77     1400   .71 0     
float-newlib/double_req_bl_0970b_true-unreach-call.c 2 .20  .20  42 3.0  .85 0   - - - - 2 19    17    1300 0   0     2 82     71     1300   .71 0     
float-newlib/double_req_bl_0971_true-unreach-call.c 2 .20  .20  42 2.5  .85 0   - - - - 2 17    15    1300 0   0     2 100     89     1400   .71 0     
float-newlib/double_req_bl_0981_true-unreach-call.c 2 .20  .20  42 2.6  .85 0   - - - - 2 19    17    1300 0   0     2 66     57     1400   .71 0     
float-newlib/double_req_bl_1011a_true-unreach-call.c 2 .091 .093 26 1.1  1.0  0   - - - - 2 4.3  2.3  250 0   0     2 20     13     390   .75 0     
float-newlib/double_req_bl_1011b_true-unreach-call.c 2 .089 .091 26 1.0  1.0  0   - - - - 2 3.7  2.1  250 0   0     2 23     15     390   .75 0     
float-newlib/double_req_bl_1012a_true-unreach-call.c 2 .087 .088 26 .98 1.0  0   - - - - 2 4.1  2.3  250 0   0     2 20     12     380   .75 0     
float-newlib/double_req_bl_1012b_true-unreach-call.c 2 .087 .091 26 1.0  1.0  0   - - - - 2 4.6  2.6  250 0   0     2 25     15     360   .75 0     
float-newlib/double_req_bl_1031_true-unreach-call.c 2 .089 .089 26 .99 1.0  0   - - - - 2 4.6  2.6  270 0   0     2 30     20     440   .71 0     
float-newlib/double_req_bl_1032a_true-unreach-call.c 2 .087 .087 26 1.2  .85 0   - - - - 2 4.3  2.5  270 0   0     2 29     19     460   .75 0     
float-newlib/double_req_bl_1032b_true-unreach-call.c 2 .089 .089 26 .98 1.0  0   - - - - 2 4.2  2.4  270 0   0     2 29     19     460   .75 0     
float-newlib/double_req_bl_1032c_true-unreach-call.c 2 .088 .089 26 1.1  1.0  0   - - - - 2 4.2  2.4  270 0   0     2 26     18     430   .71 0     
float-newlib/double_req_bl_1032d_true-unreach-call.c 2 .093 .093 27 .95 1.0  0   - - - - 2 4.6  2.5  270 0   0     2 32     23     440   .71 0     
float-newlib/double_req_bl_1051_true-unreach-call.c 2 .082 .086 27 1.1  .85 0   - - - - 2 4.7  2.6  270 0   0     2 35     26     470   .68 0     
float-newlib/double_req_bl_1052a_true-unreach-call.c 2 .090 .091 26 .95 1.0  0   - - - - 2 4.2  2.5  270 0   0     2 37     27     490   .75 0     
float-newlib/double_req_bl_1052b_true-unreach-call.c 2 .088 .088 27 .94 1.0  0   - - - - 2 5.2  3.0  270 0   0     2 32     23     490   .75 0     
float-newlib/double_req_bl_1052c_true-unreach-call.c 2 .094 .095 26 1.0  1.0  0   - - - - 2 4.5  2.5  280 0   0     2 41     33     540   .71 0     
float-newlib/double_req_bl_1052d_true-unreach-call.c 2 .094 .095 27 .97 1.0  0   - - - - 2 5.4  3.1  280 0   0     2 33     25     470   .75 0     
float-newlib/double_req_bl_1071_true-unreach-call.c 2 .094 .095 26 1.5  1.0  0   - - - - 2 4.7  2.6  270 0   0     2 29     19     420   .75 0     
float-newlib/double_req_bl_1072a_true-unreach-call.c 2 .11  .11  27 .97 1.0  0   - - - - 2 4.6  2.6  270 0   0     2 25     17     400   .75 0     
float-newlib/double_req_bl_1072b_true-unreach-call.c 2 .086 .087 26 1.1  .85 0   - - - - 2 5.0  2.9  270 0   0     2 26     16     450   .75 0     
float-newlib/double_req_bl_1072c_true-unreach-call.c 2 .090 .090 26 1.2  1.0  0   - - - - 2 5.0  2.8  270 0   0     2 26     17     450   .75 0     
float-newlib/double_req_bl_1072d_true-unreach-call.c 2 .089 .090 26 1.3  1.0  0   - - - - 2 4.8  2.7  270 0   0     2 23     15     400   .75 0     
float-newlib/double_req_bl_1091_true-unreach-call.c 2 .096 .097 26 1.3  .85 0   - - - - 2 4.0  2.3  270 0   0     2 35     26     450   .75 0     
float-newlib/double_req_bl_1092a_true-unreach-call.c 2 .089 .089 27 1.2  1.0  0   - - - - 2 4.8  2.7  270 0   0     2 35     26     420   .75 0     
float-newlib/double_req_bl_1092b_true-unreach-call.c 2 .092 .092 26 1.1  1.0  0   - - - - 2 5.4  3.0  280 0   0     2 35     26     490   .71 0     
float-newlib/double_req_bl_1092c_true-unreach-call.c 2 .093 .094 26 1.1  1.0  0   - - - - 2 4.1  2.3  270 0   0     2 29     22     480   .68 0     
float-newlib/double_req_bl_1092d_true-unreach-call.c 2 .091 .091 26 .93 .85 0   - - - - 2 4.9  2.8  270 0   0     2 33     24     470   .75 0     
float-newlib/double_req_bl_1121a_true-unreach-call.c 2 .11  .12  27 1.6  1.0  0   - - - - 2 9.1  6.4  470 0   0     2 200     190     1300   .71 0     
float-newlib/double_req_bl_1121b_true-unreach-call.c 2 .14  .14  27 1.2  1.0  0   - - - - 2 10    6.9  480 0   0     2 66     57     1200   .71 0     
float-newlib/double_req_bl_1122a_true-unreach-call.c 2 .13  .13  27 1.4  1.0  0   - - - - 2 7.8  4.9  480 0   0     2 91     82     1300   .71 0     
float-newlib/double_req_bl_1122b_true-unreach-call.c 2 .12  .12  27 1.3  .85 0   - - - - 2 8.4  5.3  480 0   0     2 340     330     1500   .71 0     
float-newlib/double_req_bl_1130a_true-unreach-call.c 2 .16  .16  27 1.2  .85 0   - - - - 2 8.9  5.5  480 0   0     2 63     51     880   .71 0     
float-newlib/double_req_bl_1131a_true-unreach-call.c 2 .21  .21  27 2.3  .85 0   - - - - 2 8.7  5.6  480 0   0     2 48     37     820   .71 0     
float-newlib/double_req_bl_1131b_true-unreach-call.c 2 .17  .17  27 2.4  .85 0   - - - - 2 8.5  5.5  470 0   0     2 41     32     820   .75 0     
float-newlib/double_req_bl_1211a_true-unreach-call.c 2 .11  .11  27 1.2  1.0  0   - - - - 2 5.7  3.3  320 0   0     2 36     26     570   .75 0     
float-newlib/double_req_bl_1211b_true-unreach-call.c 2 .11  .11  27 1.2  1.0  0   - - - - 2 5.4  3.2  330 0   0     2 40     29     560   .71 0     
float-newlib/double_req_bl_1230_true-unreach-call.c 2 .11  .11  26 .76 .85 0   - - - - 2 4.8  2.7  250 0   0     2 26     16     480   .71 0     
float-newlib/double_req_bl_1231b_true-unreach-call.c 0 11     11     15000 150    .93 0   - - - - 0 .77 .46 41 0   0     0 .027 .028 5.7 0    0     
float-newlib/double_req_bl_1232a_true-unreach-call.c 2 .098 .099 26 1.0  1.0  0   - - - - 2 4.3  2.5  260 0   0     2 31     21     510   .75 0     
float-newlib/double_req_bl_1250_true-unreach-call.c 2 .082 .083 26 1.0  .85 0   - - - - 2 4.1  2.3  260 0   0     2 22     13     470   .75 0     
float-newlib/double_req_bl_1251b_true-unreach-call.c 0 11     11     15000 150    1.1  0   - - - - 0 .77 .46 40 0   0     0 .025 .025 5.6 0    0     
float-newlib/double_req_bl_1252a_true-unreach-call.c 2 .094 .094 26 1.1  1.0  0   - - - - 2 4.0  2.2  260 0   0     2 30     21     510   .75 0     
float-newlib/double_req_bl_1300_true-unreach-call.c 2 .10  .10  26 .75 1.0  0   - - - - 2 4.5  2.6  260 0   0     2 50     39     690   .71 0     
float-newlib/float_req_bl_0220a_true-unreach-call.c 2 .36  .36  59 4.1  1.0  0   - - - - 2 7.1  3.8  290 0   0     2 79     63     750   .68 0     
float-newlib/float_req_bl_0220b_true-unreach-call.c 2 .38  .38  59 4.0  1.0  0   - - - - 2 7.2  3.8  280 0   0     2 79     64     760   .71 0     
float-newlib/float_req_bl_0240a_true-unreach-call.c 2 .39  .39  62 5.3  1.0  0   - - - - 2 7.3  3.9  280 0   0     2 70     50     700   .71 0     
float-newlib/float_req_bl_0240b_true-unreach-call.c 2 .39  .39  62 5.4  .85 0   - - - - 2 6.4  3.4  280 0   0     2 64     48     700   .71 0     
float-newlib/float_req_bl_0250a_true-unreach-call.c 2 .19  .19  34 2.1  1.0  0   - - - - 2 4.4  2.5  270 0   0     2 69     58     870   .71 0     
float-newlib/float_req_bl_0250b_true-unreach-call.c 2 .22  .22  34 2.3  1.0  0   - - - - 2 4.6  2.5  270 0   0     2 67     58     880   .68 0     
float-newlib/float_req_bl_0260_true-unreach-call.c 2 .20  .20  34 2.3  .85 0   - - - - 2 5.6  3.0  270 0   0     2 64     56     870   .71 0     
float-newlib/float_req_bl_0270a_true-unreach-call.c 2 .20  .21  35 2.3  .85 0   - - - - 2 5.4  3.0  270 0   0     2 67     56     920   .68 0     
float-newlib/float_req_bl_0270b_true-unreach-call.c 2 .20  .20  34 2.2  1.0  0   - - - - 2 5.7  3.1  270 0   0     2 68     57     950   .71 0     
float-newlib/float_req_bl_0281_true-unreach-call.c 2 9.6   9.6   270 120    .85 0   - - - - 2 11    7.7  520 0   0     2 74     64     990   .71 0     
float-newlib/float_req_bl_0310_true-unreach-call.c 2 .41  .41  59 4.4  1.0  0   - - - - 2 7.2  3.9  280 0   0     2 360     330     1000   .68 0     
float-newlib/float_req_bl_0320a_true-unreach-call.c 2 .37  .37  60 4.7  1.0  0   - - - - 2 5.7  3.1  280 0   0     2 83     65     760   .71 0     
float-newlib/float_req_bl_0320b_true-unreach-call.c 2 .39  .39  60 4.4  1.0  0   - - - - 2 5.7  3.1  290 0   0     2 84     66     750   .71 0     
float-newlib/float_req_bl_0330a_true-unreach-call.c 2 .40  .40  61 4.0  .85 0   - - - - 2 5.8  3.1  280 0   0     2 69     52     690   .71 0     
float-newlib/float_req_bl_0330b_true-unreach-call.c 2 .39  .39  61 4.8  .85 0   - - - - 2 6.4  3.4  280 0   0     2 66     48     690   .71 0     
float-newlib/float_req_bl_0460_true-unreach-call.c 2 9.6   9.6   340 100    1.0  0   - - - - 2 10    7.3  510 0   0     2 63     55     1100   .71 0     
float-newlib/float_req_bl_0470_true-unreach-call.c 2 .11  .11  27 1.1  1.0  0   - - - - 2 5.8  3.2  270 0   0     2 73     63     940   .71 0     
float-newlib/float_req_bl_0480_true-unreach-call.c 2 .13  .13  27 1.6  1.0  0   - - - - 2 5.9  3.2  290 0   0     2 70     59     950   .71 0     
float-newlib/float_req_bl_0490a_true-unreach-call.c 2 .11  .11  27 1.1  .85 0   - - - - 2 4.9  2.6  300 0   0     2 67     58     970   .71 0     
float-newlib/float_req_bl_0490b_true-unreach-call.c 2 .11  .11  27 1.3  .85 0   - - - - 2 5.7  3.1  270 0   0     2 72     62     980   .71 0     
float-newlib/float_req_bl_0530a_true-unreach-call.c 2 .39  .39  66 5.7  .85 0   - - - - 2 7.0  3.8  280 0   0     2 86     65     980   .71 0     
float-newlib/float_req_bl_0530b_true-unreach-call.c 2 .40  .41  66 6.5  .94 0   - - - - 2 6.7  3.6  280 0   0     2 83     65     990   .71 0     
float-newlib/float_req_bl_0550a_true-unreach-call.c 2 .44  .44  69 4.7  1.0  0   - - - - 2 6.7  3.6  270 0   0     2 63     47     1000   .71 0     
float-newlib/float_req_bl_0550b_true-unreach-call.c 2 .45  .45  69 6.0  1.0  0   - - - - 2 6.5  3.5  280 0   0     2 71     52     1000   .71 0     
float-newlib/float_req_bl_0610_true-unreach-call.c 2 .15  .15  28 1.6  1.0  0   - - - - 2 5.5  3.0  250 0   0     2 77     67     780   .71 0     
float-newlib/float_req_bl_0620a_true-unreach-call.c 2 .15  .16  28 1.6  .85 0   - - - - 2 5.0  2.8  250 0   0     2 71     62     770   .71 0     
float-newlib/float_req_bl_0620b_true-unreach-call.c 2 .14  .14  28 1.5  .85 0   - - - - 2 4.8  2.6  250 0   0     2 78     67     770   .71 0     
float-newlib/float_req_bl_0621a_true-unreach-call.c 2 .13  .14  27 1.9  .85 0   - - - - 2 4.9  2.7  260 0   0     0 960     950     1000   .74 0     
float-newlib/float_req_bl_0621b_true-unreach-call.c 2 .13  .13  27 1.7  1.0  0   - - - - 2 4.4  2.5  260 0   0     0 960     950     1000   1.8  0     
float-newlib/float_req_bl_0660a_true-unreach-call.c 2 .29  .29  46 4.3  .85 0   - - - - 2 8.9  6.1  530 0   0     2 44     32     730   .75 0     
float-newlib/float_req_bl_0660b_true-unreach-call.c 2 .26  .26  45 3.5  1.0  0   - - - - 2 8.4  5.8  510 0   0     2 39     29     730   .75 0     
float-newlib/float_req_bl_0661a_true-unreach-call.c 2 .29  .29  46 3.8  1.0  0   - - - - 2 8.8  6.2  500 0   0     2 120     100     940   .71 0     
float-newlib/float_req_bl_0661b_true-unreach-call.c 2 .26  .26  46 3.0  1.0  0   - - - - 2 7.0  4.8  510 0   0     2 110     95     950   .71 0     
float-newlib/float_req_bl_0662a_true-unreach-call.c 2 .28  .28  50 3.2  .85 0   - - - - 2 4.6  2.5  270 0   0     2 36     28     690   .75 0     
float-newlib/float_req_bl_0662b_true-unreach-call.c 2 .30  .30  50 3.2  .85 0   - - - - 2 5.4  3.1  270 0   0     2 49     37     720   .71 0     
float-newlib/float_req_bl_0663a_true-unreach-call.c 2 .31  .31  50 3.5  1.0  0   - - - - 2 4.4  2.5  280 0   0     2 50     36     710   .68 0     
float-newlib/float_req_bl_0663b_true-unreach-call.c 2 .28  .28  51 3.2  .85 0   - - - - 2 5.5  3.1  270 0   0     2 43     32     710   .71 0     
float-newlib/float_req_bl_0670_true-unreach-call.c 2 5.9   5.9   200 82    1.0  0   - - - - 2 8.9  6.2  520 0   0     2 78     66     780   .71 0     
float-newlib/float_req_bl_0680a_true-unreach-call.c 2 .23  .23  43 3.4  1.0  0   - - - - 2 5.3  2.9  250 0   0     2 44     33     730   .75 0     
float-newlib/float_req_bl_0680b_true-unreach-call.c 2 .23  .23  43 2.9  .85 0   - - - - 2 4.3  2.4  250 0   0     2 46     35     720   .71 0     
float-newlib/float_req_bl_0681a_true-unreach-call.c 2 .24  .25  43 3.1  1.0  0   - - - - 2 4.5  2.4  260 0   0     2 40     29     710   .75 0     
float-newlib/float_req_bl_0681b_true-unreach-call.c 2 .24  .24  43 3.5  .85 0   - - - - 2 5.5  3.0  260 0   0     2 53     39     700   .75 0     
float-newlib/float_req_bl_0682a_true-unreach-call.c 2 .36  .36  63 4.7  .85 0   - - - - 2 7.7  5.5  520 0   0     2 64     48     790   .71 0     
float-newlib/float_req_bl_0682b_true-unreach-call.c 2 .36  .36  64 5.2  1.0  0   - - - - 2 9.3  6.6  520 0   0     2 59     44     740   .68 0     
float-newlib/float_req_bl_0683a_true-unreach-call.c 2 .37  .37  64 4.9  1.0  0   - - - - 2 8.3  5.9  520 0   0     2 48     36     740   .75 0     
float-newlib/float_req_bl_0683b_true-unreach-call.c 2 .36  .36  64 4.5  1.0  0   - - - - 2 9.2  6.6  520 0   0     2 57     42     740   .71 0     
float-newlib/float_req_bl_0684a_true-unreach-call.c 2 .26  .26  48 3.5  1.0  0   - - - - 2 5.1  2.9  290 0   .31  0 960     940     1000   .72 0     
float-newlib/float_req_bl_0684b_true-unreach-call.c 2 .29  .29  48 3.2  1.0  0   - - - - 2 4.8  2.8  290 0   0     0 960     940     1100   .74 0     
float-newlib/float_req_bl_0685a_true-unreach-call.c 2 .24  .24  43 3.1  1.0  0   - - - - 2 5.3  2.9  250 0   0     2 54     41     740   .71 0     
float-newlib/float_req_bl_0685b_true-unreach-call.c 2 .23  .23  43 2.2  1.0  0   - - - - 2 4.7  2.6  250 0   0     2 59     46     740   .71 0     
float-newlib/float_req_bl_0686a_true-unreach-call.c 2 .24  .24  43 2.9  1.0  0   - - - - 2 4.5  2.5  250 0   0     2 47     34     710   .75 0     
float-newlib/float_req_bl_0686b_true-unreach-call.c 2 .23  .23  43 3.0  .85 0   - - - - 2 5.3  2.9  250 0   0     2 47     35     730   .75 0     
float-newlib/float_req_bl_0710_true-unreach-call.c 2 .54  .54  42 6.7  1.0  0   - - - - 2 6.7  4.0  300 0   0     2 310     300     2200   .71 0     
float-newlib/float_req_bl_0720_true-unreach-call.c 2 .098 .098 26 1.2  .85 0   - - - - 2 5.1  2.8  270 0   0     2 45     36     530   .75 0     
float-newlib/float_req_bl_0730a_true-unreach-call.c 2 .10  .10  27 .90 1.0  0   - - - - 2 4.3  2.4  270 0   .24  2 39     29     430   .75 0     
float-newlib/float_req_bl_0730b_true-unreach-call.c 2 .11  .11  26 .87 1.0  0   - - - - 2 5.1  2.8  270 0   0     2 24     15     450   .75 0     
float-newlib/float_req_bl_0730c_true-unreach-call.c 2 .092 .094 26 .98 1.0  0   - - - - 2 4.5  2.5  270 0   0     2 26     17     450   .75 0     
float-newlib/float_req_bl_0740_true-unreach-call.c 2 .097 .098 27 .95 1.0  0   - - - - 2 4.2  2.3  270 0   0     2 33     24     380   .71 0     
float-newlib/float_req_bl_0831_true-unreach-call.c 2 .11  .11  27 1.3  .85 0   - - - - 2 4.9  2.7  250 0   0     2 140     130     1200   .71 0     
float-newlib/float_req_bl_0832a_true-unreach-call.c 2 .14  .15  27 1.3  1.0  0   - - - - 2 5.2  2.8  260 0   0     2 130     120     760   .71 0     
float-newlib/float_req_bl_0832b_true-unreach-call.c 2 .12  .12  27 1.3  1.0  0   - - - - 2 4.2  2.3  250 0   0     2 140     130     810   .71 0     
float-newlib/float_req_bl_0833_true-unreach-call.c 2 .12  .12  27 1.6  1.0  0   - - - - 2 4.9  2.7  250 0   0     2 88     77     710   .71 0     
float-newlib/float_req_bl_0834_true-unreach-call.c 2 .14  .14  27 1.7  .85 0   - - - - 2 4.4  2.5  250 0   0     2 110     100     780   .71 0     
float-newlib/float_req_bl_0870b_true-unreach-call.c 2 .52  .52  70 6.0  .85 0   - - - - 2 6.8  3.7  290 0   0     2 67     56     910   .71 0     
float-newlib/float_req_bl_0872a_true-unreach-call.c 2 .57  .57  79 6.8  1.0  0   - - - - 2 6.9  3.7  310 0   0     2 57     47     910   .71 0     
float-newlib/float_req_bl_0872b_true-unreach-call.c 2 .62  .62  80 6.7  1.0  0   - - - - 2 5.6  3.0  280 0   0     2 70     57     910   .71 0     
float-newlib/float_req_bl_0873a_true-unreach-call.c 2 .47  .47  65 5.2  .85 0   - - - - 2 6.7  3.6  280 0   0     2 84     71     950   .70 0     
float-newlib/float_req_bl_0873b_true-unreach-call.c 2 .45  .45  65 6.4  1.0  0   - - - - 2 6.3  3.5  280 0   0     2 86     72     860   .68 0     
float-newlib/float_req_bl_0874_true-unreach-call.c 2 .80  .80  80 12    .85 0   - - - - 2 7.4  4.0  290 0   0     2 120     110     1000   .70 0     
float-newlib/float_req_bl_0875_true-unreach-call.c 2 .80  .80  79 9.5  .85 0   - - - - 2 6.6  3.6  290 0   0     2 150     130     1100   .71 0     
float-newlib/float_req_bl_0876_true-unreach-call.c 2 .62  .62  73 7.2  1.0  0   - - - - 2 7.1  3.8  290 0   0     2 120     110     1000   .71 0     
float-newlib/float_req_bl_0877_true-unreach-call.c 2 .62  .62  73 8.0  .85 0   - - - - 2 6.6  3.6  290 0   0     2 120     110     1100   .71 0     
float-newlib/float_req_bl_0880_true-unreach-call.c 2 1.8   1.8   130 20    1.0  0   - - - - 0 900    840    5900 0   0     2 510     490     1500   .71 0     
float-newlib/float_req_bl_0881_true-unreach-call.c 2 1.9   1.9   130 23    .85 0   - - - - 0 760    700    7000 0   0     2 420     390     1500   .71 0     
float-newlib/float_req_bl_0883_true-unreach-call.c 2 .54  .54  70 5.0  1.0  0   - - - - 2 6.2  3.6  340 0   0     2 230     210     1100   .71 0     
float-newlib/float_req_bl_0910a_true-unreach-call.c 2 .14  .14  27 1.5  1.0  0   - - - - 2 4.7  2.6  250 0   0     2 44     37     580   .71 0     
float-newlib/float_req_bl_0910b_true-unreach-call.c 2 .13  .13  27 1.5  1.0  0   - - - - 2 5.1  2.8  250 0   0     2 50     41     580   .68 0     
float-newlib/float_req_bl_0920a_true-unreach-call.c 2 .23  .23  34 2.5  1.0  0   - - - - 2 7.0  5.0  480 0   0     2 62     52     660   .71 0     
float-newlib/float_req_bl_0920b_true-unreach-call.c 2 .13  .13  28 1.5  1.0  0   - - - - 2 4.9  2.7  250 0   0     2 56     48     610   .71 0     
float-newlib/float_req_bl_0921_true-unreach-call.c 2 .13  .13  27 1.7  1.0  0   - - - - 2 4.8  2.6  250 0   0     2 74     64     740   .68 0     
float-newlib/float_req_bl_0930_true-unreach-call.c 2 .13  .13  27 1.3  1.0  0   - - - - 2 4.7  2.6  250 0   0     2 240     230     1700   .71 0     
float-newlib/float_req_bl_0931_true-unreach-call.c 2 .13  .13  27 1.5  1.0  0   - - - - 2 5.0  2.7  250 0   0     2 58     50     730   .71 0     
float-newlib/float_req_bl_0960a_true-unreach-call.c 2 .18  .18  32 1.9  1.0  0   - - - - 2 4.5  2.5  250 0   0     2 45     36     600   .75 0     
float-newlib/float_req_bl_0960b_true-unreach-call.c 2 .16  .16  32 1.8  1.0  0   - - - - 2 5.4  2.9  280 0   0     2 44     35     580   .71 0     
float-newlib/float_req_bl_0970a_true-unreach-call.c 2 .25  .25  42 3.0  1.0  0   - - - - 2 8.5  6.2  540 0   0     2 47     37     600   .75 0     
float-newlib/float_req_bl_0970b_true-unreach-call.c 2 .16  .16  32 2.0  1.0  0   - - - - 2 5.0  2.8  250 0   0     2 45     36     590   .71 0     
float-newlib/float_req_bl_0971_true-unreach-call.c 2 .15  .15  32 1.6  1.0  0   - - - - 2 4.9  2.6  260 0   0     2 53     43     660   .71 0     
float-newlib/float_req_bl_0981_true-unreach-call.c 2 .16  .16  32 2.1  .85 0   - - - - 2 5.1  2.8  250 0   0     2 45     35     640   .71 0     
float-newlib/float_req_bl_1010_true-unreach-call.c 2 .089 .091 26 .78 .85 0   - - - - 2 4.5  2.6  250 0   0     2 16     9.5   310   .75 0     
float-newlib/float_req_bl_1011a_true-unreach-call.c 2 .082 .083 26 .85 .85 0   - - - - 2 3.8  2.2  250 0   0     2 22     13     370   .75 0     
float-newlib/float_req_bl_1011b_true-unreach-call.c 2 .089 .089 26 .86 1.0  0   - - - - 2 3.8  2.1  250 0   0     2 22     13     360   .75 0     
float-newlib/float_req_bl_1012a_true-unreach-call.c 2 .090 .091 26 1.2  1.0  0   - - - - 2 4.2  2.3  250 0   0     2 22     13     320   .75 0     
float-newlib/float_req_bl_1012b_true-unreach-call.c 2 .10  .11  26 .88 .85 0   - - - - 2 4.3  2.4  250 0   0     2 21     12     320   .75 0     
float-newlib/float_req_bl_1031_true-unreach-call.c 2 .077 .078 26 .93 .85 0   - - - - 2 4.0  2.2  250 0   0     2 20     12     360   .71 0     
float-newlib/float_req_bl_1032a_true-unreach-call.c 2 .099 .099 26 .97 1.0  0   - - - - 2 3.8  2.1  250 0   0     2 20     13     460   .71 0     
float-newlib/float_req_bl_1032b_true-unreach-call.c 2 .086 .086 26 .89 1.0  0   - - - - 2 3.9  2.2  250 0   0     2 20     12     450   .75 0     
float-newlib/float_req_bl_1032c_true-unreach-call.c 2 .083 .083 26 .98 .85 0   - - - - 2 3.5  2.0  250 0   0     2 18     11     350   .75 0     
float-newlib/float_req_bl_1032d_true-unreach-call.c 2 .081 .082 26 .85 1.0  0   - - - - 2 3.9  2.2  250 0   0     2 22     13     340   .75 0     
float-newlib/float_req_bl_1051_true-unreach-call.c 2 .094 .095 26 .98 .85 0   - - - - 2 4.6  2.6  250 0   0     2 25     16     370   .75 0     
float-newlib/float_req_bl_1052a_true-unreach-call.c 2 .085 .086 26 .75 1.0  0   - - - - 2 4.7  2.6  250 0   0     2 22     14     390   .75 0     
float-newlib/float_req_bl_1052b_true-unreach-call.c 2 .081 .081 26 1.2  1.0  0   - - - - 2 5.2  3.0  250 0   0     2 24     15     390   .71 0     
float-newlib/float_req_bl_1052c_true-unreach-call.c 2 .089 .089 26 .97 1.0  0   - - - - 2 4.6  2.5  250 0   0     2 25     17     480   .71 0     
float-newlib/float_req_bl_1052d_true-unreach-call.c 2 .084 .085 26 .91 1.0  0   - - - - 2 4.8  2.7  250 0   0     2 23     15     450   .71 0     
float-newlib/float_req_bl_1071_true-unreach-call.c 2 .084 .086 26 1.2  .85 0   - - - - 2 4.7  2.6  250 0   0     2 19     11     320   .75 0     
float-newlib/float_req_bl_1072a_true-unreach-call.c 2 .095 .096 26 1.1  1.0  0   - - - - 2 3.6  2.1  250 0   0     2 20     12     350   .75 0     
float-newlib/float_req_bl_1072b_true-unreach-call.c 2 .088 .090 26 1.0  1.0  0   - - - - 2 4.7  2.6  250 0   0     2 21     13     360   .75 0     
float-newlib/float_req_bl_1072c_true-unreach-call.c 2 .094 .094 26 .85 1.0  0   - - - - 2 4.6  2.6  250 0   0     2 22     13     420   .75 0     
float-newlib/float_req_bl_1072d_true-unreach-call.c 2 .082 .083 26 1.2  1.0  0   - - - - 2 4.6  2.6  250 0   0     2 22     14     420   .71 0     
float-newlib/float_req_bl_1091_true-unreach-call.c 2 .10  .10  26 .78 .85 0   - - - - 2 4.3  2.4  250 0   0     2 27     17     370   .75 0     
float-newlib/float_req_bl_1092a_true-unreach-call.c 2 .11  .12  26 .94 1.0  0   - - - - 2 3.6  2.0  250 0   0     2 28     19     440   .75 0     
float-newlib/float_req_bl_1092b_true-unreach-call.c 2 .087 .088 26 1.3  .85 0   - - - - 2 4.7  2.7  260 0   0     2 30     21     480   .71 0     
float-newlib/float_req_bl_1092c_true-unreach-call.c 2 .088 .089 26 .86 1.0  0   - - - - 2 3.8  2.1  250 0   0     2 22     14     400   .75 0     
float-newlib/float_req_bl_1092d_true-unreach-call.c 2 .11  .11  26 .92 .85 0   - - - - 2 3.7  2.1  250 0   0     2 22     14     390   .68 0     
float-newlib/float_req_bl_1121a_true-unreach-call.c 2 .098 .098 27 1.1  1.0  0   - - - - 2 5.3  2.9  280 0   0     2 70     60     570   .71 0     
float-newlib/float_req_bl_1121b_true-unreach-call.c 2 .13  .13  27 1.1  .85 0   - - - - 2 5.3  2.9  280 0   0     2 81     71     570   .71 0     
float-newlib/float_req_bl_1122a_true-unreach-call.c 2 .10  .10  27 1.1  .85 0   - - - - 2 4.8  2.7  310 0   0     2 59     51     590   .68 0     
float-newlib/float_req_bl_1122b_true-unreach-call.c 2 .11  .11  27 1.5  .85 0   - - - - 2 5.4  3.1  310 0   0     2 65     56     590   .71 0     
float-newlib/float_req_bl_1130a_true-unreach-call.c 2 .12  .12  27 1.2  1.0  0   - - - - 2 6.1  3.5  320 0   0     2 32     21     490   .75 0     
float-newlib/float_req_bl_1130b_true-unreach-call.c 2 .13  .13  27 1.1  1.0  0   - - - - 2 5.0  2.9  320 0   0     2 28     18     500   .75 0     
float-newlib/float_req_bl_1131a_true-unreach-call.c 2 .10  .10  27 1.1  1.0  0   - - - - 2 4.9  2.8  320 0   0     2 30     20     510   .75 0     
float-newlib/float_req_bl_1131b_true-unreach-call.c 2 .11  .11  27 1.2  .85 0   - - - - 2 6.6  3.7  320 0   0     2 27     18     500   .71 0     
float-newlib/float_req_bl_1211a_true-unreach-call.c 2 .087 .090 27 1.1  1.0  0   - - - - 2 4.1  2.3  250 0   0     2 24     15     470   .75 0     
float-newlib/float_req_bl_1211b_true-unreach-call.c 2 .10  .10  26 1.1  1.0  0   - - - - 2 3.9  2.2  250 0   0     2 25     16     460   .75 0     
float-newlib/float_req_bl_1230_true-unreach-call.c 2 .11  .11  26 1.0  1.0  0   - - - - 2 4.1  2.3  250 0   0     2 24     15     450   .75 0     
float-newlib/float_req_bl_1231_true-unreach-call.c 2 .11  .11  26 1.0  1.0  0   - - - - 2 4.5  2.6  260 0   0     2 57     40     710   .68 0     
float-newlib/float_req_bl_1232a_true-unreach-call.c 2 .086 .086 26 1.0  1.0  0   - - - - 2 4.2  2.3  250 0   0     2 21     13     440   .75 0     
float-newlib/float_req_bl_1250_true-unreach-call.c 2 .082 .082 26 .87 1.0  0   - - - - 2 5.1  2.8  250 0   0     2 26     15     460   .75 0     
float-newlib/float_req_bl_1251_true-unreach-call.c 2 .095 .095 26 1.1  1.0  0   - - - - 2 6.0  3.4  270 0   0     2 65     47     720   .71 0     
float-newlib/float_req_bl_1252a_true-unreach-call.c 2 .090 .090 26 .78 .85 0   - - - - 2 4.7  2.6  250 0   0     2 25     15     440   .75 0     
float-newlib/float_req_bl_1270a_true-unreach-call.c 2 3.0   3.0   110 36    1.0  0   - - - - 2 7.9  5.3  420 0   0     2 120     110     730   .71 0     
float-newlib/float_req_bl_1270b_true-unreach-call.c 2 3.0   3.0   110 33    .85 0   - - - - 2 7.8  5.3  420 0   0     2 130     120     760   .71 0     
float-newlib/float_req_bl_1270c_true-unreach-call.c 2 3.0   3.0   110 40    1.0  0   - - - - 2 7.7  5.2  420 0   0     2 290     270     820   .71 0     
float-newlib/float_req_bl_1270d_true-unreach-call.c 2 3.0   3.0   110 39    1.0  0   - - - - 2 8.3  5.6  420 0   0     2 270     260     780   .71 0     
float-newlib/float_req_bl_1271a_true-unreach-call.c 2 3.0   3.0   110 36    .85 0   - - - - 2 8.1  5.4  420 0   0     2 340     320     940   .71 0     
float-newlib/float_req_bl_1271b_true-unreach-call.c 2 3.0   3.0   110 47    1.0  0   - - - - 2 8.9  6.0  420 0   0     2 430     420     970   .71 0     
float-newlib/float_req_bl_1381_true-unreach-call.c 2 .084 .084 26 .83 1.0  0   - - - - 2 4.9  2.7  260 0   0     2 21     12     320   .75 0     
float-newlib/double_req_bl_0870a_false-unreach-call.c 1 .26  .26  40 3.0  1.0  0   0 98    85    1700 0     0   0 60     51     1400   .71 0   0 4.2  2.3  250 0   0    1 .68   .67   20    .14  0      - -
float-newlib/double_req_bl_1210_false-unreach-call.c 1 .11  .11  27 1.1  .85 0   -32 4.5  2.5  250 0     0   0 15     9.3   300   .68 0   0 3.6  2.1  250 0   0    1 .61   .60   20    .057 0      - -
float-newlib/double_req_bl_1232b_false-unreach-call.c 1 .095 .095 26 1.1  .85 0   -32 4.4  2.4  250 0     0   0 14     8.3   310   .68 0   0 3.6  2.1  250 0   0    1 .58   .58   20    .057 0      - -
float-newlib/double_req_bl_1252b_false-unreach-call.c 1 .090 .093 26 1.2  1.0  0   -32 4.3  2.4  250 0     0   0 14     7.8   310   .68 0   0 4.5  2.5  250 0   0    1 .61   .60   20    .057 0      - -
float-newlib/float_req_bl_0870a_false-unreach-call.c 1 .19  .19  32 2.4  .85 0   -32 5.4  2.9  260 0     0   0 40     31     630   .68 0   0 4.3  2.4  260 0   0    1 .65   .65   20    .13  0      - -
float-newlib/float_req_bl_1210_false-unreach-call.c 1 .11  .11  26 .89 .85 0   -32 4.0  2.2  250 0     0   0 15     9.2   300   .71 0   0 3.7  2.1  250 0   0    1 .58   .58   20    .057 0      - -
float-newlib/float_req_bl_1232b_false-unreach-call.c 1 .090 .091 26 1.1  .85 0   -32 4.1  2.3  250 0     0   0 13     7.6   300   .71 0   0 3.6  2.0  250 0   0    1 .58   .58   20    .057 0      - -
float-newlib/float_req_bl_1252b_false-unreach-call.c 1 .10  .10  26 .84 .85 0   -32 4.1  2.3  250 0     0   0 14     7.7   300   .75 0   0 3.6  2.1  250 0   0    1 .58   .58   20    .057 .0041 - -
loop-floats-scientific-comp/loop1_true-unreach-call.c.i 0 900     900     270 12000    1.0  0   - - - - 0 .63 .39 40 0   0     0 .027 .028 5.6 0    0     
loop-floats-scientific-comp/loop2_true-unreach-call.c.i 0 900     900     250 11000    1.0  0   - - - - 0 .64 .38 41 0   0     0 .023 .024 5.6 0    0     
loop-floats-scientific-comp/loop3_true-unreach-call.c.i 0 900     900     260 10000    1.0  0   - - - - 0 .73 .45 43 0   0     0 .023 .024 5.7 0    0     
loop-floats-scientific-comp/loop5_true-unreach-call.c.i 0 900     900     1700 9600    1.0  0   - - - - 0 .74 .45 41 0   0     0 .022 .022 5.6 0    0     
loop-floats-scientific-comp/loop1_false-unreach-call.c.i 1 1.6   1.6   46 21    .85 0   -32 4.2  2.4  250 0     0   1 18     13     400   .71 0   1 3.5  2.1  250 0   0    1 .59   .59   20    .053 0      - -
loop-floats-scientific-comp/loop2_false-unreach-call.c.i 1 1.3   1.3   42 21    1.0  0   1 4.9  3.1  280 0     0   1 27     20     520   .68 0   1 4.2  2.4  250 0   .13 1 .59   .58   20    .057 0      - -
loop-floats-scientific-comp/loop4_false-unreach-call.c.i 0 900     900     2200 9700    .86 0   0 .62 .38 40 0     0   0 .022 .023 5.8 0    0   0 .99 .65 47 0   0    0 .0016 .0020 .53 0     0      - -
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 469 790 38000 38000 140000 440000 450    0   45 -753 440 320 14000 .016 0   45 -16 2400 2200 27000 47    0   45 28 160 92 11000 0   .13 45 -27 25   25   860 2.3   .029  424 704 32000 31000 240000 0   .61 424 626 79000 74000 380000 290 .0082
    correct results 432 822 7600 7600 30000 93000 410    0   15 15 210 160 4900 0     0   16 16 430 330 8500 11    0   28 28 100 59 6900 0   .13 37 37 22   22   750 2.1   .020  352 704 6700 5800 200000 0   .61 313 626 31000 28000 290000 230 0     
        correct true 390 780 6600 6600 26000 80000 370    0   0 0 0 0 352 704 6700 5800 200000 0   .61 313 626 31000 28000 290000 230 0     
        correct false 42 42 1100 1100 4100 14000 39    0   15 15 210 160 4900 0     0   16 16 430 330 8500 11    0   28 28 100 59 6900 0   .13 37 37 22   22   750 2.1   .020  0 0
    incorrect results 1 -32 450 450 530 4300 .85 0   24 -768 100 56 6000 0     0   1 -32 68 62 830 .68 0   0 2 -64 1.2 1.2 40 .090 .0082 0 0
        incorrect true 1 -32 450 450 530 4300 .85 0   24 -768 100 56 6000 0     0   1 -32 68 62 830 .68 0   0 2 -64 1.2 1.2 40 .090 .0082 0 0
        incorrect false 0 0 0 0 0 0 0
score (469 tasks, max score: 893) 790 -753 -16 28 -27 704 626
Run set esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats