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