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