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