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