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