Tool CBMC 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*
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-04 22:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 07:35:27 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options --graphml-witness witness.graphml -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/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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 14     14     60   150    .0082 0      1 46    44    350 0   0   1 36     30     680   .71 0   1 3.7  2.2  250 0     .11  1 .58   .58   20    .053 0      - -
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i 1 6.6   6.6   47   72    .0082 0      1 12    10    350 0   0   0 97     90     700   .75 0   1 3.6  2.1  250 0     0     1 .62   .63   20    .053 .0082 - -
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i 1 4.3   4.3   42   44    .0082 0      1 39    37    350 0   0   1 77     71     690   .68 0   1 3.6  2.1  250 0     0     1 .60   .60   20    .053 .070  - -
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i 1 8.4   8.4   49   87    .0082 0      1 13    11    350 0   0   0 97     91     700   .76 0   1 3.6  2.1  250 0     .057 1 .58   .58   20    .053 0      - -
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i 1 7.4   7.4   49   95    .0082 0      1 11    8.9  350 0   0   1 30     25     680   .68 0   1 3.6  2.1  250 0     0     1 .60   .60   20    .053 0      - -
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i 1 77     77     160   660    .0082 0      -32 4.7  2.6  250 0   0   0 97     91     800   .78 0   1 4.2  2.4  250 0     0     1 .57   .57   20    .053 0      - -
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i 1 120     120     230   1200    .0082 0      -32 5.1  2.8  250 0   0   0 97     91     810   .92 0   1 3.7  2.2  240 0     0     1 .59   .59   20    .053 0      - -
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i 1 25     25     100   310    .0082 0      -32 4.7  2.6  250 0   0   1 39     33     820   .71 0   1 3.7  2.2  250 0     0     1 .58   .58   20    .053 .0041 - -
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i 1 430     430     480   4500    .0082 0      -32 4.7  2.6  250 0   0   0 97     90     880   .73 0   1 3.9  2.2  240 0     0     1 .60   .60   20    .053 0      - -
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i 1 75     75     200   830    .0082 0      -32 4.3  2.4  250 0   0   1 52     46     920   .68 0   1 3.7  2.2  250 0     0     1 .58   .58   20    .053 0      - -
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i 1 55     55     180   540    .0082 0      -32 4.3  2.4  250 0   0   0 97     91     920   .82 0   1 3.8  2.2  250 0     0     1 .58   .59   20    .053 0      - -
floats-cdfpl/sine_1_false-unreach-call_true-termination.i 1 .90  .89  22   10    .0082 0      1 12    9.5  300 0   0   0 97     91     610   1.6  0   1 3.6  2.1  250 0     0     1 .57   .57   20    .049 0      - -
floats-cdfpl/sine_2_false-unreach-call_true-termination.i 1 4.1   4.1   31   58    .0082 0      -32 4.3  2.3  250 0   0   0 97     91     570   .73 0   1 3.9  2.3  250 0     0     1 .57   .57   20    .049 .0041 - -
floats-cdfpl/sine_3_false-unreach-call_true-termination.i 1 .98  .97  21   13    .0082 0      -32 4.6  2.5  250 0   0   0 97     91     600   1.6  0   1 3.8  2.2  250 0     .11  1 .57   .57   20    .049 0      - -
floats-cdfpl/square_1_false-unreach-call_true-termination.i 1 1.7   1.7   24   21    .0082 0      -32 4.1  2.3  250 0   0   1 84     78     430   .68 0   1 3.4  2.0  240 0     0     1 .57   .57   20    .049 0      - -
floats-cdfpl/square_2_false-unreach-call_true-termination.i 0 1.8   1.7   24   21    .0082 0      -32 4.2  2.3  250 0   0   0 97     92     450   .69 0   -32 3.7  2.1  250 0     0     -32 .58   .58   20    .049 0      - -
floats-cdfpl/square_3_false-unreach-call_true-termination.i 0 1.5   1.5   23   19    .0082 0      -32 4.5  2.5  250 0   0   0 97     91     460   .72 0   -32 3.8  2.2  250 0     0     -32 .57   .58   20    .049 0      - -
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i 2 230     230     150   2200    .0082 0      - - - - 0 900    900    580 0   0   0 960     950     970   .72 0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i 2 140     140     110   1100    .0082 0      - - - - 0 900    900    590 0   0   0 960     950     790   .72 0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i 2 170     170     110   1600    .0082 0      - - - - 0 900    900    580 0   0   0 960     950     970   1.3  0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i 2 260     260     210   3100    .0082 0      - - - - 0 900    900    520 0   0   0 960     950     890   .72 0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i 2 550     550     310   4600    .0082 0      - - - - 0 900    900    830 0   0   0 960     950     970   .71 0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i 2 350     350     340   2900    .0082 0      - - - - 0 900    900    520 0   0   0 960     950     1000   .69 0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i 2 550     550     360   4800    .0082 0      - - - - 0 900    900    560 0   0   0 960     950     1000   .72 0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i 2 830     830     590   8000    .0082 0      - - - - 0 900    900    540 0   0   0 960     950     890   .72 0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i 0 870     880     550   9600    .057  0      - - - - 0 .63 .39 41 0   0   0 .021 .021 5.5 0    0     
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i 0 880     880     480   6000    .057  0      - - - - 0 .63 .38 40 0   0   0 .030 .031 5.8 0    0     
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i 0 880     880     550   7900    .057  0      - - - - 0 .71 .43 41 0   0   0 .029 .030 5.6 0    0     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i 0 880     880     540   8500    .053  0      - - - - 0 .76 .46 42 0   0   0 .028 .029 5.5 0    0     
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i 0 880     880     850   8200    .057  0      - - - - 0 .66 .41 40 0   0   0 .027 .028 5.6 0    0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i 2 710     710     85   8100    .0082 0      - - - - 0 900    900    500 0   0   0 960     950     790   1.3  0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i 2 220     220     77   3100    .0082 .13   - - - - 0 900    900    490 0   0   0 960     950     830   .72 0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i 2 19     19     44   280    .0082 0      - - - - 0 900    900    650 0   0   0 960     950     830   .71 0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i 2 5.9   5.9   29   81    .0082 0      - - - - 2 710    710    590 0   0   0 960     950     840   .72 0     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i 2 62     62     60   680    .0082 0      - - - - 2 550    540    540 0   0   0 960     950     810   .69 0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i 2 270     270     110   3600    .0082 0      - - - - 2 570    570    570 0   0   0 960     950     670   .72 0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i 2 260     260     110   3100    .0082 0      - - - - 2 400    390    510 0   0   0 960     950     760   .73 0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i 2 93     93     62   1200    .0082 0      - - - - 2 270    270    500 0   0   0 960     950     770   1.3  0     
floats-cdfpl/square_7_true-unreach-call_true-termination.i 2 66     66     56   860    .0082 0      - - - - 0 900    900    480 0   0   2 610     610     790   .71 0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i 2 1.8   1.8   21   26    .0082 0      - - - - 2 72    70    360 0   0   2 80     75     610   .71 0     
floats-cbmc-regression/float-div1_true-unreach-call.i 2 .34  .34  15   5.2  .016  .34   - - - - 2 5.5  3.4  320 0   0   2 46     39     950   .71 0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 2 .29  .29  24   3.1  .016  .39   - - - - 2 13    10    780 0   0   0 14     8.3   290   .75 0     
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i 2 .043 .040 7.3 .33 .0082 0      - - - - 2 3.6  2.0  250 0   0   2 15     8.6   300   .71 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 2 1.7   1.7   10   19    .016  0      - - - - 2 20    17    300 0   0   2 55     46     550   .71 0     
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i 2 .050 .049 7.7 .39 .0082 0      - - - - 2 3.5  1.9  250 0   0   2 12     7.3   300   .75 0     
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 2 .17  .17  9.3 2.6  .016  .090  - - - - 2 5.6  3.0  290 0   0   2 20     12     450   .64 0     
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i 2 .043 .041 6.6 .40 .0082 0      - - - - 2 4.4  2.4  250 0   0   2 17     11     300   .75 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i 2 .11  .10  5.6 .24 .0082 0      - - - - 2 3.9  2.2  250 0   0   2 15     8.4   300   .75 0     
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 .079 .077 8.0 .80 .016  0      - - - - 2 5.8  3.2  260 0   0   0 15     8.0   290   .75 0     
floats-cbmc-regression/float-rounding1_true-unreach-call.i 2 .087 .085 7.2 .78 .016  0      - - - - 0 5.6  3.1  260 0   0   0 8.0   4.6   280   .66 0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i 2 .14  .14  6.8 1.2  .016  0      - - - - 2 5.3  2.9  270 0   0   2 37     29     450   .68 0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i 2 .049 .046 6.2 .25 .0082 0      - - - - 2 3.7  2.0  250 0   0   2 15     8.5   300   .71 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i 2 .052 .049 6.5 .31 .0082 0      - - - - 2 4.4  2.4  250 0   0   2 17     9.8   310   .75 0     
floats-cbmc-regression/float11_true-unreach-call_true-termination.i 2 .047 .045 6.6 .37 .0082 0      - - - - 2 3.8  2.1  250 0   0   2 16     9.2   300   .71 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i 2 .085 .082 6.4 .76 .0082 0      - - - - 2 3.7  2.1  250 0   0   2 23     17     300   .75 0     
floats-cbmc-regression/float13_true-unreach-call_true-termination.i 2 .054 .052 6.4 .32 .0082 0      - - - - 2 4.4  2.5  250 0   0   2 16     9.4   310   .75 0     
floats-cbmc-regression/float14_true-unreach-call.i 2 .11  .10  7.7 .84 .016  0      - - - - 2 5.6  3.1  260 0   0   2 18     10     390   .75 0     
floats-cbmc-regression/float18_true-unreach-call.i 2 .19  .19  7.8 2.3  .078  0      - - - - 0 6.1  3.3  300 0   0   0 16     9.2   290   .75 0     
floats-cbmc-regression/float19_true-unreach-call.i 2 .097 .094 7.1 .72 .016  0      - - - - 2 6.0  3.2  260 0   0   2 18     10     390   .75 0     
floats-cbmc-regression/float1_true-unreach-call_true-termination.i 2 .078 .074 6.1 .22 .0082 .049  - - - - 2 3.7  2.1  250 0   0   2 16     9.4   300   .75 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i 2 .095 .092 7.9 .85 .0082 0      - - - - 2 3.4  1.9  250 0   0   2 22     15     370   .75 0     
floats-cbmc-regression/float21_true-unreach-call.i 2 .21  .21  8.4 2.6  .016  .11   - - - - 2 8.9  6.7  290 0   0   2 86     75     580   .71 0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i 2 .060 .058 6.4 .55 .0082 0      - - - - 2 4.2  2.4  270 0   0   2 220     200     740   .71 0     
floats-cbmc-regression/float2_true-unreach-call_true-termination.i 2 .072 .067 5.9 .27 .0082 0      - - - - 2 3.5  2.0  250 0   0   2 16     9.6   310   .75 0     
floats-cbmc-regression/float3_true-unreach-call_true-termination.i 2 .078 .076 7.2 .76 .0082 0      - - - - 2 4.4  2.5  270 0   0   2 20     13     320   .71 0     
floats-cbmc-regression/float4_true-unreach-call.i 2 9.7   9.7   25   130    .016  0      - - - - 2 74    72    330 0   0   2 92     84     590   .68 0     
floats-cbmc-regression/float5_true-unreach-call_true-termination.i 2 .075 .073 6.3 .60 .0082 0      - - - - 2 3.5  2.0  260 0   0   2 32     26     290   .75 0     
floats-cbmc-regression/float6_true-unreach-call_true-termination.i 2 .069 .067 5.9 .49 .0082 0      - - - - 2 4.2  2.3  250 0   0   2 15     8.8   310   .75 0     
floats-cbmc-regression/float8_true-unreach-call.i 2 .63  .63  7.7 8.6  .016  0      - - - - 2 7.6  5.6  270 0   0   2 16     9.8   390   .71 0     
floats-cbmc-regression/float_lib1_true-unreach-call.i 2 .14  .14  8.6 1.8  .016  0      - - - - 2 5.9  3.1  260 0   0   0 14     8.1   280   .75 0     
floats-cbmc-regression/float_lib2_true-unreach-call.i 2 .13  .12  8.3 1.1  .016  .090  - - - - 2 5.1  2.8  260 0   0   2 17     10     420   .71 0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c 1 .068 .061 9.2 .61 .0082 0      1 4.1  2.3  260 0   0   1 18     11     310   .75 0   0 3.7  2.1  250 0     0     0 .58   .61   20    .037 0      - -
float-benchs/cast_union_loose_false-unreach-call_true-termination.c 1 .083 .071 9.5 .57 .0082 0      1 4.2  2.4  270 0   0   1 14     8.6   310   .75 0   1 4.0  2.3  240 0     0     1 .59   .59   20    .057 0      - -
float-benchs/cast_union_tight_false-unreach-call_true-termination.c 1 .085 .075 9.6 .68 .0082 0      1 5.0  2.9  270 0   0   1 17     9.8   320   .71 0   1 3.8  2.2  250 0     0     1 .61   .62   20    .057 0      - -
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c 1 .091 .081 9.0 .89 .0082 0      1 4.7  2.6  260 0   0   1 16     9.6   310   .75 0   1 3.7  2.1  240 0     0     1 .59   .59   20    .053 0      - -
float-benchs/inv_Newton_false-unreach-call.c 0 880     880     780   5900    .074  0      0 .58 .36 41 0   0   0 .028 .030 5.7 0    0   0 .95 .65 47 0     0     0 .0018 .0022 .52 0     0      - -
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c 0 880     880     12000   4900    15      0      0 .66 .39 42 0   0   0 .026 .027 5.6 0    0   0 1.0  .69 48 0     0     0 .0051 .0061 .54 0     0      - -
float-benchs/inv_square_false-unreach-call_true-termination.c 1 .073 .065 9.7 .70 .0082 0      1 4.8  2.7  260 0   0   1 14     8.3   300   .75 0   1 3.7  2.2  250 0     0     1 .60   .61   20    .053 0      - -
float-benchs/nan_double_false-unreach-call_true-termination.c 1 .071 .059 9.0 .40 .0082 0      1 4.7  2.6  260 0   0   1 13     7.8   300   .71 0   0 3.6  2.1  250 0     0     0 .56   .56   20    .037 0      - -
float-benchs/nan_float_false-unreach-call_true-termination.c 1 .054 .044 9.3 .69 .0082 0      1 4.9  2.7  260 0   0   1 12     7.0   300   .75 0   0 3.7  2.2  250 0     0     0 .56   .55   20    .037 0      - -
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c 1 2.6   2.6   190   29    .0082 0      1 8.9  6.1  380 0   0   1 34     25     1000   .68 0   1 4.5  2.6  260 0     0     1 .62   .62   20    .086 0      - -
float-benchs/sqrt_poly2_false-unreach-call.c 1 .53  .52  35   5.9  .0082 0      -32 5.6  3.1  260 0   0   1 26     19     610   .75 0   1 4.4  2.4  270 0     0     1 .60   .60   20    .061 .17   - -
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c 2 .34  .33  7.0 3.0  .35   0      - - - - 0 10    6.5  520 0   0   0 960     900     2500   1.3  0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c 2 .31  .30  6.5 3.4  .35   0      - - - - 0 10    6.6  520 0   0   0 960     890     4400   .68 0     
float-benchs/Rump_double_true-unreach-call_true-termination.c 2 .049 .046 6.9 .39 .0082 0      - - - - 2 4.4  2.5  250 0   0   2 29     23     990   .71 0     
float-benchs/Rump_float_true-unreach-call_true-termination.c 2 .056 .054 7.1 .31 .0082 0      - - - - 2 4.4  2.5  250 0   0   2 19     12     430   .75 0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c 2 .051 .049 7.0 .46 .0082 0      - - - - 2 4.8  2.7  250 0   0   2 14     8.4   290   .71 0     
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c 2 .050 .048 7.0 .32 .0082 0      - - - - 2 4.2  2.3  250 0   0   2 15     8.7   300   .75 0     
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c 2 .049 .046 7.4 .41 .0082 0      - - - - 2 3.5  1.9  250 0   0   2 15     8.9   300   .71 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c 2 97     97     300   1100    .0082 0      - - - - 2 32    30    500 0   0   0 150     140     2600   .71 0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c 0 880     880     1400   9900    .77   0      - - - - 0 .72 .45 41 0   0   0 .027 .027 5.6 0    0     
float-benchs/cast_float_union_true-unreach-call.c 2 .13  .12  5.7 .29 .0082 0      - - - - 2 3.5  2.0  250 0   0   2 7.2   4.1   300   .62 0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c 2 48     48     96   360    .0082 0      - - - - 0 900    900    1300 0   0   0 960     950     3000   .71 0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c 0 880     880     3100   5900    5.1    0      - - - - 0 .75 .45 40 0   0   0 .025 .027 5.6 0    0     
float-benchs/divmul_diverge_true-unreach-call_true-termination.c 0 880     880     6200   6900    7.7    0      - - - - 0 .63 .39 41 0   0   0 .028 .028 5.6 0    0     
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c 2 .095 .089 7.1 .71 .037  0      - - - - 0 5.2  2.9  290 0   0   2 380     370     660   .71 0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c 2 .080 .077 7.2 .56 .037  0      - - - - 0 5.0  2.8  290 0   0   2 290     280     610   .68 0     
float-benchs/exp_loop_true-unreach-call.c 2 1.0   1.0   20   15    .46   0      - - - - 0 9.2  5.5  440 0   0   0 960     950     1200   .72 0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c 0 880     880     1800   9100    .75   0      - - - - 0 .71 .44 41 0   0   0 .024 .024 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c 0 880     880     2500   9400    13      0      - - - - 0 .73 .45 40 0   0   0 .026 .027 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c 0 880     880     2800   8700    41      0      - - - - 0 .69 .42 40 0   0   0 .022 .030 5.7 0    0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c 0 880     880     2800   11000    41      0      - - - - 0 .76 .46 41 0   0   0 .027 .028 5.6 0    0     
float-benchs/filter1_true-unreach-call_true-termination.c 0 880     880     1600   9500    .40   0      - - - - 0 .71 .43 41 0   0   0 .025 .025 5.6 0    0     
float-benchs/filter2_alt_true-unreach-call.c 0 880     880     340   9600    .074  0      - - - - 0 .59 .38 40 0   0   0 .022 .022 5.6 0    0     
float-benchs/filter2_iterated_true-unreach-call.c 0 560     560     15000   8100    20      .0041 - - - - 0 .60 .36 42 0   0   0 .024 .024 5.6 0    0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c 0 880     880     740   8700    .12   0      - - - - 0 .69 .42 40 0   0   0 .022 .022 5.6 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c 0 880     880     1800   8100    .070  0      - - - - 0 .59 .37 41 0   0   0 .027 .027 5.7 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c 0 870     880     710   9700    .11   0      - - - - 0 .66 .40 40 0   0   0 .021 .022 5.6 0    0     
float-benchs/filter_iir_true-unreach-call.c 0 880     880     850   7300    .12   0      - - - - 0 .73 .46 41 0   0   0 .021 .022 5.7 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c 2 .050 .047 7.8 .32 .0082 0      - - - - 2 4.1  2.3  250 0   0   2 13     7.9   310   .75 0     
float-benchs/image_filter_true-unreach-call.c 0 880     880     3000   6600    2.6    0      - - - - 0 .71 .44 40 0   0   0 .028 .030 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c 2 .91  .91  29   11    .057  0      - - - - 0 900    900    1400 0   0   0 960     950     1500   1.3  0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c 2 .94  .94  29   13    .057  0      - - - - 0 900    900    920 0   0   0 960     950     1500   .84 0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c 2 1.1   1.1   29   13    .057  0      - - - - 2 190    190    690 0   0   0 960     950     1600   .71 0     
float-benchs/interpolation2_true-unreach-call_true-termination.c 2 .52  .51  12   7.4  .025  0      - - - - 0 900    900    1300 0   0   0 960     950     1600   .72 0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c 2 .62  .61  20   6.5  .057  0      - - - - 2 530    530    1500 0   0   0 960     950     1500   .72 0     
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c 2 .58  .58  20   8.0  .057  0      - - - - 2 650    640    1500 0   0   0 960     950     1400   .70 .0082
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c 2 .67  .67  21   8.3  .057  0      - - - - 2 180    180    560 0   0   0 960     950     1500   .71 0     
float-benchs/interpolation_true-unreach-call_true-termination.c 2 .25  .25  8.7 3.0  .025  0      - - - - 0 900    900    1700 0   0   0 960     950     1600   .72 0     
float-benchs/inv_Newton_true-unreach-call.c 0 880     880     440   7200    .074  0      - - - - 0 .69 .42 42 0   0   0 .027 .027 5.6 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c 2 .39  .38  18   5.2  .0082 0      - - - - 2 7.0  5.2  310 0   0   2 95     86     1200   .71 0     
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c 2 .46  .46  12   5.7  .0082 0      - - - - 2 5.4  3.3  280 0   0   2 83     76     520   .71 0     
float-benchs/inv_square_int_true-unreach-call_true-termination.c 2 .14  .14  6.9 .92 .0082 0      - - - - 2 3.9  2.2  260 0   0   2 21     15     340   .75 0     
float-benchs/inv_square_true-unreach-call_true-termination.c 2 .14  .14  6.3 .59 .0082 0      - - - - 2 3.6  2.1  260 0   0   2 75     69     350   .71 0     
float-benchs/loop_true-unreach-call.c 0 360     360     15000   5500    6.4    0      - - - - 0 .64 .39 40 0   0   0 .025 .026 5.6 0    0     
float-benchs/mea8000_true-unreach-call.c 0 250     250     14000   2900    14      0      - - - - 0 .76 .46 41 0   0   0 .027 .028 5.6 0    0     
float-benchs/nan_double_range_true-unreach-call_true-termination.c 2 .050 .046 6.1 .36 .0082 0      - - - - 2 4.2  2.4  250 0   0   2 15     8.6   300   .75 0     
float-benchs/nan_float_range_true-unreach-call_true-termination.c 2 .067 .065 6.6 .33 .0082 0      - - - - 2 3.4  1.9  250 0   0   2 13     8.5   290   .75 0     
float-benchs/rlim_exit_true-unreach-call_true-termination.c 0 880     880     5300   6600    16      0      - - - - 0 .68 .41 42 0   0   0 .022 .023 5.6 0    0     
float-benchs/rlim_invariant_true-unreach-call.c.p+cfa-reducer.c 0 880     880     1500   7900    2.1    0      - - - - 0 .71 .43 40 0   0   0 .020 .021 5.6 0    0     
float-benchs/rlim_invariant_true-unreach-call.c.v+lhb-reducer.c 0 880     880     2500   6700    3.0    0      - - - - 0 .59 .37 40 0   0   0 .024 .025 5.6 0    0     
float-benchs/rlim_invariant_true-unreach-call.c.v+nlh-reducer.c 0 880     880     2500   6500    3.0    0      - - - - 0 .94 .56 41 0   0   0 .026 .027 5.6 0    0     
float-benchs/rlim_invariant_true-unreach-call_true-termination.c 0 880     880     1100   6300    3.4    0      - - - - 0 .67 .42 41 0   0   0 .023 .024 5.6 0    0     
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c 0 880     880     630   7100    .074  0      - - - - 0 .71 .44 41 0   0   0 .026 .027 5.6 0    0     
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c 0 880     880     630   7700    .074  0      - - - - 0 .74 .44 40 0   0   0 .021 .022 5.6 0    0     
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c 0 880     880     610   8100    .074  0      - - - - 0 .57 .36 40 0   0   0 .022 .023 5.6 0    0     
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 880     880     4900   6900    .89   0      - - - - 0 .62 .39 41 0   0   0 .027 .028 5.6 0    0     
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 870     880     3500   6800    .92   0      - - - - 0 .73 .45 40 0   0   0 .022 .024 5.7 0    0     
float-benchs/sqrt_Householder_constant_true-unreach-call.c 2 .85  .84  10   13    .99   0      - - - - 0 16    10    820 0   0   0 260     240     3100   .71 0     
float-benchs/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c 2 1.1   1.1   13   14    1.4    0      - - - - 0 21    13    930 0   0   0 560     550     3600   .71 0     
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 880     880     820   6700    .074  0      - - - - 0 .60 .38 40 0   0   0 .026 .027 5.7 0    0     
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 880     880     2700   8900    .082  0      - - - - 0 .58 .35 41 0   0   0 .027 .029 5.7 0    0     
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 880     880     2600   7900    .082  0      - - - - 0 .65 .40 40 0   0   0 .028 .029 5.5 0    0     
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 880     880     3300   8900    .082  0      - - - - 0 .69 .42 40 0   0   0 .026 .029 5.7 0    0     
float-benchs/sqrt_poly_true-unreach-call_true-termination.c 2 2.0   2.0   43   23    .0082 0      - - - - 2 46    44    490 0   0   2 130     130     1100   .71 0     
float-benchs/water_pid_true-unreach-call_true-termination.c 2 .59  .58  11   7.7  .82   0      - - - - 0 11    6.1  560 0   0   0 200     190     3000   .71 0     
float-benchs/zonotope_2_true-unreach-call_true-termination.c 2 110     110     4500   1500    430      .0082 - - - - 0 960    500    5500 0   0   0 960     920     5400   .64 0     
float-benchs/zonotope_3_true-unreach-call.c.p+cfa-reducer.c 0 870     880     13000   8700    38      0      - - - - 0 .60 .37 41 0   0   0 .021 .022 5.6 0    0     
float-benchs/zonotope_3_true-unreach-call.c.v+lhb-reducer.c 0 880     880     13000   10000    48      0      - - - - 0 .73 .45 40 0   0   0 .021 .022 5.6 0    0     
float-benchs/zonotope_3_true-unreach-call_true-termination.c 0 250     250     14000   2800    17      0      - - - - 0 .60 .38 40 0   0   0 .025 .027 5.7 0    0     
float-benchs/zonotope_loose_true-unreach-call.c.v+cfa-reducer.c 2 .40  .40  23   5.0  .0082 0      - - - - 2 5.7  3.7  310 0   0   2 220     210     850   .71 0     
float-benchs/zonotope_loose_true-unreach-call_true-termination.c 2 .34  .34  17   4.0  .0082 0      - - - - 2 5.7  3.6  310 0   0   2 140     130     1100   .68 0     
float-benchs/zonotope_tight_true-unreach-call_true-termination.c 2 .25  .25  17   3.0  .0082 0      - - - - 2 4.8  3.1  310 0   0   2 200     190     1100   .68 0     
floats-esbmc-regression/Double_div_true-unreach-call.i 2 1.7   1.7   14   18    1.3    0      - - - - 0 15    8.0  670 0   0   2 210     200     2800   .71 0     
floats-esbmc-regression/Float_div_true-unreach-call.i 2 .19  .18  6.6 2.0  .23   0      - - - - 0 6.8  3.7  310 0   0   2 220     210     630   .71 0     
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 2 4.5   4.5   34   54    .033  .11   - - - - 0 4.8  2.6  260 0   0   0 12     7.0   290   .75 0     
floats-esbmc-regression/ceil_true-unreach-call.i 2 .21  .21  11   2.9  .033  .11   - - - - 2 5.2  2.8  280 0   0   0 13     7.7   280   .68 0     
floats-esbmc-regression/copysign_true-unreach-call.i 2 .17  .16  10   1.7  .025  0      - - - - 2 5.3  2.9  250 0   0   0 12     6.7   290   .68 0     
floats-esbmc-regression/digits_for_true-unreach-call.i 2 .24  .23  6.1 2.7  .23   0      - - - - 0 7.2  4.0  310 0   0   0 960     950     3100   .72 0     
floats-esbmc-regression/digits_while_true-unreach-call.i 2 .29  .28  7.0 3.7  .23   0      - - - - 0 6.2  3.5  310 0   0   0 960     950     3100   1.1  0     
floats-esbmc-regression/fabs_true-unreach-call.i 2 .090 .087 7.9 .86 .016  0      - - - - 2 4.3  2.4  250 0   0   2 19     11     390   .75 0     
floats-esbmc-regression/fdim_true-unreach-call.i 2 .11  .11  8.3 1.0  .016  .090  - - - - 2 4.4  2.4  260 0   0   2 17     9.6   410   .71 0     
floats-esbmc-regression/floor_nondet_true-unreach-call.i 2 4.5   4.5   34   59    .033  .41   - - - - 0 5.8  3.1  260 0   0   0 16     8.9   290   .75 0     
floats-esbmc-regression/floor_true-unreach-call.i 2 .21  .21  11   2.5  .033  .11   - - - - 2 5.3  2.9  260 0   0   0 13     7.6   290   .75 0     
floats-esbmc-regression/fmax_true-unreach-call.i 2 .12  .12  8.0 1.3  .016  .090  - - - - 2 4.5  2.5  260 0   0   2 17     9.4   400   .68 0     
floats-esbmc-regression/fmin_true-unreach-call.i 2 .12  .11  8.4 1.3  .016  .090  - - - - 2 5.8  3.2  260 0   0   2 15     8.5   400   .75 0     
floats-esbmc-regression/fmod2_true-unreach-call.i 2 .21  .20  11   2.3  .041  .016  - - - - 2 9.4  7.1  470 0   0   0 14     8.0   290   .75 0     
floats-esbmc-regression/fmod3_true-unreach-call.i 2 .22  .21  11   2.5  .041  0      - - - - 2 9.5  7.2  470 0   0   0 15     8.3   290   .71 0     
floats-esbmc-regression/fmod_true-unreach-call.i 2 .22  .22  11   2.6  .041  .11   - - - - 2 4.6  2.5  260 0   0   0 16     9.1   290   .75 0     
floats-esbmc-regression/isgreater_true-unreach-call.i 2 .078 .076 7.9 .73 .016  0      - - - - 2 4.9  2.7  260 0   0   2 17     9.9   390   .75 0     
floats-esbmc-regression/isgreaterequal_true-unreach-call.i 2 .074 .074 7.6 1.2  .016  0      - - - - 2 4.6  2.5  260 0   0   2 18     10     390   .71 0     
floats-esbmc-regression/isless_true-unreach-call.i 2 .076 .072 7.5 .67 .016  0      - - - - 2 4.6  2.5  260 0   0   2 19     11     390   .75 0     
floats-esbmc-regression/islessequal_true-unreach-call.i 2 .11  .10  7.2 .70 .016  0      - - - - 2 4.8  2.6  250 0   0   2 19     11     400   .71 0     
floats-esbmc-regression/islessgreater_true-unreach-call.i 2 .074 .072 7.4 .69 .016  0      - - - - 2 5.2  2.9  260 0   0   2 16     9.4   400   .68 0     
floats-esbmc-regression/isunordered_true-unreach-call.i 2 .079 .077 7.7 .78 .016  0      - - - - 2 5.4  3.0  260 0   0   2 19     11     390   .75 0     
floats-esbmc-regression/lrint_true-unreach-call.i 2 .22  .21  11   2.5  .033  0      - - - - 0 4.5  2.5  250 0   0   0 8.4   4.8   280   .62 0     
floats-esbmc-regression/modf_true-unreach-call.i 2 .18  .18  10   2.0  .033  .11   - - - - 2 4.6  2.5  250 0   0   0 7.2   4.2   290   .62 0     
floats-esbmc-regression/nan_true-unreach-call.i 2 .11  .11  7.4 .67 .016  0      - - - - 2 4.4  2.4  260 0   0   2 19     11     420   .71 0     
floats-esbmc-regression/nearbyint2_true-unreach-call.i 2 .22  .21  11   2.6  .033  0      - - - - 0 5.9  3.2  260 0   0   0 8.6   4.8   290   .66 0     
floats-esbmc-regression/nearbyint_true-unreach-call.i 2 .38  .37  11   4.8  .086  .11   - - - - 0 6.1  3.3  280 0   0   0 10     5.4   300   .66 0     
floats-esbmc-regression/remainder_true-unreach-call.i 2 .25  .24  11   3.0  .041  .11   - - - - 2 5.4  3.0  250 0   0   0 16     8.7   290   .75 0     
floats-esbmc-regression/rint2_true-unreach-call.i 2 .22  .22  11   3.0  .033  .13   - - - - 0 4.8  2.6  260 0   0   0 6.7   3.6   280   .66 0     
floats-esbmc-regression/rint_true-unreach-call.i 2 .38  .37  11   5.6  .086  .11   - - - - 0 6.3  3.4  300 0   0   0 8.7   4.8   290   .62 0     
floats-esbmc-regression/round_nondet_true-unreach-call.i 2 5.0   5.0   47   68    .025  .11   - - - - 0 5.6  3.0  250 0   0   0 13     7.4   290   .75 0     
floats-esbmc-regression/round_true-unreach-call.i 2 .24  .23  12   2.9  .033  .41   - - - - 2 4.9  2.7  260 0   0   0 15     8.6   290   .75 0     
floats-esbmc-regression/rounding_functions_true-unreach-call.i 2 .26  .26  11   3.1  .033  .41   - - - - 2 5.0  2.7  260 0   0   0 16     9.5   380   .71 0     
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 2 2.7   2.7   16   38    .033  .11   - - - - 2 6.2  4.1  270 0   0   0 110     99     610   .71 0     
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 2 3.1   3.1   34   47    .033  .11   - - - - 0 4.8  2.6  260 0   0   0 12     6.6   290   .71 0     
floats-esbmc-regression/trunc_true-unreach-call.i 2 .21  .21  12   2.9  .033  .38   - - - - 2 4.4  2.4  250 0   0   0 15     8.5   300   .75 0     
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 1 5.8   5.8   33   67    3.8    0      -32 21    11    740 0   0   0 97     73     6500   1.6  0   1 24    13    740 0     0     1 1.4    1.4    41    .045 .0041 - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 1 .53  .52  10   5.1  .61   0      -32 6.0  3.2  300 0   0   0 97     75     3800   .75 0   1 6.6  3.6  300 0     0     1 .69   .69   23    .045 0      - -
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 1 .27  .26  9.9 3.2  .29   0      -32 5.3  2.9  260 0   0   0 56     34     7000   .74 0   1 5.3  3.0  280 0     .12  -32 .61   .61   22    .045 0      - -
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 1 .31  .29  10   2.9  .29   0      -32 4.8  2.6  260 0   0   0 97     84     2000   .77 0   1 5.3  3.0  280 0     0     -32 .66   .66   21    .045 .0041 - -
floats-esbmc-regression/Double_div_true-unreach-call.i.p+cfa-reducer.c 2 1.8   1.8   13   20    1.4    0      - - - - 0 14    7.8  670 0   0   2 220     210     2800   .71 0     
floats-esbmc-regression/Float_div_true-unreach-call.i.p+cfa-reducer.c 2 .22  .21  6.5 2.8  .23   0      - - - - 0 8.1  4.5  320 0   0   0 390     380     2800   .71 0     
floats-esbmc-regression/Double_div_bad_false-unreach-call.i.p+cfa-reducer.c 1 5.8   5.8   34   76    5.3    0      -32 21    11    740 0   0   0 98     72     6400   1.8  0   1 32    18    820 0     0     1 1.4    1.4    42    .045 .0041 - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i.p+cfa-reducer.c 1 .51  .49  11   5.7  .64   0      -32 7.6  4.0  320 0   0   0 97     82     3400   .79 0   1 7.4  4.0  330 0     0     1 .67   .67   23    .045 0      - -
float-newlib/double_req_bl_0210_true-unreach-call.c 2 .090 .086 7.9 .77 .0082 0      - - - - 2 18    14    1400 0   0   2 230     210     1400   .71 0     
float-newlib/double_req_bl_0220a_true-unreach-call.c 2 .10  .098 8.3 .93 .0082 0      - - - - 2 20    16    1300 0   0   2 120     99     1200   .71 0     
float-newlib/double_req_bl_0220b_true-unreach-call.c 2 .095 .092 8.2 .71 .0082 0      - - - - 2 19    15    1300 0   0   2 110     96     1200   .68 0     
float-newlib/double_req_bl_0240a_true-unreach-call.c 2 .11  .11  7.8 .74 .0082 0      - - - - 2 18    14    1400 0   0   2 86     69     960   .71 0     
float-newlib/double_req_bl_0240b_true-unreach-call.c 2 .13  .12  7.9 .85 .0082 0      - - - - 2 20    16    1400 0   0   2 77     63     980   .71 0     
float-newlib/double_req_bl_0250a_true-unreach-call.c 2 .063 .061 6.6 .55 .0082 0      - - - - 2 19    17    1300 0   0   2 91     80     2200   .71 0     
float-newlib/double_req_bl_0250b_true-unreach-call.c 2 .084 .079 6.3 .38 .0082 0      - - - - 2 19    17    1300 0   0   2 160     140     2400   .71 0     
float-newlib/double_req_bl_0260_true-unreach-call.c 2 .058 .056 7.1 .56 .0082 0      - - - - 2 24    21    1300 0   0   2 160     150     2500   .71 0     
float-newlib/double_req_bl_0270a_true-unreach-call.c 2 .056 .052 6.2 .58 .0082 0      - - - - 2 20    17    1300 0   0   2 87     78     2200   .68 0     
float-newlib/double_req_bl_0270b_true-unreach-call.c 2 .053 .051 6.5 .52 .0082 0      - - - - 2 22    19    1300 0   0   2 96     87     2200   .71 0     
float-newlib/double_req_bl_0281_true-unreach-call.c 2 1.8   1.8   240   27    .0082 0      - - - - 2 23    20    1300 0   0   2 46     34     1500   .71 0     
float-newlib/double_req_bl_0310_true-unreach-call.c 2 .086 .083 8.1 .85 .0082 0      - - - - 2 20    16    1300 0   0   2 360     340     1500   .68 0     
float-newlib/double_req_bl_0320_true-unreach-call.c 2 9.0   8.9   790   92    .0082 0      - - - - 2 21    16    1500 0   0   2 110     89     1200   .71 0     
float-newlib/double_req_bl_0330a_true-unreach-call.c 2 .086 .083 8.3 .78 .0082 0      - - - - 2 17    14    1300 0   0   2 87     71     940   .68 0     
float-newlib/double_req_bl_0330b_true-unreach-call.c 2 .11  .11  8.0 .80 .0082 0      - - - - 2 22    18    1300 0   0   2 81     66     960   .71 0     
float-newlib/double_req_bl_0460_true-unreach-call.c 2 9.3   9.3   360   100    .0082 0      - - - - 2 23    19    1200 0   0   2 140     130     2500   .71 0     
float-newlib/double_req_bl_0470_true-unreach-call.c 2 .061 .059 6.4 .56 .0082 0      - - - - 2 18    16    1200 0   0   2 160     150     2500   .68 0     
float-newlib/double_req_bl_0480_true-unreach-call.c 2 .073 .069 6.1 .43 .0082 0      - - - - 2 19    16    1200 0   0   2 94     83     2200   .71 0     
float-newlib/double_req_bl_0490a_true-unreach-call.c 2 .066 .063 7.2 .65 .0082 0      - - - - 2 20    17    1200 0   0   2 150     140     2600   .71 0     
float-newlib/double_req_bl_0490b_true-unreach-call.c 2 .062 .058 6.3 .42 .0082 0      - - - - 2 21    18    1200 0   0   2 180     170     2500   .71 0     
float-newlib/double_req_bl_0520_true-unreach-call.c 2 .083 .079 8.8 .90 .0082 0      - - - - 2 30    26    2100 0   0   2 380     360     2600   .71 0     
float-newlib/double_req_bl_0530a_true-unreach-call.c 2 .087 .084 8.2 .90 .0082 0      - - - - 2 27    23    2100 0   0   2 140     120     2100   .71 0     
float-newlib/double_req_bl_0530b_true-unreach-call.c 2 .088 .086 8.0 .78 .0082 0      - - - - 2 30    27    2100 0   0   2 140     120     2100   .71 0     
float-newlib/double_req_bl_0550a_true-unreach-call.c 2 .076 .073 8.4 .82 .0082 0      - - - - 2 32    28    2100 0   0   2 110     95     2200   .68 0     
float-newlib/double_req_bl_0550b_true-unreach-call.c 2 .088 .085 8.2 .78 .0082 0      - - - - 2 26    23    2100 0   0   2 120     97     2200   .71 0     
float-newlib/double_req_bl_0620a_true-unreach-call.c 2 .11  .10  6.2 .32 .0082 0      - - - - 2 13    11    1100 0   0   2 250     240     2100   .71 0     
float-newlib/double_req_bl_0620b_true-unreach-call.c 2 .077 .072 6.1 .32 .0082 0      - - - - 2 16    14    1100 0   0   2 230     220     2100   .68 0     
float-newlib/double_req_bl_0621a_true-unreach-call.c 2 .052 .050 6.9 .49 .0082 0      - - - - 2 12    10    1000 0   0   2 740     720     2400   .71 0     
float-newlib/double_req_bl_0621b_true-unreach-call.c 2 .095 .088 6.1 .27 .0082 0      - - - - 2 14    12    1100 0   0   0 960     940     2000   .72 0     
float-newlib/double_req_bl_0660a_true-unreach-call.c 2 2.8   2.8   210   35    .0082 0      - - - - 2 19    16    1300 0   0   2 99     83     1500   .71 0     
float-newlib/double_req_bl_0660b_true-unreach-call.c 2 3.3   3.3   210   35    .0082 0      - - - - 2 18    15    1300 0   0   2 82     69     1500   .71 0     
float-newlib/double_req_bl_0661a_true-unreach-call.c 2 3.4   3.4   220   43    .0082 0      - - - - 2 17    14    1300 0   0   2 260     250     2400   .71 0     
float-newlib/double_req_bl_0661b_true-unreach-call.c 2 4.6   4.6   220   52    .0082 0      - - - - 2 17    15    1300 0   0   2 280     270     2300   .71 0     
float-newlib/double_req_bl_0662a_true-unreach-call.c 2 .10  .10  8.3 1.2  .0082 0      - - - - 2 17    15    1300 0   0   2 160     140     1600   .68 0     
float-newlib/double_req_bl_0662b_true-unreach-call.c 2 .10  .10  8.4 .91 .0082 0      - - - - 2 19    16    1300 0   0   2 420     400     2400   .68 0     
float-newlib/double_req_bl_0663a_true-unreach-call.c 2 .12  .11  7.9 1.3  .0082 0      - - - - 2 18    15    1300 0   0   2 100     85     1500   .68 0     
float-newlib/double_req_bl_0663b_true-unreach-call.c 2 .11  .10  8.2 .92 .0082 0      - - - - 2 18    15    1300 0   0   2 540     520     2500   .68 0     
float-newlib/double_req_bl_0670_true-unreach-call.c 2 8.1   8.1   360   86    .0082 0      - - - - 2 18    15    1400 0   0   2 190     180     1400   .71 0     
float-newlib/double_req_bl_0680a_true-unreach-call.c 2 .085 .080 6.3 .37 .0082 0      - - - - 2 16    13    1300 0   0   2 94     80     1500   .71 0     
float-newlib/double_req_bl_0680b_true-unreach-call.c 2 .071 .069 6.9 .40 .0082 0      - - - - 2 17    14    1300 0   0   2 79     64     1400   .71 0     
float-newlib/double_req_bl_0681a_true-unreach-call.c 2 .068 .065 6.4 .51 .0082 0      - - - - 2 16    14    1300 0   0   2 120     100     1500   .71 0     
float-newlib/double_req_bl_0681b_true-unreach-call.c 2 .064 .061 6.7 .59 .0082 0      - - - - 2 19    16    1300 0   0   2 94     78     1400   .71 0     
float-newlib/double_req_bl_0682a_true-unreach-call.c 2 2.5   2.5   200   30    .0082 0      - - - - 2 18    15    1200 0   0   2 140     120     1600   .68 0     
float-newlib/double_req_bl_0682b_true-unreach-call.c 2 2.4   2.4   200   34    .0082 0      - - - - 2 16    14    1200 0   0   2 100     85     1500   .68 0     
float-newlib/double_req_bl_0683a_true-unreach-call.c 2 2.5   2.5   200   30    .0082 0      - - - - 2 18    15    1300 0   0   2 100     87     1500   .68 0     
float-newlib/double_req_bl_0683b_true-unreach-call.c 2 2.5   2.5   200   32    .0082 0      - - - - 2 16    14    1300 0   0   2 100     84     1500   .71 0     
float-newlib/double_req_bl_0684a_true-unreach-call.c 2 .13  .13  8.9 1.4  .0082 0      - - - - 2 17    14    1200 0   0   0 960     930     2100   .71 0     
float-newlib/double_req_bl_0684b_true-unreach-call.c 2 .13  .13  9.1 1.4  .0082 0      - - - - 2 15    13    1200 0   0   0 960     930     2000   1.1  0     
float-newlib/double_req_bl_0685a_true-unreach-call.c 2 .059 .057 6.9 .61 .0082 0      - - - - 2 16    13    1300 0   0   2 170     160     2000   .71 0     
float-newlib/double_req_bl_0685b_true-unreach-call.c 2 .071 .068 6.8 .43 .0082 0      - - - - 2 17    14    1300 0   0   2 180     160     2100   .68 0     
float-newlib/double_req_bl_0686a_true-unreach-call.c 2 .080 .077 6.3 .51 .0082 0      - - - - 2 16    14    1300 0   0   2 120     100     1600   .71 0     
float-newlib/double_req_bl_0686b_true-unreach-call.c 2 .060 .057 6.4 .48 .0082 0      - - - - 2 18    15    1200 0   0   2 150     140     2000   .48 0     
float-newlib/double_req_bl_0720_true-unreach-call.c 2 .054 .051 6.3 .51 .0082 0      - - - - 2 6.0  3.3  290 0   0   2 71     59     880   .71 0     
float-newlib/double_req_bl_0730a_true-unreach-call.c 2 .064 .061 6.4 .42 .0082 0      - - - - 2 7.0  4.4  430 0   0   2 58     48     750   .71 0     
float-newlib/double_req_bl_0730b_true-unreach-call.c 2 .055 .052 6.7 .45 .0082 0      - - - - 2 6.4  4.0  400 0   0   2 41     32     820   .68 0     
float-newlib/double_req_bl_0730c_true-unreach-call.c 2 .090 .084 6.2 .47 .0082 0      - - - - 2 6.6  4.0  400 0   0   2 51     39     900   .71 0     
float-newlib/double_req_bl_0740_true-unreach-call.c 2 .068 .064 6.8 .31 .0082 0      - - - - 2 6.9  4.3  430 0   0   2 50     40     690   .71 0     
float-newlib/double_req_bl_0832_true-unreach-call.c 2 2.0   2.0   120   24    .0082 0      - - - - 2 11    8.7  870 0   0   2 160     150     1600   .71 0     
float-newlib/double_req_bl_0833_true-unreach-call.c 2 .056 .055 6.2 .47 .0082 0      - - - - 2 9.9  8.1  840 0   0   2 140     130     1600   .71 0     
float-newlib/double_req_bl_0834_true-unreach-call.c 2 .069 .065 6.6 .35 .0082 0      - - - - 2 10    8.5  800 0   0   2 110     100     1500   .71 0     
float-newlib/double_req_bl_0870b_true-unreach-call.c 2 .12  .11  8.5 1.2  .016  0      - - - - 2 38    34    2600 0   0   2 260     240     2100   .71 0     
float-newlib/double_req_bl_0872a_true-unreach-call.c 2 .14  .13  8.0 .98 .016  0      - - - - 2 34    30    2600 0   0   2 220     200     2800   .71 0     
float-newlib/double_req_bl_0872b_true-unreach-call.c 2 .094 .092 8.4 .91 .016  0      - - - - 2 34    31    2600 0   0   2 640     620     3300   .70 0     
float-newlib/double_req_bl_0873a_true-unreach-call.c 2 .094 .092 9.6 .94 .016  0      - - - - 2 32    28    2600 0   0   2 270     250     2300   .71 0     
float-newlib/double_req_bl_0873b_true-unreach-call.c 2 .093 .090 8.9 .98 .016  0      - - - - 2 38    34    2600 0   0   2 260     240     2300   .71 0     
float-newlib/double_req_bl_0874_true-unreach-call.c 2 .20  .20  11   2.0  .016  0      - - - - 2 34    30    2600 0   0   2 240     230     2200   .71 0     
float-newlib/double_req_bl_0876_true-unreach-call.c 2 .17  .17  12   2.0  .016  0      - - - - 2 31    28    2700 0   0   2 270     250     2200   .71 0     
float-newlib/double_req_bl_0882_true-unreach-call.c 2 .22  .22  14   2.7  .016  0      - - - - 2 34    30    2700 0   0   0 370     350     2700   .71 0     
float-newlib/double_req_bl_0883_true-unreach-call.c 2 .18  .18  15   2.6  .016  0      - - - - 2 36    32    2600 0   0   2 560     540     2600   .71 0     
float-newlib/double_req_bl_0910a_true-unreach-call.c 2 .067 .065 6.7 .43 .0082 0      - - - - 2 15    13    1100 0   0   2 350     340     2000   .71 0     
float-newlib/double_req_bl_0910b_true-unreach-call.c 2 .061 .060 6.7 .44 .0082 0      - - - - 2 14    12    1100 0   0   2 85     74     1500   .71 0     
float-newlib/double_req_bl_0920a_true-unreach-call.c 2 2.8   2.8   200   34    .0082 0      - - - - 2 14    12    1100 0   0   2 110     97     1500   .71 0     
float-newlib/double_req_bl_0920b_true-unreach-call.c 2 .058 .057 6.2 .52 .0082 0      - - - - 2 14    12    1100 0   0   2 100     90     1500   .71 0     
float-newlib/double_req_bl_0921_true-unreach-call.c 2 .068 .065 6.5 .49 .0082 0      - - - - 2 15    13    1100 0   0   2 120     110     1900   .71 0     
float-newlib/double_req_bl_0930_true-unreach-call.c 2 .072 .069 7.0 .51 .0082 0      - - - - 2 12    11    1100 0   0   2 110     100     1700   .71 0     
float-newlib/double_req_bl_0931_true-unreach-call.c 2 .072 .068 6.4 .33 .0082 0      - - - - 2 15    13    1100 0   0   2 84     75     1700   .71 0     
float-newlib/double_req_bl_0960b_true-unreach-call.c 2 .059 .056 6.8 .55 .0082 0      - - - - 2 20    17    1300 0   0   2 79     71     1400   .71 0     
float-newlib/double_req_bl_0970a_true-unreach-call.c 2 3.5   3.5   220   38    .0082 0      - - - - 2 19    17    1300 0   0   2 97     84     1400   .68 0     
float-newlib/double_req_bl_0970b_true-unreach-call.c 2 .062 .059 6.3 .42 .0082 0      - - - - 2 19    16    1300 0   0   2 79     70     1400   .68 0     
float-newlib/double_req_bl_0971_true-unreach-call.c 2 .058 .054 6.5 .45 .0082 0      - - - - 2 19    17    1300 0   0   2 91     80     1400   .71 0     
float-newlib/double_req_bl_0981_true-unreach-call.c 2 .064 .060 6.2 .40 .0082 0      - - - - 2 17    15    1300 0   0   2 87     76     1400   .71 0     
float-newlib/double_req_bl_1011a_true-unreach-call.c 2 .053 .051 8.0 .39 .0082 0      - - - - 2 3.5  2.0  250 0   0   2 26     16     380   .75 0     
float-newlib/double_req_bl_1011b_true-unreach-call.c 2 .067 .063 6.4 .31 .0082 0      - - - - 2 4.0  2.3  250 0   0   2 25     16     380   .75 0     
float-newlib/double_req_bl_1012a_true-unreach-call.c 2 .052 .049 6.8 .36 .0082 0      - - - - 2 3.6  2.0  250 0   0   2 24     15     370   .75 0     
float-newlib/double_req_bl_1012b_true-unreach-call.c 2 .048 .046 7.9 .41 .0082 0      - - - - 2 3.6  2.1  250 0   0   2 24     15     370   .68 0     
float-newlib/double_req_bl_1031_true-unreach-call.c 2 .052 .048 6.7 .46 .0082 0      - - - - 2 4.3  2.5  260 0   0   2 30     21     440   .71 0     
float-newlib/double_req_bl_1032a_true-unreach-call.c 2 .095 .088 6.0 .38 .0082 0      - - - - 2 4.2  2.3  270 0   0   2 27     18     450   .71 0     
float-newlib/double_req_bl_1032b_true-unreach-call.c 2 .084 .079 6.8 .36 .0082 0      - - - - 2 4.0  2.2  260 0   0   2 27     18     460   .71 0     
float-newlib/double_req_bl_1032c_true-unreach-call.c 2 .060 .058 6.7 .39 .0082 0      - - - - 2 4.5  2.6  270 0   0   2 27     18     430   .75 0     
float-newlib/double_req_bl_1032d_true-unreach-call.c 2 .060 .056 6.7 .43 .0082 0      - - - - 2 4.8  2.7  270 0   0   2 27     19     440   .75 0     
float-newlib/double_req_bl_1051_true-unreach-call.c 2 .095 .087 6.5 .27 .0082 0      - - - - 2 4.6  2.6  270 0   0   2 30     23     480   .75 0     
float-newlib/double_req_bl_1052a_true-unreach-call.c 2 .053 .051 7.1 .62 .0082 0      - - - - 2 5.4  3.1  280 0   0   2 31     22     480   .68 0     
float-newlib/double_req_bl_1052b_true-unreach-call.c 2 .10  .098 6.5 .30 .0082 0      - - - - 2 4.3  2.5  270 0   0   2 36     25     500   .71 0     
float-newlib/double_req_bl_1052c_true-unreach-call.c 2 .10  .10  6.1 .39 .0082 0      - - - - 2 5.0  2.9  280 0   0   2 50     39     530   .71 0     
float-newlib/double_req_bl_1052d_true-unreach-call.c 2 .062 .058 6.6 .42 .0082 0      - - - - 2 4.7  2.7  280 0   0   2 29     21     480   .75 0     
float-newlib/double_req_bl_1071_true-unreach-call.c 2 .054 .052 7.2 .41 .0082 0      - - - - 2 3.9  2.2  270 0   0   2 28     18     420   .75 0     
float-newlib/double_req_bl_1072a_true-unreach-call.c 2 .051 .048 7.0 .40 .0082 0      - - - - 2 4.0  2.3  270 0   0   2 26     17     380   .75 0     
float-newlib/double_req_bl_1072b_true-unreach-call.c 2 .065 .061 6.6 .37 .0082 0      - - - - 2 4.4  2.5  270 0   0   2 25     16     450   .75 0     
float-newlib/double_req_bl_1072c_true-unreach-call.c 2 .072 .068 6.5 .33 .0082 0      - - - - 2 4.8  2.7  270 0   0   2 21     14     450   .71 0     
float-newlib/double_req_bl_1072d_true-unreach-call.c 2 .060 .059 6.3 .41 .0082 0      - - - - 2 4.2  2.4  270 0   0   2 25     17     380   .75 0     
float-newlib/double_req_bl_1091_true-unreach-call.c 2 .054 .051 6.7 .42 .0082 0      - - - - 2 4.8  2.8  270 0   0   2 29     21     460   .71 0     
float-newlib/double_req_bl_1092a_true-unreach-call.c 2 .060 .058 7.2 .42 .0082 0      - - - - 2 4.8  2.7  270 0   0   2 32     23     430   .71 0     
float-newlib/double_req_bl_1092b_true-unreach-call.c 2 .053 .051 6.6 .50 .0082 0      - - - - 2 3.9  2.2  270 0   0   2 44     33     500   .75 0     
float-newlib/double_req_bl_1092c_true-unreach-call.c 2 .056 .054 6.6 .45 .0082 0      - - - - 2 4.3  2.5  270 0   0   2 30     22     470   .71 0     
float-newlib/double_req_bl_1092d_true-unreach-call.c 2 .050 .047 6.8 .48 .0082 0      - - - - 2 4.8  2.7  270 0   0   2 35     25     480   .71 0     
float-newlib/double_req_bl_1121a_true-unreach-call.c 2 .12  .11  8.4 1.6  .0082 0      - - - - 2 9.9  6.7  480 0   0   2 96     85     1300   .71 0     
float-newlib/double_req_bl_1121b_true-unreach-call.c 2 .12  .12  8.6 1.2  .0082 0      - - - - 2 11    7.5  480 0   0   2 81     70     1100   .68 0     
float-newlib/double_req_bl_1122a_true-unreach-call.c 2 .092 .088 7.4 .65 .0082 0      - - - - 2 7.2  4.4  480 0   0   2 81     72     1200   .68 0     
float-newlib/double_req_bl_1122b_true-unreach-call.c 2 .083 .080 7.3 .69 .0082 0      - - - - 2 9.4  5.8  480 0   0   2 78     68     1200   .71 0     
float-newlib/double_req_bl_1130a_true-unreach-call.c 2 .37  .37  21   5.4  .0082 0      - - - - 2 8.4  5.2  500 0   0   2 55     43     850   .71 0     
float-newlib/double_req_bl_1131a_true-unreach-call.c 2 .30  .29  18   3.7  .0082 0      - - - - 2 12    7.6  490 0   0   2 52     39     830   .75 0     
float-newlib/double_req_bl_1131b_true-unreach-call.c 2 .31  .30  18   3.9  .0082 0      - - - - 2 8.3  5.2  500 0   0   2 50     38     840   .71 0     
float-newlib/double_req_bl_1211a_true-unreach-call.c 2 .062 .061 6.0 .55 .0082 0      - - - - 2 5.4  3.2  310 0   0   2 50     37     580   .71 0     
float-newlib/double_req_bl_1211b_true-unreach-call.c 2 .062 .059 6.5 .43 .0082 0      - - - - 2 5.7  3.4  320 0   0   2 41     30     570   .71 0     
float-newlib/double_req_bl_1230_true-unreach-call.c 2 .072 .068 6.6 .30 .0082 0      - - - - 2 4.1  2.3  250 0   0   2 27     17     480   .75 0     
float-newlib/double_req_bl_1231b_true-unreach-call.c 2 .063 .061 6.9 .65 .0082 0      - - - - 2 4.6  2.6  250 0   0   2 40     28     600   .75 0     
float-newlib/double_req_bl_1232a_true-unreach-call.c 2 .051 .050 6.8 .46 .0082 0      - - - - 2 5.0  2.8  260 0   0   2 31     21     500   .68 0     
float-newlib/double_req_bl_1250_true-unreach-call.c 2 .053 .049 6.7 .34 .0082 0      - - - - 2 4.0  2.3  250 0   0   2 23     14     470   .75 0     
float-newlib/double_req_bl_1251b_true-unreach-call.c 2 .087 .083 6.5 .44 .0082 0      - - - - 2 3.9  2.2  260 0   0   2 42     30     590   .71 0     
float-newlib/double_req_bl_1252a_true-unreach-call.c 2 .10  .098 6.3 .25 .0082 0      - - - - 2 4.0  2.3  260 0   0   2 34     24     500   .75 0     
float-newlib/double_req_bl_1300_true-unreach-call.c 2 .054 .051 6.6 .46 .0082 0      - - - - 2 3.8  2.1  260 0   0   2 100     90     1100   .71 0     
float-newlib/float_req_bl_0220a_true-unreach-call.c 2 .089 .086 8.5 .86 .0082 0      - - - - 2 8.3  4.5  300 0   0   2 78     63     740   .68 0     
float-newlib/float_req_bl_0220b_true-unreach-call.c 2 .14  .13  7.9 .72 .0082 0      - - - - 2 6.9  3.7  300 0   0   2 91     72     730   .68 0     
float-newlib/float_req_bl_0240a_true-unreach-call.c 2 .078 .076 7.4 .86 .0082 0      - - - - 2 8.1  4.3  280 0   0   2 73     53     680   .71 0     
float-newlib/float_req_bl_0240b_true-unreach-call.c 2 .079 .076 8.7 .86 .0082 0      - - - - 2 6.3  3.4  290 0   0   2 78     58     680   .71 0     
float-newlib/float_req_bl_0250a_true-unreach-call.c 2 .13  .12  6.3 .37 .0082 0      - - - - 2 5.8  3.2  280 0   0   2 58     50     880   .71 0     
float-newlib/float_req_bl_0250b_true-unreach-call.c 2 .056 .053 7.1 .58 .0082 0      - - - - 2 5.7  3.1  280 0   0   2 71     60     860   .68 0     
float-newlib/float_req_bl_0260_true-unreach-call.c 2 .063 .061 6.5 .36 .0082 0      - - - - 2 6.2  3.4  280 0   0   2 62     53     860   .71 0     
float-newlib/float_req_bl_0270a_true-unreach-call.c 2 .051 .048 7.0 .54 .0082 0      - - - - 2 6.5  3.5  280 0   0   2 74     61     930   .71 0     
float-newlib/float_req_bl_0270b_true-unreach-call.c 2 .061 .058 6.9 .62 .0082 0      - - - - 2 6.0  3.3  280 0   0   2 67     56     950   .71 0     
float-newlib/float_req_bl_0281_true-unreach-call.c 2 1.5   1.5   96   16    .0082 0      - - - - 2 13    8.6  530 0   0   2 68     58     990   .71 0     
float-newlib/float_req_bl_0310_true-unreach-call.c 2 .11  .11  7.6 .77 .0082 0      - - - - 2 7.0  3.8  280 0   0   2 380     360     1100   .71 0     
float-newlib/float_req_bl_0320a_true-unreach-call.c 2 .086 .083 8.4 .74 .0082 0      - - - - 2 7.6  4.1  290 0   0   2 79     61     730   .71 0     
float-newlib/float_req_bl_0320b_true-unreach-call.c 2 .086 .084 8.2 .77 .0082 0      - - - - 2 6.7  3.6  310 0   0   2 73     58     750   .68 0     
float-newlib/float_req_bl_0330a_true-unreach-call.c 2 .093 .090 8.7 .75 .0082 0      - - - - 2 7.3  3.9  290 0   0   2 60     45     680   .71 0     
float-newlib/float_req_bl_0330b_true-unreach-call.c 2 .087 .084 8.0 .88 .0082 0      - - - - 2 7.9  4.2  290 0   0   2 68     50     690   .68 0     
float-newlib/float_req_bl_0460_true-unreach-call.c 2 2.2   2.2   120   26    .0082 0      - - - - 2 9.2  6.2  530 0   0   2 75     65     1100   .71 0     
float-newlib/float_req_bl_0470_true-unreach-call.c 2 .059 .056 6.4 .53 .0082 0      - - - - 2 6.1  3.4  280 0   0   2 74     65     970   .68 0     
float-newlib/float_req_bl_0480_true-unreach-call.c 2 .053 .051 7.0 .64 .0082 0      - - - - 2 6.3  3.5  280 0   0   2 67     56     950   .71 0     
float-newlib/float_req_bl_0490a_true-unreach-call.c 2 .055 .052 6.3 .55 .0082 0      - - - - 2 4.9  2.7  280 0   0   2 71     63     970   .68 0     
float-newlib/float_req_bl_0490b_true-unreach-call.c 2 .094 .090 6.1 .62 .0082 0      - - - - 2 5.5  3.0  280 0   0   2 72     63     970   .71 0     
float-newlib/float_req_bl_0530a_true-unreach-call.c 2 .082 .080 8.4 .94 .0082 0      - - - - 2 7.8  4.2  290 0   0   2 83     66     1000   .71 0     
float-newlib/float_req_bl_0530b_true-unreach-call.c 2 .11  .11  8.6 .82 .0082 0      - - - - 2 6.7  3.6  310 0   0   2 85     68     950   .68 0     
float-newlib/float_req_bl_0550a_true-unreach-call.c 2 .087 .084 8.7 .79 .0082 0      - - - - 2 8.1  4.3  290 0   0   2 64     48     990   .71 0     
float-newlib/float_req_bl_0550b_true-unreach-call.c 2 .12  .12  8.0 .73 .0082 0      - - - - 2 6.0  3.2  280 0   0   2 72     54     990   .71 0     
float-newlib/float_req_bl_0610_true-unreach-call.c 2 .064 .059 6.6 .46 .0082 0      - - - - 2 3.9  2.2  250 0   0   2 74     63     790   .71 0     
float-newlib/float_req_bl_0620a_true-unreach-call.c 2 .061 .058 6.4 .40 .0082 0      - - - - 2 4.1  2.2  250 0   0   2 100     90     890   .71 0     
float-newlib/float_req_bl_0620b_true-unreach-call.c 2 .064 .062 6.3 .51 .0082 0      - - - - 2 4.1  2.3  250 0   0   2 100     90     890   .68 0     
float-newlib/float_req_bl_0621a_true-unreach-call.c 2 .060 .058 6.4 .40 .0082 0      - - - - 2 4.3  2.4  260 0   0   0 960     950     1000   .72 0     
float-newlib/float_req_bl_0621b_true-unreach-call.c 2 .076 .071 6.4 .29 .0082 0      - - - - 2 4.4  2.4  260 0   0   0 960     950     1000   .71 0     
float-newlib/float_req_bl_0660a_true-unreach-call.c 2 1.3   1.3   72   16    .0082 0      - - - - 2 7.3  5.2  510 0   0   2 46     35     740   .71 0     
float-newlib/float_req_bl_0660b_true-unreach-call.c 2 1.2   1.2   72   17    .0082 0      - - - - 2 7.4  5.1  510 0   0   2 45     33     730   .75 0     
float-newlib/float_req_bl_0661a_true-unreach-call.c 2 1.0   1.0   73   13    .0082 0      - - - - 2 8.7  6.1  510 0   0   2 98     86     930   .71 0     
float-newlib/float_req_bl_0661b_true-unreach-call.c 2 1.2   1.2   73   14    .0082 0      - - - - 2 10    6.7  520 0   0   2 120     100     940   .71 0     
float-newlib/float_req_bl_0662a_true-unreach-call.c 2 .089 .087 7.0 .91 .0082 0      - - - - 2 5.1  2.9  270 0   0   2 39     30     710   .71 0     
float-newlib/float_req_bl_0662b_true-unreach-call.c 2 .091 .089 6.9 .69 .0082 0      - - - - 2 5.1  2.9  270 0   0   2 51     39     710   .71 0     
float-newlib/float_req_bl_0663a_true-unreach-call.c 2 .081 .079 7.2 .87 .0082 0      - - - - 2 4.6  2.6  270 0   0   2 46     34     710   .71 0     
float-newlib/float_req_bl_0663b_true-unreach-call.c 2 .12  .12  6.9 .87 .0082 0      - - - - 2 4.8  2.7  300 0   0   2 45     32     700   .71 0     
float-newlib/float_req_bl_0670_true-unreach-call.c 2 1.7   1.7   130   20    .0082 0      - - - - 2 7.3  5.1  520 0   0   2 70     58     790   .71 0     
float-newlib/float_req_bl_0680a_true-unreach-call.c 2 .067 .064 6.8 .41 .0082 0      - - - - 2 4.1  2.2  250 0   0   2 47     34     720   .75 0     
float-newlib/float_req_bl_0680b_true-unreach-call.c 2 .065 .062 6.7 .55 .0082 0      - - - - 2 4.4  2.4  250 0   0   2 57     43     720   .71 0     
float-newlib/float_req_bl_0681a_true-unreach-call.c 2 .072 .069 6.3 .92 .0082 0      - - - - 2 5.3  2.9  250 0   0   2 38     28     730   .68 0     
float-newlib/float_req_bl_0681b_true-unreach-call.c 2 .077 .074 6.6 .53 .0082 0      - - - - 2 4.3  2.3  250 0   0   2 53     39     700   .71 0     
float-newlib/float_req_bl_0682a_true-unreach-call.c 2 .91  .90  67   11    .0082 0      - - - - 2 9.2  6.3  550 0   0   2 68     51     800   .71 0     
float-newlib/float_req_bl_0682b_true-unreach-call.c 2 .93  .92  68   11    .0082 0      - - - - 2 7.4  5.3  520 0   0   2 48     37     730   .71 0     
float-newlib/float_req_bl_0683a_true-unreach-call.c 2 .96  .96  68   11    .0082 0      - - - - 2 9.7  6.7  520 0   0   2 51     38     750   .71 0     
float-newlib/float_req_bl_0683b_true-unreach-call.c 2 .94  .94  68   11    .0082 0      - - - - 2 8.4  5.9  520 0   0   2 57     43     750   .68 0     
float-newlib/float_req_bl_0684a_true-unreach-call.c 2 .10  .099 7.3 1.1  .0082 0      - - - - 2 4.8  2.8  290 0   0   0 960     940     1000   .69 0     
float-newlib/float_req_bl_0684b_true-unreach-call.c 2 .11  .10  7.7 1.1  .0082 0      - - - - 2 5.3  3.0  290 0   0   0 960     940     1000   .69 0     
float-newlib/float_req_bl_0685a_true-unreach-call.c 2 .059 .055 7.0 .81 .0082 0      - - - - 2 4.0  2.2  250 0   0   2 53     40     740   .71 0     
float-newlib/float_req_bl_0685b_true-unreach-call.c 2 .064 .061 7.3 .41 .0082 0      - - - - 2 5.0  2.7  260 0   0   2 62     48     760   .71 0     
float-newlib/float_req_bl_0686a_true-unreach-call.c 2 .11  .10  6.3 .36 .0082 0      - - - - 2 5.5  3.0  260 0   0   2 49     36     700   .68 0     
float-newlib/float_req_bl_0686b_true-unreach-call.c 2 .062 .061 6.9 .63 .0082 0      - - - - 2 4.4  2.4  250 0   0   2 52     39     710   .71 0     
float-newlib/float_req_bl_0710_true-unreach-call.c 2 .18  .18  12   2.5  .0082 0      - - - - 2 6.5  3.8  310 0   0   0 300     290     2600   .71 0     
float-newlib/float_req_bl_0720_true-unreach-call.c 2 .054 .052 6.9 .46 .0082 0      - - - - 2 5.4  3.0  280 0   0   2 45     36     530   .71 0     
float-newlib/float_req_bl_0730a_true-unreach-call.c 2 .060 .056 6.9 .37 .0082 0      - - - - 2 5.7  3.1  280 0   0   2 34     26     430   .68 0     
float-newlib/float_req_bl_0730b_true-unreach-call.c 2 .056 .052 6.7 .36 .0082 0      - - - - 2 5.6  3.1  270 0   0   2 24     15     450   .75 0     
float-newlib/float_req_bl_0730c_true-unreach-call.c 2 .049 .047 6.7 .62 .0082 0      - - - - 2 5.9  3.2  280 0   0   2 27     17     440   .75 0     
float-newlib/float_req_bl_0740_true-unreach-call.c 2 .052 .050 6.8 .45 .0082 0      - - - - 2 5.1  2.8  280 0   0   2 35     25     380   .71 0     
float-newlib/float_req_bl_0831_true-unreach-call.c 2 .064 .060 6.9 .41 .0082 0      - - - - 2 4.1  2.3  250 0   0   2 170     160     1600   .71 0     
float-newlib/float_req_bl_0832a_true-unreach-call.c 2 .052 .051 6.4 .53 .0082 0      - - - - 2 4.9  2.7  260 0   0   2 130     120     740   .71 0     
float-newlib/float_req_bl_0832b_true-unreach-call.c 2 .11  .10  6.2 .28 .0082 0      - - - - 2 5.0  2.7  260 0   0   2 120     110     760   .71 0     
float-newlib/float_req_bl_0833_true-unreach-call.c 2 .078 .074 6.3 .33 .0082 0      - - - - 2 4.2  2.3  250 0   0   2 82     72     720   .71 0     
float-newlib/float_req_bl_0834_true-unreach-call.c 2 .064 .061 6.6 .44 .0082 0      - - - - 2 4.7  2.6  250 0   0   2 130     110     780   .71 0     
float-newlib/float_req_bl_0870b_true-unreach-call.c 2 .12  .11  8.7 1.2  .016  0      - - - - 2 8.1  4.3  300 0   0   2 75     60     900   .71 0     
float-newlib/float_req_bl_0872a_true-unreach-call.c 2 .097 .095 8.4 1.0  .016  0      - - - - 2 6.0  3.2  280 0   0   2 59     47     760   .71 0     
float-newlib/float_req_bl_0872b_true-unreach-call.c 2 .10  .10  8.5 1.3  .016  0      - - - - 2 6.1  3.3  290 0   0   2 58     48     910   .70 0     
float-newlib/float_req_bl_0873a_true-unreach-call.c 2 .099 .097 9.2 1.1  .016  0      - - - - 2 5.8  3.2  280 0   0   2 93     77     950   .71 0     
float-newlib/float_req_bl_0873b_true-unreach-call.c 2 .10  .095 9.2 1.1  .016  0      - - - - 2 7.6  4.1  280 0   0   2 84     72     960   .68 0     
float-newlib/float_req_bl_0874_true-unreach-call.c 2 .15  .14  10   2.0  .016  0      - - - - 2 6.4  3.5  290 0   0   2 120     110     1000   .70 0     
float-newlib/float_req_bl_0875_true-unreach-call.c 2 .16  .15  9.6 3.3  .016  0      - - - - 2 7.6  4.1  290 0   0   2 140     120     1100   .71 0     
float-newlib/float_req_bl_0876_true-unreach-call.c 2 .14  .14  9.9 1.6  .016  0      - - - - 2 6.7  3.6  330 0   0   2 140     120     1000   .71 0     
float-newlib/float_req_bl_0877_true-unreach-call.c 2 .19  .18  9.6 1.4  .016  0      - - - - 2 6.5  3.5  300 0   0   2 150     130     1100   .71 0     
float-newlib/float_req_bl_0880_true-unreach-call.c 2 4.7   4.7   50   68    .69   0      - - - - 0 900    890    5400 0   0   2 520     480     1400   .71 0     
float-newlib/float_req_bl_0881_true-unreach-call.c 2 4.8   4.8   50   61    .69   0      - - - - 0 910    880    5200 0   0   2 460     430     1400   .68 0     
float-newlib/float_req_bl_0883_true-unreach-call.c 2 .17  .17  12   2.1  .016  0      - - - - 2 7.2  4.1  350 0   0   2 220     210     1100   .71 0     
float-newlib/float_req_bl_0910a_true-unreach-call.c 2 .054 .052 6.6 .48 .0082 0      - - - - 2 3.9  2.1  250 0   0   2 48     39     590   .68 0     
float-newlib/float_req_bl_0910b_true-unreach-call.c 2 .061 .059 6.2 .43 .0082 0      - - - - 2 4.8  2.6  250 0   0   2 55     45     580   .71 0     
float-newlib/float_req_bl_0920a_true-unreach-call.c 2 1.7   1.7   76   18    .0082 0      - - - - 2 6.7  4.9  480 0   0   2 56     47     650   .71 0     
float-newlib/float_req_bl_0920b_true-unreach-call.c 2 .066 .061 6.7 .43 .0082 0      - - - - 2 4.9  2.7  250 0   0   2 52     44     620   .71 0     
float-newlib/float_req_bl_0921_true-unreach-call.c 2 .064 .061 6.2 .48 .0082 0      - - - - 2 4.3  2.4  250 0   0   2 64     56     740   .71 0     
float-newlib/float_req_bl_0930_true-unreach-call.c 2 .059 .056 6.2 .43 .0082 0      - - - - 2 4.6  2.4  280 0   0   2 240     230     1700   .68 0     
float-newlib/float_req_bl_0931_true-unreach-call.c 2 .11  .11  5.7 .34 .0082 0      - - - - 2 4.2  2.3  250 0   0   2 60     51     720   .71 0     
float-newlib/float_req_bl_0960a_true-unreach-call.c 2 .092 .086 6.2 .40 .0082 0      - - - - 2 4.4  2.4  280 0   0   2 45     35     580   .75 0     
float-newlib/float_req_bl_0960b_true-unreach-call.c 2 .065 .063 6.5 .39 .0082 0      - - - - 2 4.7  2.6  250 0   0   2 44     34     590   .71 0     
float-newlib/float_req_bl_0970a_true-unreach-call.c 2 1.3   1.3   83   13    .0082 0      - - - - 2 8.3  6.0  540 0   0   2 50     39     630   .71 0     
float-newlib/float_req_bl_0970b_true-unreach-call.c 2 .065 .062 6.5 .43 .0082 0      - - - - 2 4.0  2.2  250 0   0   2 42     33     590   .71 0     
float-newlib/float_req_bl_0971_true-unreach-call.c 2 .068 .065 6.4 .49 .0082 0      - - - - 2 5.0  2.7  280 0   0   2 59     48     670   .71 0     
float-newlib/float_req_bl_0981_true-unreach-call.c 2 .062 .060 6.4 .34 .0082 0      - - - - 2 4.2  2.3  250 0   0   2 43     34     660   .71 0     
float-newlib/float_req_bl_1010_true-unreach-call.c 2 .054 .051 6.4 .46 .0082 0      - - - - 2 4.6  2.5  250 0   0   2 21     12     310   .75 0     
float-newlib/float_req_bl_1011a_true-unreach-call.c 2 .050 .047 7.2 .39 .0082 0      - - - - 2 4.0  2.3  250 0   0   2 19     12     370   .75 0     
float-newlib/float_req_bl_1011b_true-unreach-call.c 2 .059 .055 7.4 .31 .0082 0      - - - - 2 3.6  2.0  250 0   0   2 23     14     360   .75 0     
float-newlib/float_req_bl_1012a_true-unreach-call.c 2 .062 .058 6.4 .34 .0082 0      - - - - 2 4.2  2.3  250 0   0   2 23     14     330   .75 0     
float-newlib/float_req_bl_1012b_true-unreach-call.c 2 .053 .050 6.9 .33 .0082 0      - - - - 2 3.5  2.0  250 0   0   2 20     12     330   .68 0     
float-newlib/float_req_bl_1031_true-unreach-call.c 2 .049 .046 7.1 .36 .0082 0      - - - - 2 3.6  1.9  260 0   0   2 21     12     360   .75 0     
float-newlib/float_req_bl_1032a_true-unreach-call.c 2 .096 .090 5.9 .27 .0082 0      - - - - 2 4.2  2.3  250 0   0   2 20     12     450   .68 0     
float-newlib/float_req_bl_1032b_true-unreach-call.c 2 .056 .054 7.6 .47 .0082 0      - - - - 2 3.8  2.1  250 0   0   2 23     14     440   .75 0     
float-newlib/float_req_bl_1032c_true-unreach-call.c 2 .050 .047 6.6 .41 .0082 0      - - - - 2 4.0  2.2  250 0   0   2 19     12     350   .75 0     
float-newlib/float_req_bl_1032d_true-unreach-call.c 2 .054 .050 6.8 .33 .0082 0      - - - - 2 4.5  2.5  250 0   0   2 23     14     360   .75 0     
float-newlib/float_req_bl_1051_true-unreach-call.c 2 .054 .052 6.4 .42 .0082 0      - - - - 2 3.9  2.2  250 0   0   2 23     15     380   .71 0     
float-newlib/float_req_bl_1052a_true-unreach-call.c 2 .10  .099 6.2 .36 .0082 0      - - - - 2 4.4  2.5  250 0   0   2 25     16     390   .75 0     
float-newlib/float_req_bl_1052b_true-unreach-call.c 2 .050 .049 6.8 .49 .0082 0      - - - - 2 3.6  2.0  250 0   0   2 26     17     390   .75 0     
float-newlib/float_req_bl_1052c_true-unreach-call.c 2 .052 .049 7.0 .54 .0082 0      - - - - 2 4.7  2.6  250 0   0   2 28     19     480   .75 0     
float-newlib/float_req_bl_1052d_true-unreach-call.c 2 .085 .080 6.3 .36 .0082 0      - - - - 2 3.7  2.0  250 0   0   2 26     17     440   .75 0     
float-newlib/float_req_bl_1071_true-unreach-call.c 2 .088 .083 6.0 .29 .0082 0      - - - - 2 4.3  2.3  250 0   0   2 18     10     330   .75 0     
float-newlib/float_req_bl_1072a_true-unreach-call.c 2 .044 .043 6.7 .40 .0082 0      - - - - 2 3.9  2.2  250 0   0   2 18     11     360   .75 0     
float-newlib/float_req_bl_1072b_true-unreach-call.c 2 .054 .050 6.5 .32 .0082 0      - - - - 2 4.6  2.5  250 0   0   2 18     10     350   .75 0     
float-newlib/float_req_bl_1072c_true-unreach-call.c 2 .050 .049 6.6 .48 .0082 0      - - - - 2 3.6  2.0  250 0   0   2 26     16     410   .75 0     
float-newlib/float_req_bl_1072d_true-unreach-call.c 2 .063 .060 6.3 .47 .0082 0      - - - - 2 4.6  2.6  250 0   0   2 22     13     430   .75 0     
float-newlib/float_req_bl_1091_true-unreach-call.c 2 .094 .087 5.9 .38 .0082 0      - - - - 2 3.7  2.1  250 0   0   2 20     13     370   .68 0     
float-newlib/float_req_bl_1092a_true-unreach-call.c 2 .053 .051 6.4 .39 .0082 0      - - - - 2 4.5  2.5  250 0   0   2 25     17     430   .75 0     
float-newlib/float_req_bl_1092b_true-unreach-call.c 2 .053 .051 7.0 .63 .0082 0      - - - - 2 4.7  2.6  250 0   0   2 30     20     480   .75 0     
float-newlib/float_req_bl_1092c_true-unreach-call.c 2 .054 .052 7.4 .38 .0082 0      - - - - 2 4.8  2.7  250 0   0   2 25     16     400   .75 0     
float-newlib/float_req_bl_1092d_true-unreach-call.c 2 .062 .060 6.7 .34 .0082 0      - - - - 2 3.7  2.1  250 0   0   2 23     15     400   .71 0     
float-newlib/float_req_bl_1121a_true-unreach-call.c 2 .11  .11  6.4 .52 .0082 0      - - - - 2 6.3  3.4  280 0   0   2 63     55     570   .71 0     
float-newlib/float_req_bl_1121b_true-unreach-call.c 2 .076 .075 7.1 .67 .0082 0      - - - - 2 6.1  3.3  280 0   0   2 74     64     580   .68 0     
float-newlib/float_req_bl_1122a_true-unreach-call.c 2 .066 .063 6.4 .61 .0082 0      - - - - 2 5.6  3.1  320 0   0   2 65     57     580   .71 0     
float-newlib/float_req_bl_1122b_true-unreach-call.c 2 .066 .063 6.4 .58 .0082 0      - - - - 2 5.4  3.1  320 0   0   2 67     58     580   .68 0     
float-newlib/float_req_bl_1130a_true-unreach-call.c 2 .22  .21  11   2.0  .0082 0      - - - - 2 6.5  3.6  330 0   0   2 23     14     510   .71 0     
float-newlib/float_req_bl_1130b_true-unreach-call.c 2 .18  .17  11   2.2  .0082 0      - - - - 2 6.7  3.8  330 0   0   2 32     20     500   .75 0     
float-newlib/float_req_bl_1131a_true-unreach-call.c 2 .16  .15  11   1.4  .0082 0      - - - - 2 7.1  4.0  330 0   0   2 25     16     520   .68 0     
float-newlib/float_req_bl_1131b_true-unreach-call.c 2 .19  .18  10   1.4  .0082 0      - - - - 2 6.3  3.6  320 0   0   2 28     19     510   .71 0     
float-newlib/float_req_bl_1211a_true-unreach-call.c 2 .083 .074 6.2 .46 .0082 0      - - - - 2 5.0  2.8  250 0   0   2 23     15     470   .75 0     
float-newlib/float_req_bl_1211b_true-unreach-call.c 2 .060 .057 6.3 .35 .0082 0      - - - - 2 4.7  2.6  250 0   0   2 21     13     470   .75 0     
float-newlib/float_req_bl_1230_true-unreach-call.c 2 .052 .049 6.4 .44 .0082 0      - - - - 2 3.6  2.0  250 0   0   2 26     15     460   .75 0     
float-newlib/float_req_bl_1231_true-unreach-call.c 2 .078 .076 7.3 .98 .0082 0      - - - - 2 4.1  2.3  260 0   0   2 60     43     740   .71 0     
float-newlib/float_req_bl_1232a_true-unreach-call.c 2 .058 .054 6.7 .36 .0082 0      - - - - 2 4.5  2.5  250 0   0   2 26     16     430   .75 0     
float-newlib/float_req_bl_1250_true-unreach-call.c 2 .055 .051 6.5 .39 .0082 0      - - - - 2 4.4  2.5  250 0   0   2 22     13     460   .71 0     
float-newlib/float_req_bl_1251_true-unreach-call.c 2 .085 .082 6.5 .76 .0082 0      - - - - 2 4.4  2.5  260 0   0   2 57     41     720   .71 0     
float-newlib/float_req_bl_1252a_true-unreach-call.c 2 .060 .057 6.7 .38 .0082 0      - - - - 2 3.8  2.2  250 0   0   2 24     14     430   .75 0     
float-newlib/float_req_bl_1270a_true-unreach-call.c 2 .58  .58  45   9.2  .0082 0      - - - - 2 10    6.4  450 0   0   2 130     110     730   .71 0     
float-newlib/float_req_bl_1270b_true-unreach-call.c 2 .59  .59  44   7.9  .0082 0      - - - - 2 11    6.8  440 0   0   2 150     130     760   .71 0     
float-newlib/float_req_bl_1270c_true-unreach-call.c 2 .59  .59  44   7.9  .0082 0      - - - - 2 11    6.9  440 0   0   2 320     300     800   .71 0     
float-newlib/float_req_bl_1270d_true-unreach-call.c 2 .61  .60  44   7.0  .0082 0      - - - - 2 11    6.7  450 0   0   2 270     250     810   .68 0     
float-newlib/float_req_bl_1271a_true-unreach-call.c 2 .59  .58  44   6.9  .0082 0      - - - - 2 9.5  6.2  450 0   0   2 290     270     860   .71 0     
float-newlib/float_req_bl_1271b_true-unreach-call.c 2 .59  .58  44   7.0  .0082 0      - - - - 2 9.3  6.0  460 0   0   2 340     330     870   .71 0     
float-newlib/float_req_bl_1381_true-unreach-call.c 2 .057 .054 6.6 .37 .0082 0      - - - - 2 3.6  2.1  260 0   0   2 20     12     310   .75 0     
float-newlib/double_req_bl_0870a_false-unreach-call.c 1 .12  .11  9.8 1.1  .012  0      0 5.4  2.9  260 0   0   0 60     53     1400   .71 0   1 4.9  2.7  270 0     .17  1 .68   .69   20    .13  0      - -
float-newlib/double_req_bl_1210_false-unreach-call.c 1 .070 .060 9.9 .75 .0082 0      0 5.0  2.8  250 0   0   0 14     8.3   300   .75 0   1 4.1  2.4  250 0     .20  1 .61   .61   20    .066 0      - -
float-newlib/double_req_bl_1232b_false-unreach-call.c 1 .080 .067 9.0 .45 .0082 0      1 5.2  2.9  260 0   0   0 13     8.1   300   .71 0   1 3.9  2.3  250 0     0     1 .60   .60   20    .066 0      - -
float-newlib/double_req_bl_1252b_false-unreach-call.c 1 .082 .071 9.4 .54 .0082 0      1 5.8  3.2  250 0   0   0 14     8.1   300   .71 0   1 4.0  2.3  250 0     0     1 .60   .60   20    .066 0      - -
float-newlib/float_req_bl_0870a_false-unreach-call.c 1 .16  .15  9.5 1.0  .012  0      -32 6.8  3.6  280 0   0   0 37     29     600   .70 0   1 4.9  2.8  260 0     .42  1 .69   .70   20    .14  .016  - -
float-newlib/float_req_bl_1210_false-unreach-call.c 1 .063 .057 8.8 1.4  .0082 0      -32 5.1  2.8  250 0   0   0 17     9.8   310   .68 0   1 4.1  2.4  250 0     0     1 .59   .59   20    .061 .0041 - -
float-newlib/float_req_bl_1232b_false-unreach-call.c 1 .16  .14  9.5 .48 .0082 0      1 4.7  2.6  250 0   0   0 15     8.2   310   .75 0   1 4.0  2.3  250 0     0     1 .61   .61   20    .061 0      - -
float-newlib/float_req_bl_1252b_false-unreach-call.c 1 .061 .070 9.2 1.3  .0082 0      1 5.5  3.0  250 0   0   0 15     9.0   300   .68 0   1 4.0  2.3  250 0     .11  1 .59   .59   20    .061 0      - -
loop-floats-scientific-comp/loop1_true-unreach-call.c.i 0 880     880     560   8000    .23   0      - - - - 0 .71 .44 42 0   0   0 .026 .028 5.6 0    0     
loop-floats-scientific-comp/loop2_true-unreach-call.c.i 0 870     880     570   6800    .11   0      - - - - 0 .75 .45 40 0   0   0 .020 .020 5.6 0    0     
loop-floats-scientific-comp/loop3_true-unreach-call.c.i 0 880     880     520   7800    .23   0      - - - - 0 .59 .36 41 0   0   0 .020 .020 5.6 0    0     
loop-floats-scientific-comp/loop5_true-unreach-call.c.i 0 880     880     2100   6300    .55   0      - - - - 0 .73 .44 41 0   0   0 .028 .029 5.7 0    0     
loop-floats-scientific-comp/loop1_false-unreach-call.c.i 1 .12  .11  13   1.6  .0082 0      -32 4.6  2.5  250 0   0   1 17     11     400   .71 0   1 3.9  2.2  250 0     0     1 .58   .58   20    .053 0      - -
loop-floats-scientific-comp/loop2_false-unreach-call.c.i 1 .20  .19  20   2.4  .0082 0      -32 4.5  2.5  250 0   0   1 46     38     630   .71 0   1 3.9  2.3  250 0     .13  1 .59   .59   21    .057 0      - -
loop-floats-scientific-comp/loop4_false-unreach-call.c.i 0 .37  .36  26   4.5  .012  0      -32 4.8  2.6  260 0   0   0 12     7.3   280   .75 0   0 4.5  130    250 .037 .078 0 .67   .67   20    .057 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 800 44000   44000   180000 410000 760     4.4 45 -718 350 240 13000 0   0   45 17 2300 2000 50000 35 0   45 -27 230   250   12000 .037 1.5 45 -93 27   28   930 2.4  .29   424 670 26000 24000 230000 0   0   424 618 68000 64000 370000 270 .0082
    correct results 420 800 6100   6100   18000 63000 450     4.4 18 18 200 160 5300 0   0   17 17 550 440 9000 12 0   37 37 200   120   10000 0     1.4 35 35 23   23   760 2.1  .29   335 670 7200 6400 190000 0   0   309 618 29000 25000 290000 220 0     
        correct true 380 760 5200   5200   16000 54000 440     4.4 0 0 0 0 335 670 7200 6400 190000 0   0   309 618 29000 25000 290000 220 0     
        correct false 40 40 850   850   2200 8800 11     0   18 18 200 160 5300 0   0   17 17 550 440 9000 12 0   37 37 200   120   10000 0     1.4 35 35 23   23   760 2.1  .29   0 0
    correct-unconfimed results 3 0 3.7 3.6 73 44 .029 0   0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 3 0 3.7 3.6 73 44 .029 0   0 0 0 0 0 0
    incorrect results 0 23 -736 150 80 6900 0   0   0 2 -64 7.4 4.3 490 0     0   4 -128 2.4 2.4 83 .19 .0041 0 0
        incorrect true 0 23 -736 150 80 6900 0   0   0 2 -64 7.4 4.3 490 0     0   4 -128 2.4 2.4 83 .19 .0041 0 0
        incorrect false 0 0 0 0 0 0 0
score (469 tasks, max score: 893) 800 -718 17 -27 -93 670 618
Run set cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats