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 ---