Tool skink 2.0 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-07 12:00:55 CET 2018-12-07 18:03:00 CET 2018-12-07 19:11:22 CET 2018-12-07 19:49:22 CET 2018-12-12 21:02:00 CET 2018-12-07 17:09:07 CET 2018-12-07 18:50:30 CET
Run set skink.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options -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/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/skink.2018-12-07_1200.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/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/skink.2018-12-07_1200.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 unknown 0 --- inspect 34   35   2900 310 .049 0      error (invalid witness file) 0 --- inspect .70 .43 41 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .63 47 0   0   error (invalid witness file) 0 --- inspect .0056 .0072 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i unknown 0 --- inspect 34   35   2900 280 .21  0      error (invalid witness file) 0 --- inspect .75 .45 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0   error (invalid witness file) 0 --- inspect .0020 .0025 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i unknown 0 --- inspect 34   35   2900 280 .049 0      error (invalid witness file) 0 --- inspect .73 .46 40 0   0   error (2) 0 --- inspect .023 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .65 46 0   0   error (invalid witness file) 0 --- inspect .0040 .0051 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i unknown 0 --- inspect 37   39   2900 350 .082 0      error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .73 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0021 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i unknown 0 --- inspect 33   35   2900 290 .21  0      error (invalid witness file) 0 --- inspect .69 .43 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .80 46 0   0   error (invalid witness file) 0 --- inspect .0019 .0045 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i unknown 0 --- inspect 35   36   2900 330 .049 0      error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .74 48 0   0   error (invalid witness file) 0 --- inspect .0023 .0030 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i unknown 0 --- inspect 34   35   2900 330 .25  0      error (invalid witness file) 0 --- inspect .74 .44 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 48 0   0   error (invalid witness file) 0 --- inspect .0068 .0085 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i unknown 0 --- inspect 33   35   2900 280 .25  0      error (invalid witness file) 0 --- inspect .68 .42 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0   error (invalid witness file) 0 --- inspect .0061 .0073 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i unknown 0 --- inspect 35   36   2900 310 .049 0      error (invalid witness file) 0 --- inspect .69 .43 41 0   0   error (2) 0 --- inspect .042 .043 5.5 0    0   error (invalid witness file) 0 --- inspect 1.1  .73 47 0   0   error (invalid witness file) 0 --- inspect .0045 .0059 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i unknown 0 --- inspect 35   35   2900 320 .049 0      error (invalid witness file) 0 --- inspect .73 .46 40 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 48 0   0   error (invalid witness file) 0 --- inspect .0018 .0021 .40 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i unknown 0 --- inspect 35   35   2900 320 .29  0      error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .75 48 0   0   error (invalid witness file) 0 --- inspect .0057 .0077 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 31   24   2800 250 .18  0      false(unreach-call) 1 wit inspect 15    13    320 0   0   timeout 0 --- inspect 97     92     610   1.5  0   true -32 --- inspect 3.6  2.1  240 0   0   true -32 --- inspect .58   .58   20    .049 .0041 - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 32   25   2800 260 .17  0      false(unreach-call) 1 wit inspect 60    58    340 0   0   timeout 0 --- inspect 97     91     570   .75 0   true -32 --- inspect 4.9  2.8  250 0   0   true -32 --- inspect .57   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 28   20   2800 230 .18  0      timeout 0 wit inspect 92    90    380 0   0   timeout 0 --- inspect 97     91     610   .72 0   true -32 --- inspect 4.5  2.6  250 0   0   true -32 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i unknown 0 --- inspect 33   35   1300 290 .17  0      error (invalid witness file) 0 --- inspect .72 .45 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0   error (invalid witness file) 0 --- inspect .0053 .010  .53 0     0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i unknown 0 --- inspect 32   35   1300 320 .049 0      error (invalid witness file) 0 --- inspect .75 .45 41 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .79 49 0   0   error (invalid witness file) 0 --- inspect .0054 .0080 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i unknown 0 --- inspect 33   35   1200 310 .17  0      error (invalid witness file) 0 --- inspect .64 .41 41 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0   error (invalid witness file) 0 --- inspect .0047 .0062 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i unknown 0 --- inspect 34   35   2900 320 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i unknown 0 --- inspect 33   35   2900 290 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .030 .033 5.6 0    0   
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i unknown 0 --- inspect 34   35   2900 310 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 42 0   0   error (2) 0 --- inspect .027 .029 5.6 0    0   
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i unknown 0 --- inspect 44   45   2900 500 .082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i unknown 0 --- inspect 35   36   2900 330 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 42 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0   
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i unknown 0 --- inspect 41   42   2900 400 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 42 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0   
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i unknown 0 --- inspect 35   36   2900 330 .049 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-cdfpl/newton_2_5_true-unreach-call_true-termination.i unknown 0 --- inspect 34   35   2900 350 .25  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .020 .022 5.6 0    0   
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i unknown 0 --- inspect 35   35   2900 410 .041 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i unknown 0 --- inspect 35   35   2900 310 .041 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i unknown 0 --- inspect 35   35   2900 330 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i unknown 0 --- inspect 35   36   2900 390 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i unknown 0 --- inspect 35   35   2900 310 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
floats-cdfpl/sine_4_true-unreach-call_true-termination.i unknown 0 --- inspect 32   35   2800 330 .16  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   
floats-cdfpl/sine_5_true-unreach-call_true-termination.i unknown 0 --- inspect 33   35   2800 310 .049 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   
floats-cdfpl/sine_6_true-unreach-call_true-termination.i unknown 0 --- inspect 32   35   2800 300 .16  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
floats-cdfpl/sine_7_true-unreach-call_true-termination.i unknown 0 --- inspect 32   35   2800 310 .16  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   
floats-cdfpl/sine_8_true-unreach-call_true-termination.i unknown 0 --- inspect 31   35   2800 270 .16  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
floats-cdfpl/square_4_true-unreach-call_true-termination.i unknown 0 --- inspect 32   35   1300 390 .17  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 40 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   
floats-cdfpl/square_5_true-unreach-call_true-termination.i unknown 0 --- inspect 32   35   1600 300 .086 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   
floats-cdfpl/square_6_true-unreach-call_true-termination.i unknown 0 --- inspect 32   35   1300 270 .17  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0   
floats-cdfpl/square_7_true-unreach-call_true-termination.i unknown 0 --- inspect 32   35   1300 270 .17  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   
floats-cdfpl/square_8_true-unreach-call_true-termination.i unknown 0 --- inspect 32   35   1300 350 .17  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .025 .026 5.5 0    0   
floats-cbmc-regression/float-div1_true-unreach-call.i unknown 0 --- inspect 10   4.4 300 88 .37  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 19   6.8 580 170 3.5   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    8.6  780 0   0   error (7) 0 --- inspect 14     8.0   290   .75 0   
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 3.6 1.7 210 36 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 12     7.4   300   .75 0   
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 12   5.2 370 110 .49  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    18    300 0   0   true 2 --- inspect 48     41     540   .71 0   
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 3.7 1.7 200 37 .037 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 12     7.3   300   .75 0   
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 16   5.8 480 160 1.3   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.6  270 0   0   true 2 --- inspect 20     11     450   .75 0   
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 3.8 1.7 210 37 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 17     10     310   .75 0   
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 3.7 1.7 210 33 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 13     7.5   300   .71 0   
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 4.0 1.8 210 33 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.5  280 0   0   error (7) 0 --- inspect 16     8.5   280   .68 0   
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 --- inspect 8.2 3.7 250 77 .38  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .026 .028 5.8 0    0   
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 11   5.0 320 95 .36  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  260 0   0   true 2 --- inspect 25     19     420   .75 0   
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 3.7 1.7 200 29 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 15     9.1   300   .71 0   
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 4.0 1.8 220 36 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.0  250 0   0   true 2 --- inspect 16     9.1   310   .75 0   
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 3.6 1.7 210 36 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 13     8.1   300   .75 0   
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 17   9.2 360 150 .14  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 21     15     300   .75 0   
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 3.7 1.7 200 35 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 15     9.3   300   .75 0   
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 9.2 4.1 300 88 .35  .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  260 0   0   true 2 --- inspect 20     11     410   .71 0   
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 3.9 1.8 210 32 .037 .078  - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    33    650 0   0   error (7) 0 --- inspect 13     7.0   280   .75 0   
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 11   5.2 340 120 .37  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  260 0   0   true 2 --- inspect 16     9.9   400   .68 0   
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 3.8 1.7 200 40 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 17     9.7   310   .68 0   
floats-cbmc-regression/float20_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 7.4 2.7 330 65 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.1  260 0   0   true 2 --- inspect 24     17     370   .68 0   
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 15   8.4 390 150 .53  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.3  6.3  300 0   0   true 2 --- inspect 80     71     590   .68 0   
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 4.1 1.9 220 41 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  270 0   0   true 2 --- inspect 200     190     770   .71 0   
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 3.6 1.7 210 33 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 15     8.9   310   .75 0   
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 6.1 2.4 300 56 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.1  270 0   0   true 2 --- inspect 18     12     310   .71 0   
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 18   10   370 170 .67  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 69    67    330 0   0   true 2 --- inspect 87     80     580   .68 0   
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 6.1 2.5 300 57 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  2.0  260 0   0   true 2 --- inspect 29     24     300   .75 0   
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 16   6.0 390 140 .68  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  260 0   0   true 2 --- inspect 17     9.8   300   .75 0   
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 12   4.9 320 110 .36  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.8  5.7  270 0   0   true 2 --- inspect 15     8.8   390   .75 0   
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 13   5.1 380 120 .68  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.7  260 0   0   error (7) 0 --- inspect 12     7.0   280   .75 0   
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 11   4.3 320 100 .42  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  260 0   0   true 2 --- inspect 17     9.7   430   .75 0   
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 11   4.6 320 100 .18  0      exception 0 --- inspect 2.7  1.5  200 0   0   false(unreach-call) 1 --- inspect 15     8.4   310   .75 0   exception 0 --- inspect 3.9  2.2  200 0   0   true -32 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   5.1 360 120 .16  0      false(unreach-call) 1 wit inspect 4.6  2.6  270 0   0   false(unreach-call) 1 --- inspect 13     8.2   300   .75 0   false(unreach-call) 1 --- inspect 3.9  2.2  250 0   0   false(unreach-call) 1 --- inspect .61   .62   20    .053 0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 14   6.7 390 110 .16  0      false(unreach-call) 1 wit inspect 4.4  2.5  270 0   0   false(unreach-call) 1 --- inspect 13     8.0   300   .75 0   false(unreach-call) 1 --- inspect 4.4  2.5  250 0   0   false(unreach-call) 1 --- inspect .61   .60   20    .049 0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 22   15   470 190 .15  0      false(unreach-call) 1 wit inspect 5.0  2.8  260 0   0   false(unreach-call) 1 --- inspect 13     7.6   310   .68 0   false(unreach-call) 1 --- inspect 4.2  2.4  250 0   0   false(unreach-call) 1 --- inspect .59   .60   20    .049 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c unknown 0 --- inspect 84   85   1000 670 .049 0      error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .021 .021 5.7 0    0   error (invalid witness file) 0 --- inspect 1.3  .82 49 0   0   error (invalid witness file) 0 --- inspect .0052 .0072 .52 0     0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c unknown 0 --- inspect 200   200   3100 2100 .057 0      error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0   error (invalid witness file) 0 --- inspect 1.1  .73 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0098 .49 0     0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 22   15   510 180 .16  0      false(unreach-call) 1 wit inspect 4.1  2.3  260 0   0   false(unreach-call) 1 --- inspect 15     9.1   300   .75 0   false(unreach-call) 1 --- inspect 4.7  2.7  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.7 4.4 300 90 .13  0      exception 0 --- inspect 2.7  1.5  200 0   0   false(unreach-call) 1 --- inspect 12     7.8   300   .68 0   exception 0 --- inspect 3.9  2.3  200 0   0   true -32 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 11   4.6 330 110 .13  0      exception 0 --- inspect 3.2  1.8  200 0   0   false(unreach-call) 1 --- inspect 13     7.6   290   .75 0   exception 0 --- inspect 3.6  2.1  200 0   0   true -32 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 31   19   670 340 1.2   0      false(unreach-call) 1 wit inspect 8.8  5.5  330 0   0   true -32 --- inspect 8.9   4.8   320   .66 0   true -32 --- inspect 6.1  3.4  280 0   0   true -32 --- inspect .63   .64   20    .082 0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 15   6.2 470 140 .36  0      false(unreach-call) 1 wit inspect 17    14    420 0   0   true -32 --- inspect 6.6   4.1   300   .66 0   false(unreach-call) 1 --- inspect 4.6  2.6  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .057 0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c unknown 0 --- inspect 37   22   1400 400 39     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c unknown 0 --- inspect 42   26   1400 470 17     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.8 220 33 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 26     20     990   .71 0   
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 3.8 1.8 210 35 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 15     11     430   .75 0   
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 3.9 1.8 220 42 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 13     7.5   310   .75 0   
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.8 220 36 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 14     7.6   300   .75 0   
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 4.0 1.8 220 34 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 14     8.1   300   .75 0   
float-benchs/arctan_Pade_true-unreach-call_true-termination.c unknown 0 --- inspect 59   58   2300 540 .11  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 42 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   
float-benchs/bary_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 170   150   2900 2500 70     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0   
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 3.7 1.8 230 34 .037 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 7.4   4.1   300   .66 0   
float-benchs/cos_polynomial_true-unreach-call_true-termination.c unknown 0 --- inspect 23   25   570 220 .32  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .025 .027 5.6 0    0   
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 59   41   2200 810 19     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
float-benchs/divmul_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 52   36   1700 660 .34  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 3.8 1.8 210 36 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    22    410 0   0   true 2 --- inspect 400     380     690   .71 0   
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.8 210 39 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    21    410 0   0   true 2 --- inspect 490     480     710   .71 0   
float-benchs/exp_loop_true-unreach-call.c unknown 0 --- inspect 59   43   1700 680 21     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .030 .030 5.6 0    0   
float-benchs/feedback_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 65   48   1700 810 42     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c unknown 0 --- inspect 98   97   910 1200 .45  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c unknown 0 --- inspect 140   120   2000 2200 85     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .024 .024 5.5 0    0   
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c unknown 0 --- inspect 140   120   1800 1800 96     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
float-benchs/filter1_true-unreach-call_true-termination.c unknown 0 --- inspect 54   56   550 520 .098 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .026 .027 5.7 0    0   
float-benchs/filter2_alt_true-unreach-call.c unknown 0 --- inspect 120   99   2800 1500 8.2   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   
float-benchs/filter2_iterated_true-unreach-call.c unknown 0 --- inspect 100   83   2100 1600 64     .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0   
float-benchs/filter2_reinit_true-unreach-call_true-termination.c unknown 0 --- inspect 58   59   780 510 .078 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   
float-benchs/filter2_set_true-unreach-call_true-termination.c unknown 0 --- inspect 59   59   990 490 .086 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .020 .022 5.6 0    0   
float-benchs/filter2_true-unreach-call_true-termination.c unknown 0 --- inspect 54   56   810 570 .074 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   
float-benchs/filter_iir_true-unreach-call.c unknown 0 --- inspect 13   5.0 310 120 .32  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/float_double_true-unreach-call_true-termination.c true 2 wit inspect 3.8 1.8 210 41 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 12     7.4   300   .71 0   
float-benchs/image_filter_true-unreach-call.c unknown 0 --- inspect 46   25   3900 470 35     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 70   60   1800 540 .29  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    630 0   0   timeout 0 --- inspect 960     950     1600   .71 0   
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 70   60   1800 580 .18  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 63    61    570 0   0   timeout 0 --- inspect 960     950     1600   .71 0   
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c unknown 0 --- inspect 56   39   1900 630 12     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect 79   69   1900 610 .053 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    38    550 0   0   timeout 0 --- inspect 960     950     1600   .68 0   
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 66   57   1800 470 .066 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 30    28    470 0   0   timeout 0 --- inspect 960     950     1500   .72 0   
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 66   57   1800 470 .25  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 71    68    480 0   0   timeout 0 --- inspect 960     950     1500   .71 0   
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c unknown 0 --- inspect 54   37   1700 560 15     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0   error (2) 0 --- inspect .021 .021 5.7 0    0   
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect 78   68   1700 530 .28  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    24    480 0   0   timeout 0 --- inspect 960     950     1700   .27 0   
float-benchs/inv_Newton_true-unreach-call.c unknown 0 --- inspect 76   78   1000 640 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 13   5.7 410 130 .22  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.2  4.5  310 0   0   true 2 --- inspect 93     84     1200   .71 0   
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect 38   31   840 290 .19  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.7  280 0   0   true 2 --- inspect 71     65     510   .71 0   
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 27   20   470 230 .15  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  260 0   0   true 2 --- inspect 100     99     360   .71 0   
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 6.2 2.4 310 50 .037 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  260 0   0   true 2 --- inspect 62     57     350   .71 0   
float-benchs/loop_true-unreach-call.c unknown 0 --- inspect 37   22   1300 400 41     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   
float-benchs/mea8000_true-unreach-call.c unknown 0 --- inspect 27   8.8 830 230 2.4   0      - --- inspect - --- inspect - ---