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