Tool CBMC CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 07:35:27 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i 1 14     14     60   150    .0082 0      1 46    44    350 0   0   1 36     30     680   .71 0   1 3.7  2.2  250 0     .11  1 .58   .58   20    .053 0      - -
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i 1 6.6   6.6   47   72    .0082 0      1 12    10    350 0   0   0 97     90     700   .75 0   1 3.6  2.1  250 0     0     1 .62   .63   20    .053 .0082 - -
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i 1 4.3   4.3   42   44    .0082 0      1 39    37    350 0   0   1 77     71     690   .68 0   1 3.6  2.1  250 0     0     1 .60   .60   20    .053 .070  - -
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i 1 8.4   8.4   49   87    .0082 0      1 13    11    350 0   0   0 97     91     700   .76 0   1 3.6  2.1  250 0     .057 1 .58   .58   20    .053 0      - -
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i 1 7.4   7.4   49   95    .0082 0      1 11    8.9  350 0   0   1 30     25     680   .68 0   1 3.6  2.1  250 0     0     1 .60   .60   20    .053 0      - -
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i 1 77     77     160   660    .0082 0      -32 4.7  2.6  250 0   0   0 97     91     800   .78 0   1 4.2  2.4  250 0     0     1 .57   .57   20    .053 0      - -
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i 1 120     120     230   1200    .0082 0      -32 5.1  2.8  250 0   0   0 97     91     810   .92 0   1 3.7  2.2  240 0     0     1 .59   .59   20    .053 0      - -
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i 1 25     25     100   310    .0082 0      -32 4.7  2.6  250 0   0   1 39     33     820   .71 0   1 3.7  2.2  250 0     0     1 .58   .58   20    .053 .0041 - -
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i 1 430     430     480   4500    .0082 0      -32 4.7  2.6  250 0   0   0 97     90     880   .73 0   1 3.9  2.2  240 0     0     1 .60   .60   20    .053 0      - -
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i 1 75     75     200   830    .0082 0      -32 4.3  2.4  250 0   0   1 52     46     920   .68 0   1 3.7  2.2  250 0     0     1 .58   .58   20    .053 0      - -
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i 1 55     55     180   540    .0082 0      -32 4.3  2.4  250 0   0   0 97     91     920   .82 0   1 3.8  2.2  250 0     0     1 .58   .59   20    .053 0      - -
floats-cdfpl/sine_1_false-unreach-call_true-termination.i 1 .90  .89  22   10    .0082 0      1 12    9.5  300 0   0   0 97     91     610   1.6  0   1 3.6  2.1  250 0     0     1 .57   .57   20    .049 0      - -
floats-cdfpl/sine_2_false-unreach-call_true-termination.i 1 4.1   4.1   31   58    .0082 0      -32 4.3  2.3  250 0   0   0 97     91     570   .73 0   1 3.9  2.3  250 0     0     1 .57   .57   20    .049 .0041 - -
floats-cdfpl/sine_3_false-unreach-call_true-termination.i 1 .98  .97  21   13    .0082 0      -32 4.6  2.5  250 0   0   0 97     91     600   1.6  0   1 3.8  2.2  250 0     .11  1 .57   .57   20    .049 0      - -
floats-cdfpl/square_1_false-unreach-call_true-termination.i 1 1.7   1.7   24   21    .0082 0      -32 4.1  2.3  250 0   0   1 84     78     430   .68 0   1 3.4  2.0  240 0     0     1 .57   .57   20    .049 0      - -
floats-cdfpl/square_2_false-unreach-call_true-termination.i 0 1.8   1.7   24   21    .0082 0      -32 4.2  2.3  250 0   0   0 97     92     450   .69 0   -32 3.7  2.1  250 0     0     -32 .58   .58   20    .049 0      - -
floats-cdfpl/square_3_false-unreach-call_true-termination.i 0 1.5   1.5   23   19    .0082 0      -32 4.5  2.5  250 0   0   0 97     91     460   .72 0   -32 3.8  2.2  250 0     0     -32 .57   .58   20    .049 0      - -
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i 2 230     230     150   2200    .0082 0      - - - - 0 900    900    580 0   0   0 960     950     970   .72 0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i 2 140     140     110   1100    .0082 0      - - - - 0 900    900    590 0   0   0 960     950     790   .72 0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i 2 170     170     110   1600    .0082 0      - - - - 0 900    900    580 0   0   0 960     950     970   1.3  0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i 2 260     260     210   3100    .0082 0      - - - - 0 900    900    520 0   0   0 960     950     890   .72 0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i 2 550     550     310   4600    .0082 0      - - - - 0 900    900    830 0   0   0 960     950     970   .71 0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i 2 350     350     340   2900    .0082 0      - - - - 0 900    900    520 0   0   0 960     950     1000   .69 0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i 2 550     550     360   4800    .0082 0      - - - - 0 900    900    560 0   0   0 960     950     1000   .72 0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i 2 830     830     590   8000    .0082 0      - - - - 0 900    900    540 0   0   0 960     950     890   .72 0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i 0 870     880     550   9600    .057  0      - - - - 0 .63 .39 41 0   0   0 .021 .021 5.5 0    0     
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i 0 880     880     480   6000    .057  0      - - - - 0 .63 .38 40 0   0   0 .030 .031 5.8 0    0     
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i 0 880     880     550   7900    .057  0      - - - - 0 .71 .43 41 0   0   0 .029 .030 5.6 0    0     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i 0 880     880     540   8500    .053  0      - - - - 0 .76 .46 42 0   0   0 .028 .029 5.5 0    0     
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i 0 880     880     850   8200    .057  0      - - - - 0 .66 .41 40 0   0   0 .027 .028 5.6 0    0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i 2 710     710     85   8100    .0082 0      - - - - 0 900    900    500 0   0   0 960     950     790   1.3  0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i 2 220     220     77   3100    .0082 .13   - - - - 0 900    900    490 0   0   0 960     950     830   .72 0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i 2 19     19     44   280    .0082 0      - - - - 0 900    900    650 0   0   0 960     950     830   .71 0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i 2 5.9   5.9   29   81    .0082 0      - - - - 2 710    710    590 0   0   0 960     950     840   .72 0     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i 2 62     62     60   680    .0082 0      - - - - 2 550    540    540 0   0   0 960     950     810   .69 0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i 2 270     270     110   3600    .0082 0      - - - - 2 570    570    570 0   0   0 960     950     670   .72 0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i 2 260     260     110   3100    .0082 0      - - - - 2 400    390    510 0   0   0 960     950     760   .73 0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i 2 93     93     62   1200    .0082 0      - - - - 2 270    270    500 0   0   0 960     950     770   1.3  0     
floats-cdfpl/square_7_true-unreach-call_true-termination.i 2 66     66     56   860    .0082 0      - - - - 0 900    900    480 0   0   2 610     610     790   .71 0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i 2 1.8   1.8   21   26    .0082 0      - - - - 2 72    70    360 0   0   2 80     75     610   .71 0     
floats-cbmc-regression/float-div1_true-unreach-call.i 2 .34  .34  15   5.2  .016  .34   - - - - 2 5.5  3.4  320 0   0   2 46     39     950   .71 0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 2 .29  .29  24   3.1  .016  .39   - - - - 2 13    10    780 0   0   0 14     8.3   290   .75 0     
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i 2 .043 .040 7.3 .33 .0082 0      - - - - 2 3.6  2.0  250 0   0   2 15     8.6   300   .71 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 2 1.7   1.7   10   19    .016  0      - - - - 2 20    17    300 0   0   2 55     46     550   .71 0     
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i 2 .050 .049 7.7 .39 .0082 0      - - - - 2 3.5  1.9  250 0   0   2 12     7.3   300   .75 0     
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 2 .17  .17  9.3 2.6  .016  .090  - - - - 2 5.6  3.0  290 0   0   2 20     12     450   .64 0     
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i 2 .043 .041 6.6 .40 .0082 0      - - - - 2 4.4  2.4  250 0   0   2 17     11     300   .75 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i 2 .11  .10  5.6 .24 .0082 0      - - - - 2 3.9  2.2  250 0   0   2 15     8.4   300   .75 0     
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 .079 .077 8.0 .80 .016  0      - - - - 2 5.8  3.2  260 0   0   0 15     8.0   290   .75 0     
floats-cbmc-regression/float-rounding1_true-unreach-call.i 2 .087 .085 7.2 .78 .016  0      - - - - 0 5.6  3.1  260 0   0   0 8.0   4.6   280   .66 0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i 2 .14  .14  6.8 1.2  .016  0      - - - - 2 5.3  2.9  270 0   0   2 37     29     450   .68 0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i 2 .049 .046 6.2 .25 .0082 0      - - - - 2 3.7  2.0  250 0   0   2 15     8.5   300   .71 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i 2 .052 .049 6.5 .31 .0082 0      - - - - 2 4.4  2.4  250 0   0   2 17     9.8   310   .75 0     
floats-cbmc-regression/float11_true-unreach-call_true-termination.i 2 .047 .045 6.6 .37 .0082 0      - - - - 2 3.8  2.1  250 0   0   2 16     9.2   300   .71 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i 2 .085 .082 6.4 .76 .0082 0      - - - - 2 3.7  2.1  250 0   0   2 23     17     300   .75 0     
floats-cbmc-regression/float13_true-unreach-call_true-termination.i 2 .054 .052 6.4 .32 .0082 0      - - - - 2 4.4  2.5  250 0   0   2 16     9.4   310   .75 0     
floats-cbmc-regression/float14_true-unreach-call.i 2 .11  .10  7.7 .84 .016  0      - - - - 2 5.6  3.1  260 0   0   2 18     10     390   .75 0     
floats-cbmc-regression/float18_true-unreach-call.i 2 .19  .19  7.8 2.3  .078  0      - - - - 0 6.1  3.3  300 0   0   0 16     9.2   290   .75 0     
floats-cbmc-regression/float19_true-unreach-call.i 2 .097 .094 7.1 .72 .016  0      - - - - 2 6.0  3.2  260 0   0   2 18     10     390   .75 0     
floats-cbmc-regression/float1_true-unreach-call_true-termination.i 2 .078 .074 6.1 .22 .0082 .049  - - - - 2 3.7  2.1  250 0   0   2 16     9.4   300   .75 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i 2 .095 .092 7.9 .85 .0082 0      - - - - 2 3.4  1.9  250 0   0   2 22     15     370   .75 0     
floats-cbmc-regression/float21_true-unreach-call.i 2 .21  .21  8.4 2.6  .016  .11   - - - - 2 8.9  6.7  290 0   0   2 86     75     580   .71 0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i 2 .060 .058 6.4 .55 .0082 0      - - - - 2 4.2  2.4  270 0   0   2 220     200     740   .71 0     
floats-cbmc-regression/float2_true-unreach-call_true-termination.i 2 .072 .067 5.9 .27 .0082 0      - - - - 2 3.5  2.0  250 0   0   2 16     9.6   310   .75 0     
floats-cbmc-regression/float3_true-unreach-call_true-termination.i 2 .078 .076 7.2 .76 .0082 0      - - - - 2 4.4  2.5  270 0   0   2 20     13     320   .71 0     
floats-cbmc-regression/float4_true-unreach-call.i 2 9.7   9.7   25   130    .016  0      - - - - 2 74    72    330 0   0   2 92     84     590   .68 0     
floats-cbmc-regression/float5_true-unreach-call_true-termination.i 2 .075 .073 6.3 .60 .0082 0      - - - - 2 3.5  2.0  260 0   0   2 32     26     290   .75 0     
floats-cbmc-regression/float6_true-unreach-call_true-termination.i 2 .069 .067 5.9 .49 .0082 0      - - - - 2 4.2  2.3  250 0   0   2 15     8.8   310   .75 0     
floats-cbmc-regression/float8_true-unreach-call.i 2 .63  .63  7.7 8.6  .016  0      - - - - 2 7.6  5.6  270 0   0   2 16     9.8   390   .71 0     
floats-cbmc-regression/float_lib1_true-unreach-call.i 2 .14  .14  8.6 1.8  .016  0      - - - - 2 5.9  3.1  260 0   0   0 14     8.1   280   .75 0     
floats-cbmc-regression/float_lib2_true-unreach-call.i 2 .13  .12  8.3 1.1  .016  .090  - - - - 2 5.1  2.8  260 0   0   2 17     10     420   .71 0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c 1 .068 .061 9.2 .61 .0082 0      1 4.1  2.3  260 0   0   1 18     11     310   .75 0   0 3.7  2.1  250 0     0     0 .58   .61   20    .037 0      - -
float-benchs/cast_union_loose_false-unreach-call_true-termination.c 1 .083 .071 9.5 .57 .0082 0      1 4.2  2.4  270 0   0   1 14     8.6   310   .75 0   1 4.0  2.3  240 0     0     1 .59   .59   20    .057 0      - -
float-benchs/cast_union_tight_false-unreach-call_true-termination.c 1 .085 .075 9.6 .68 .0082 0      1 5.0  2.9  270 0   0   1 17     9.8   320   .71 0   1 3.8  2.2  250 0     0     1 .61   .62   20    .057 0      - -
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c 1 .091 .081 9.0 .89 .0082 0      1 4.7  2.6  260 0   0   1 16     9.6   310   .75 0   1 3.7  2.1  240 0     0     1 .59   .59   20    .053 0      - -
float-benchs/inv_Newton_false-unreach-call.c 0 880     880     780   5900    .074  0      0 .58 .36 41 0   0   0 .028 .030 5.7 0    0   0 .95 .65 47 0     0     0 .0018 .0022 .52 0     0      - -
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c 0 880     880     12000   4900    15      0      0 .66 .39 42 0   0   0 .026 .027 5.6 0    0   0 1.0  .69 48 0     0     0 .0051 .0061 .54 0     0      - -
float-benchs/inv_square_false-unreach-call_true-termination.c 1 .073 .065 9.7 .70 .0082 0      1 4.8  2.7  260 0   0   1 14     8.3   300   .75 0   1 3.7  2.2  250 0     0     1 .60   .61   20    .053 0      - -
float-benchs/nan_double_false-unreach-call_true-termination.c 1 .071 .059 9.0 .40 .0082 0      1 4.7  2.6  260 0   0   1 13     7.8   300   .71 0   0 3.6  2.1  250 0     0     0 .56   .56   20    .037 0      - -
float-benchs/nan_float_false-unreach-call_true-termination.c 1 .054 .044 9.3 .69 .0082 0      1 4.9  2.7  260 0   0   1 12     7.0   300   .75 0   0 3.7  2.2  250 0     0     0 .56   .55   20    .037 0      - -
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c 1 2.6   2.6   190   29    .0082 0      1 8.9  6.1  380 0   0   1 34     25     1000   .68 0   1 4.5  2.6  260 0     0     1 .62   .62   20    .086 0      - -
float-benchs/sqrt_poly2_false-unreach-call.c 1 .53  .52  35   5.9  .0082 0      -32 5.6  3.1  260 0   0   1 26     19     610   .75 0   1 4.4  2.4  270 0     0     1 .60   .60   20    .061 .17   - -
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c 2 .34  .33  7.0 3.0  .35   0      - - - - 0 10    6.5  520 0   0   0 960     900     2500   1.3  0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c 2 .31  .30  6.5 3.4  .35   0      - - - - 0 10    6.6  520 0   0   0 960     890     4400   .68 0     
float-benchs/Rump_double_true-unreach-call_true-termination.c 2 .049 .046 6.9 .39 .0082 0      - - - - 2 4.4  2.5  250 0   0   2 29     23     990   .71 0     
float-benchs/Rump_float_true-unreach-call_true-termination.c 2 .056 .054 7.1 .31 .0082 0      - - - - 2 4.4  2.5  250 0   0   2 19     12     430   .75 0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c 2 .051 .049 7.0 .46 .0082 0      - - - - 2 4.8  2.7  250 0   0   2 14     8.4   290   .71 0     
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c 2 .050 .048 7.0 .32 .0082 0      - - - - 2 4.2  2.3  250 0   0   2 15     8.7   300   .75 0     
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c 2 .049 .046 7.4 .41 .0082 0      - - - - 2 3.5  1.9  250 0   0   2 15     8.9   300   .71 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c 2 97     97     300   1100    .0082 0      - - - - 2 32    30    500 0   0   0 150     140     2600   .71 0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c 0 880     880     1400   9900    .77   0      - - - - 0 .72 .45 41 0   0   0 .027 .027 5.6 0    0     
float-benchs/cast_float_union_true-unreach-call.c 2 .13  .12  5.7 .29 .0082 0      - - - - 2 3.5  2.0  250 0   0   2 7.2   4.1   300   .62 0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c 2 48     48     96   360    .0082 0      - - - - 0 900    900    1300 0   0   0 960     950     3000   .71 0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c 0 880     880     3100   5900    5.1    0      - - - - 0 .75 .45 40 0   0   0 .025 .027 5.6 0    0     
float-benchs/divmul_diverge_true-unreach-call_true-termination.c 0 880     880     6200   6900    7.7    0      - - - - 0 .63 .39 41 0   0   0 .028 .028 5.6 0    0     
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c 2 .095 .089 7.1 .71 .037  0      - - - - 0 5.2  2.9  290 0   0   2 380     370     660   .71 0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c 2 .080 .077 7.2 .56 .037  0      - - - - 0 5.0  2.8  290 0   0   2 290     280     610   .68 0     
float-benchs/exp_loop_true-unreach-call.c 2 1.0   1.0   20   15    .46   0      - - - - 0 9.2  5.5  440 0   0   0 960     950     1200   .72 0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c 0 880     880     1800   9100    .75   0      - - - - 0 .71 .44 41 0   0   0 .024 .024 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c 0 880     880     2500   9400    13      0      - - - - 0 .73 .45 40 0   0   0 .026 .027 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c 0 880     880     2800   8700    41      0      - - - - 0 .69 .42 40 0   0   0 .022 .030 5.7 0    0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c 0 880     880     2800   11000    41      0      - - - - 0 .76 .46 41 0   0   0 .027 .028 5.6 0    0     
float-benchs/filter1_true-unreach-call_true-termination.c 0 880     880     1600   9500    .40   0      - - - - 0 .71 .43 41 0   0   0 .025 .025 5.6 0    0     
float-benchs/filter2_alt_true-unreach-call.c 0 880     880     340   9600    .074  0      - - - - 0 .59 .38 40 0   0   0 .022 .022 5.6 0    0     
float-benchs/filter2_iterated_true-unreach-call.c 0 560     560     15000   8100    20      .0041 - - - - 0 .60 .36 42 0   0   0 .024 .024 5.6 0    0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c 0 880     880     740   8700    .12   0      - - - - 0 .69 .42 40 0   0   0 .022 .022 5.6 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c 0 880     880     1800   8100    .070  0      - - - - 0 .59 .37 41 0   0   0 .027 .027 5.7 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c 0 870     880     710   9700    .11   0      - - - - 0 .66 .40 40 0   0   0 .021 .022 5.6 0    0     
float-benchs/filter_iir_true-unreach-call.c 0 880     880     850   7300    .12   0      - - - - 0 .73 .46 41 0   0   0 .021 .022 5.7 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c 2 .050 .047 7.8 .32 .0082 0      - - - - 2 4.1  2.3  250 0   0   2 13     7.9   310   .75 0     
float-benchs/image_filter_true-unreach-call.c 0 880     880     3000   6600    2.6    0      - - - - 0 .71 .44 40 0   0   0 .028 .030 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c 2 .91  .91  29   11    .057  0      - - - - 0 900    900    1400 0   0   0 960     950     1500   1.3  0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c 2 .94  .94  29   13    .057  0      - - - - 0 900    900    920 0   0   0 960     950     1500   .84 0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c 2 1.1   1.1   29   13    .057  0      - - - - 2 190    190    690 0   0   0 960     950     1600   .71 0     
float-benchs/interpolation2_true-unreach-call_true-termination.c 2 .52  .51  12   7.4  .025  0      - - - - 0 900    900    1300 0   0   0 960     950     1600   .72 0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c 2 .62  .61  20   6.5  .057  0      - - - - 2 530    530    1500 0   0   0 960     950     1500   .72 0     
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c 2 .58  .58  20   8.0  .057  0      - - - - 2 650    640    1500 0   0   0 960     950     1400   .70 .0082
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c 2 .67  .67  21   8.3  .057  0      - - - - 2 180    180    560 0   0   0 960     950     1500   .71 0     
float-benchs/interpolation_true-unreach-call_true-termination.c 2 .25  .25  8.7 3.0  .025  0      - - - - 0 900    900    1700 0   0   0 960     950     1600   .72 0     
float-benchs/inv_Newton_true-unreach-call.c 0 880     880     440   7200    .074  0      - - - - 0 .69 .42 42 0   0   0 .027 .027 5.6 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c 2 .39  .38  18   5.2  .0082 0      - - - - 2 7.0  5.2  310 0   0   2 95     86     1200   .71 0     
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c 2 .46  .46  12   5.7  .0082 0      - - - - 2 5.4  3.3  280 0   0   2 83     76     520   .71 0     
float-benchs/inv_square_int_true-unreach-call_true-termination.c 2 .14  .14  6.9 .92 .0082 0      - - -