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