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