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