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