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