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