Tool CBMC Path 5.10 () CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET 2018-12-06 10:22:39 CET 2018-12-12 19:23:37 CET 2018-12-06 07:24:45 CET 2018-12-06 09:28:06 CET
Run set cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.2   9.2   54   96    .0082 0      false(unreach-call) 1 wit inspect 57    55    340 0   0   false(unreach-call) 1 --- inspect 37     30     670   .71 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   4.8   false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.3   7.3   51   89    .0082 0      false(unreach-call) 1 wit inspect 13    11    350 0   0   timeout 0 --- inspect 97     91     700   1.7  0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0     false(unreach-call) 1 --- inspect .59   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.5   5.5   44   72    .0082 0      false(unreach-call) 1 wit inspect 39    37    350 0   0   false(unreach-call) 1 --- inspect 72     67     690   .65 0   false(unreach-call) 1 --- inspect 3.5  2.1  240 0   4.7   false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.4   2.4   41   31    .0082 0      false(unreach-call) 1 wit inspect 10    8.7  350 0   0   timeout 0 --- inspect 97     91     710   1.7  0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0     false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .92  .92  38   11    .0082 0      false(unreach-call) 1 wit inspect 12    10    350 0   0   false(unreach-call) 1 --- inspect 26     21     690   .75 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0     false(unreach-call) 1 --- inspect .57   .57   20    .053 .016  - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 57     57     140   600    .0082 0      timeout 0 wit inspect 92    90    450 0   0   timeout 0 --- inspect 97     90     800   1.1  0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   .012 false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 53     53     140   490    .0082 0      false(unreach-call) 1 wit inspect 83    81    450 0   0   timeout 0 --- inspect 97     91     800   1.3  0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   1.2   false(unreach-call) 1 --- inspect .58   .58   20    .053 .0041 - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 21     21     99   270    .0082 0      false(unreach-call) 1 wit inspect 22    20    450 0   0   false(unreach-call) 1 --- inspect 41     35     820   .71 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   .094 false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 340     340     460   3200    .0082 0      true -32 wit inspect 3.8  2.1  250 0   0   timeout 0 --- inspect 97     90     880   1.6  0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0     false(unreach-call) 1 --- inspect .59   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 38     38     150   360    .0082 0      true -32 wit inspect 4.2  2.3  250 0   0   false(unreach-call) 1 --- inspect 55     49     920   .71 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   .14  false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 84     84     220   820    .0082 0      true -32 wit inspect 4.8  2.7  250 0   0   timeout 0 --- inspect 97     91     920   2.2  0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   5.0   false(unreach-call) 1 --- inspect .60   .61   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .91  .90  21   11    .0082 0      timeout 0 wit inspect 92    90    330 0   0   timeout 0 --- inspect 97     92     590   2.0  0   false(unreach-call) 1 --- inspect 3.6  2.1  240 0   .025 false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.4   1.4   23   18    .0082 0      false(unreach-call) 1 wit inspect 7.7  5.5  310 0   0   timeout 0 --- inspect 97     91     570   .74 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   .041 false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.3   1.3   23   17    .0082 0      false(unreach-call) 1 wit inspect 9.0  7.2  300 0   0   timeout 0 --- inspect 97     90     600   1.6  0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0     false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.6   1.6   23   21    .0082 0      false(unreach-call) 1 wit inspect 12    10    310 0   0   true -32 --- inspect 7.4   4.1   290   .66 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0     false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.1   2.1   26   25    .0082 0      false(unreach-call) 1 wit inspect 58    56    340 0   0   true -32 --- inspect 6.8   3.8   300   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0     false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.5   1.4   26   18    .0082 0      false(unreach-call) 1 wit inspect 21    19    320 0   0   true -32 --- inspect 6.4   3.6   300   .62 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0     false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 2 wit inspect 320     320     95   2200    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0     timeout 0 --- inspect 960     950     960   .70 0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 2 wit inspect 100     100     85   1100    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0     timeout 0 --- inspect 960     950     780   1.7  0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 2 wit inspect 410     410     140   4900    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    570 0   0     timeout 0 --- inspect 960     950     960   .77 0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 2 wit inspect 300     300     240   2800    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    530 0   0     timeout 0 --- inspect 960     950     900   .84 0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 2 wit inspect 320     320     240   3000    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    830 0   0     timeout 0 --- inspect 960     950     970   1.1  0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 2 wit inspect 430     430     440   4200    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    530 0   0     timeout 0 --- inspect 960     950     990   1.7  0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 2 wit inspect 510     510     280   4400    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    530 0   0     timeout 0 --- inspect 960     950     1100   1.7  0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i true 2 wit inspect 700     700     660   6700    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0     timeout 0 --- inspect 960     950     890   1.8  0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i error (42) 0 --- inspect 880     880     520   9000    .057  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .026 .026 5.6 0    0     
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 2 wit inspect 670     670     430   7200    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0     timeout 0 --- inspect 960     950     1100   1.9  0     
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i true 2 wit inspect 720     720     450   6300    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    680 0   0     timeout 0 --- inspect 960     950     1100   1.6  0     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i error (42) 0 --- inspect 880     880     600   7400    .057  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0    0     
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i error (42) 0 --- inspect 880     880     480   8500    .057  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .022 .024 5.6 0    0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i error (42) 0 --- inspect 880     880     110   10000    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 2 wit inspect 250     250     86   3100    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    490 0   0     timeout 0 --- inspect 960     950     820   .78 0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 220     220     100   2500    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    650 0   0     timeout 0 --- inspect 960     950     820   1.6  0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 220     220     87   3000    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 800    800    590 0   0     timeout 0 --- inspect 960     950     820   .82 0     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 40     40     60   570    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 590    590    540 0   0     timeout 0 --- inspect 960     960     810   1.3  0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 250     250     140   3900    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 670    670    570 0   0     timeout (true) 0 --- inspect 960     950     830   .68 0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 250     250     110   2400    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 500    500    510 0   0     timeout 0 --- inspect 960     950     760   .78 0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 130     130     90   1500    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 260    260    500 0   0     timeout 0 --- inspect 960     950     770   1.7  0     
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 30     30     42   390    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    480 0   0     true 2 --- inspect 620     610     760   .68 0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 2.0   2.0   21   24    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 76    74    360 0   0     true 2 --- inspect 80     73     610   .71 .0082
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect .35  .35  17   4.8  .025  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.6  320 0   0     true 2 --- inspect 46     38     940   .71 0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect .31  .31  26   4.5  .016  .090  - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 14    11    780 0   0     error (7) 0 --- inspect 16     9.0   290   .75 0     
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect .065 .063 6.0 .20 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .51 42 0   0     error (invalid witness file) 0 --- inspect 5.7   3.1   270   .65 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 1.6   1.6   11   22    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    20    300 0   0     true 2 --- inspect 52     44     530   .68 0     
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect .042 .040 6.0 .31 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 43 0   0     error (invalid witness file) 0 --- inspect 5.1   3.2   260   .61 0     
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect .19  .19  12   2.7  .057  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  270 0   0     true 2 --- inspect 18     11     450   .68 0     
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect .080 .076 5.6 .22 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 44 0   0     error (invalid witness file) 0 --- inspect 5.5   3.0   270   .61 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect .040 .039 6.4 .22 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .47 43 0   0     error (invalid witness file) 0 --- inspect 5.6   3.1   260   .65 0     
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .12  .12  8.5 .72 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 42 0   0     error (invalid witness file) 0 --- inspect 6.7   3.7   270   .65 0     
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .094 .091 9.2 .78 .016  .016  - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 4.7  2.5  260 0   0     unknown 0 --- inspect 6.2   3.7   290   .62 0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .13  .13  9.6 1.5  .025  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.9  2.7  260 0   0     true 2 --- inspect 35     28     440   .68 0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect .11  .11  5.5 .21 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 43 0   0     error (invalid witness file) 0 --- inspect 5.0   3.2   270   .61 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect .040 .039 5.8 .29 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 44 0   0     error (invalid witness file) 0 --- inspect 5.0   2.8   260   .61 0     
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect .041 .041 6.5 .29 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 43 0   0     error (invalid witness file) 0 --- inspect 5.1   3.2   260   .61 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect .060 .058 6.5 .42 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0     true 2 --- inspect 19     14     300   .68 .078 
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect .051 .047 6.6 .30 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.1  250 0   0     true 2 --- inspect 14     8.4   310   .68 0     
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .075 .074 9.7 .76 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 43 0   0     error (invalid witness file) 0 --- inspect 5.3   2.9   260   .65 0     
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect .18  .17  9.5 2.2  .041  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 42 0   0     error (invalid witness file) 0 --- inspect 6.3   3.7   270   .61 3.4   
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .091 .087 9.6 .89 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  2.9  260 0   0     true 2 --- inspect 15     9.1   400   .68 .0082
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect .041 .039 5.9 .27 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 43 0   0     error (invalid witness file) 0 --- inspect 5.8   3.1   260   .61 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect .097 .094 8.1 .77 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0     true 2 --- inspect 24     17     370   .71 0     
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect .19  .18  11   1.7  .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.9  6.7  290 0   0     true 2 --- inspect 80     71     590   .68 0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect .059 .055 6.1 .64 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  270 0   0     true 2 --- inspect 230     210     770   .68 .078 
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect .037 .036 6.2 .35 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 43 0   0     error (invalid witness file) 0 --- inspect 5.1   2.8   260   .65 0     
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect .073 .069 7.2 .56 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.6  270 0   0     true 2 --- inspect 19     12     310   .68 .086 
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 10     10     26   120    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 78    76    340 0   0     true 2 --- inspect 87     79     570   .68 0     
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect .075 .073 7.4 .64 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.5  260 0   0     true 2 --- inspect 25     21     300   .68 0     
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect .099 .094 6.1 .50 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  250 0   0     true 2 --- inspect 15     8.6   300   .68 0     
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect .65  .65  9.9 8.7  .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.1  6.7  270 0   0     true 2 --- inspect 17     10     390   .68 0     
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect .14  .13  11   1.4  .016  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .91 .55 43 0   0     error (invalid witness file) 0 --- inspect 6.2   3.6   250   .61 0     
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect .14  .13  11   1.4  .016  .090  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 42 0   0     error (invalid witness file) 0 --- inspect 5.2   3.2   270   .61 0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .082 .070 8.9 .46 .0082 0      false(unreach-call) 1 wit inspect 5.0  2.7  250 0   0   false(unreach-call) 1 --- inspect 17     9.8   310   .75 0   unknown 0 --- inspect 3.8  2.3  250 0   .72  error (2) 0 --- inspect .56   .56   20    .037 0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .085 .076 8.8 .54 .0082 0      false(unreach-call) 1 wit inspect 4.2  2.4  270 0   0   false(unreach-call) 1 --- inspect 15     9.4   310   .68 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   4.9   false(unreach-call) 1 --- inspect .59   .59   20    .057 .0041 - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .076 .067 9.1 .84 .0082 0      false(unreach-call) 1 wit inspect 4.1  2.3  270 0   0   false(unreach-call) 1 --- inspect 13     8.6   310   .71 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   .32  false(unreach-call) 1 --- inspect .59   .58   20    .057 .0041 - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  .12  9.2 .68 .0082 0      false(unreach-call) 1 wit inspect 4.2  2.4  260 0   0   false(unreach-call) 1 --- inspect 13     8.2   300   .71 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0     false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c error (42) 0 --- inspect 880     880     540   6400    .17   0      error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .62 47 0   0     error (invalid witness file) 0 --- inspect .0016 .0021 .52 0     0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c error (42) 0 --- inspect 880     880     500   8000    .99   0      error (invalid witness file) 0 --- inspect .80 .49 42 0   0   error (2) 0 --- inspect .026 .027 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .64 48 0   0     error (invalid witness file) 0 --- inspect .0055 .0072 .40 0     0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .096 .083 8.8 .48 .0082 0      false(unreach-call) 1 wit inspect 4.0  2.3  260 0   0   false(unreach-call) 1 --- inspect 14     8.3   310   .71 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   5.0   false(unreach-call) 1 --- inspect .61   .61   20    .053 0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .066 .057 9.5 .42 .0082 0      false(unreach-call) 1 wit inspect 3.8  2.1  260 0   0   false(unreach-call) 1 --- inspect 15     9.3   300   .75 0   unknown 0 --- inspect 3.7  2.1  250 0   .012 error (2) 0 --- inspect .58   .57   20    .037 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .061 .053 9.9 .49 .0082 0      false(unreach-call) 1 wit inspect 4.8  2.7  260 0   0   false(unreach-call) 1 --- inspect 14     8.1   310   .68 0   unknown 0 --- inspect 3.7  2.2  240 0   0     error (2) 0 --- inspect .54   .54   20    .037 0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .25  .24  18   2.1  .0082 0      true -32 wit inspect 7.1  3.8  260 0   0   false(unreach-call) 1 --- inspect 33     24     1000   .68 0   true -32 --- inspect 4.5  2.5  270 0   5.1   true -32 --- inspect .65   .65   20    .086 0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect .33  .32  32   4.1  .0082 0      true -32 wit inspect 4.6  2.5  250 0   0   false(unreach-call) 1 --- inspect 23     16     590   .71 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   5.0   false(unreach-call) 1 --- inspect .62   .62   20    .061 0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .31  .30  6.3 2.4  .049  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .38 43 0   0     error (invalid witness file) 0 --- inspect 5.0   2.8   270   .61 0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect .25  .25  6.2 3.3  .086  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 13    11    500 0   0     timeout 0 --- inspect 960     910     4500   .68 0     
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect .045 .045 6.4 .32 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 44 0   0     error (invalid witness file) 0 --- inspect 5.1   3.3   270   .55 0     
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect .11  .099 6.3 .26 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 42 0   0     error (invalid witness file) 0 --- inspect 5.5   2.9   260   .65 0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect .042 .041 6.4 .34 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .88 .52 44 0   0     error (invalid witness file) 0 --- inspect 5.9   3.4   270   .61 0     
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect .044 .044 6.3 .30 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .53 42 0   0     error (invalid witness file) 0 --- inspect 5.4   2.9   270   .61 0     
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect .041 .040 6.3 .30 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .85 .50 43 0   0     error (invalid witness file) 0 --- inspect 7.4   4.1   270   .61 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 82     82     380   1100    .033  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    38    500 0   0     error (7) 0 --- inspect 140     130     2600   .68 0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c out of memory 0 --- inspect 720     720     15000   8800    290      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 42 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .047 .047 6.3 .32 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 42 0   0     error (invalid witness file) 0 --- inspect 5.1   2.8   250   .61 0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 2 wit inspect 290     290     160   1900    .057  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1200 0   0     timeout 0 --- inspect 960     950     3000   1.6  0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c out of memory 0 --- inspect 510     510     15000   5700    130      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .020 .021 5.5 0    0     
float-benchs/divmul_diverge_true-unreach-call_true-termination.c out of memory 0 --- inspect 510     510     15000   5900    100      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .48 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0    0     
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .073 .072 6.6 .54 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .50 43 0   0     error (invalid witness file) 0 --- inspect 6.3   3.7   260   .61 0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect .12  .12  6.2 .40 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 42 0   0     error (invalid witness file) 0 --- inspect 5.6   3.0   260   .61 0     
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 7.6   7.6   22   110    11      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 18    14    520 0   0     timeout 0 --- inspect 960     950     1200   .76 0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c out of memory 0 --- inspect 620     620     15000   7000    120      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0     error (2) 0 --- inspect .055 .056 5.5 0    0     
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c error (134) 0 --- inspect .046 .045 6.6 .28 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .026 .027 5.5 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c error (134) 0 --- inspect .079 .078 6.5 .28 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0     error (2) 0 --- inspect .025 .026 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c error (134) 0 --- inspect .053 .053 6.4 .36 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0     error (2) 0 --- inspect .023 .025 5.7 0    0     
float-benchs/filter1_true-unreach-call_true-termination.c error (42) 0 --- inspect 880     880     4100   11000    110      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     
float-benchs/filter2_alt_true-unreach-call.c error (42) 0 --- inspect 880     880     220   11000    1.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0     
float-benchs/filter2_iterated_true-unreach-call.c out of memory 0 --- inspect 420     420     15000   5700    .59   .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 42 0   0     error (2) 0 --- inspect .022 .022 5.6 0    0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c error (134) 0 --- inspect .98  .98  33   15    .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c error (42) 0 --- inspect 880     880     540   8500    1.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .34 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c error (42) 0 --- inspect 880     880     290   8700    2.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .023 .023 5.6 0    0     
float-benchs/filter_iir_true-unreach-call.c error (42) 0 --- inspect 880     880     380   8900    2.1    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .43 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect .044 .042 6.4 .27 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 42 0   0     error (invalid witness file) 0 --- inspect 5.0   3.2   270   .61 0     
float-benchs/image_filter_true-unreach-call.c error (42) 0 --- inspect 880     880     5500   10000    330      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 40 0   0     error (2) 0 --- inspect .023 .024 5.8 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .98  .98  29   13    .21   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 14    11    370 0   0     timeout 0 --- inspect 960     950     1400   1.6  0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect .97  .97  29   11    .21   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 9.0  6.7  350 0   0     timeout 0 --- inspect 960     950     1500   1.6  0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 1.3   1.3   30   16    .28   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 42    40    410 0   0     timeout 0 --- inspect 960     950     1500   1.6  0     
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect .65  .65  12   8.3  .19   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1800 0   0     timeout 0 --- inspect 960     950     1500   .78 0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .62  .62  21   8.5  .18   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 8.9  6.0  330 0   0     timeout 0 --- inspect 960     950     1500   .81 .012 
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect .57  .57  21   7.2  .18   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 53    51    350 0   0     timeout 0 --- inspect 960     950     1500   1.2  .0082
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect .75  .75  21   10    .26   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 25    22    430 0   0     timeout 0 --- inspect 960     950     1400   1.6  0     
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect .36  .35  9.6 5.0  .18   .13   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    2200 0   0     timeout 0 --- inspect 960     950     1700   .79 0     
float-benchs/inv_Newton_true-unreach-call.c error (42) 0 --- inspect 880     880     390   7700    .13   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 40 0   0     error (2) 0 --- inspect .022 .023 5.7 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect .94  .94  20   10    .020  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.0  5.9  310 0   0     true 2 --- inspect 90     82     1200   .68 0     
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect .24  .24  12   3.1  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  3.3  280 0   0     true 2 --- inspect 72     65     510   .68 .078 
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect .11  .10  7.2 1.0  .0082 0      - --- inspect - ---