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