Tool DepthK 3.1 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* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] 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-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 09:26:28 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-depthk.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/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.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/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.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 26    26    99 360   1.0  0      false(unreach-call) 1 wit inspect 51    49    350 0     0   false(unreach-call) 1 --- inspect 37     32     670   .68 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 33    33    99 420   .85 0      false(unreach-call) 1 wit inspect 13    11    350 0     0   timeout 0 --- inspect 97     91     690   1.6  0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 42    42    100 580   1.0  0      false(unreach-call) 1 wit inspect 36    34    350 0     0   false(unreach-call) 1 --- inspect 68     63     700   .68 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0   false(unreach-call) 1 --- inspect .58   .59   20    .053 .0041 - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.0  9.0  100 130   1.0  0      false(unreach-call) 1 wit inspect 13    11    350 0     0   timeout 0 --- inspect 97     92     700   1.3  0   false(unreach-call) 1 --- inspect 3.5  2.1  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 39    39    99 520   1.0  0      false(unreach-call) 1 wit inspect 9.6  7.9  350 0     0   false(unreach-call) 1 --- inspect 27     22     680   .71 0   false(unreach-call) 1 --- inspect 3.5  2.1  240 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 130    130    200 1700   1.0  0      true -32 wit inspect 4.8  2.6  250 0     0   timeout 0 --- inspect 97     91     790   1.7  0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 120    120    200 1400   1.0  0      true -32 wit inspect 4.2  2.3  250 0     0   timeout 0 --- inspect 97     91     800   1.6  0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0   false(unreach-call) 1 --- inspect .58   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 61    61    200 740   .85 0      true -32 wit inspect 5.0  2.8  250 0     0   false(unreach-call) 1 --- inspect 39     33     820   .71 0   false(unreach-call) 1 --- inspect 3.7  2.2  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 100    100    300 980   1.0  0      true -32 wit inspect 4.0  2.2  250 0     0   timeout 0 --- inspect 97     91     890   1.6  0   false(unreach-call) 1 --- inspect 3.7  2.2  240 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 120    120    280 1400   1.0  0      true -32 wit inspect 4.9  2.7  250 0     0   false(unreach-call) 1 --- inspect 52     46     910   .71 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0   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 130    130    310 1500   .85 0      true -32 wit inspect 5.0  2.8  250 0     0   timeout 0 --- inspect 97     91     930   .83 0   false(unreach-call) 1 --- inspect 3.6  2.1  240 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 20    20    71 320   1.0  0      true -32 wit inspect 4.1  2.3  250 0     0   timeout 0 --- inspect 97     91     610   2.3  0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 20    20    71 240   1.0  0      true -32 wit inspect 4.3  2.4  250 0     0   timeout 0 --- inspect 97     91     570   1.1  0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19    19    71 310   1.0  0      true -32 wit inspect 4.3  2.3  250 0     0   timeout 0 --- inspect 97     91     610   1.9  0   false(unreach-call) 1 --- inspect 3.5  2.1  240 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.8  4.8  64 73   1.0  0      true -32 wit inspect 3.5  2.0  250 0     0   false(unreach-call) 1 --- inspect 88     83     450   .71 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_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.9  6.9  62 85   1.0  0      true -32 wit inspect 3.9  2.1  250 0     0   timeout (false(unreach-call)) 0 --- inspect 96     91     430   .68 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .56   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.6  7.6  63 110   1.0  0      true -32 wit inspect 3.6  2.0  250 0     0   timeout 0 --- inspect 97     91     460   1.9  0   false(unreach-call) 1 --- inspect 4.1  2.4  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i unknown 0 wit inspect 110    110    100 1400   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    590 0     0   timeout 0 --- inspect 960     950     990   .70 0  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i unknown 0 wit inspect 120    120    100 1700   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0     0   timeout 0 --- inspect 960     950     800   1.1  0  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i unknown 0 wit inspect 130    130    100 1800   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    570 0     0   timeout 0 --- inspect 960     950     970   .68 0  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i unknown 0 wit inspect 480    480    200 6000   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    530 0     0   timeout 0 --- inspect 960     950     880   .72 0  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i unknown 0 wit inspect 510    510    200 5900   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    840 0     0   timeout 0 --- inspect 960     950     990   .71 0  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i unknown 0 wit inspect 480    480    200 5800   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    520 0     0   timeout 0 --- inspect 960     950     1000   .69 0  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i unknown 0 wit inspect 470    470    200 6500   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    570 0     0   timeout 0 --- inspect 960     950     1100   .72 0  
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i unknown 0 wit inspect 540    540    200 6900   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0     0   timeout 0 --- inspect 960     950     900   1.1  0  
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i unknown 0 wit inspect 890    900    300 12000   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    590 0     0   timeout 0 --- inspect 960     950     1000   .72 0  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    310 9600   21    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    550 0     0   timeout 0 --- inspect 960     950     1100   .68 0  
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    300 13000   21    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    680 0     0   timeout 0 --- inspect 960     950     1100   .68 0  
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    310 10000   21    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    700 0     0   timeout 0 --- inspect 960     950     1000   .72 0  
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i unknown 0 wit inspect 900    900    310 9800   21    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0     0   timeout 0 --- inspect 960     950     1000   .72 0  
floats-cdfpl/sine_4_true-unreach-call_true-termination.i unknown 0 wit inspect 100    100    73 1500   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    500 0     0   timeout 0 --- inspect 960     950     790   .72 0  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i unknown 0 wit inspect 53    53    72 570   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    490 0     0   timeout 0 --- inspect 960     950     820   .72 0  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i unknown 0 wit inspect 62    62    72 760   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    650 0     0   timeout 0 --- inspect 960     950     830   1.1  0  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i unknown 0 wit inspect 44    44    72 570   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 680    670    590 0     0   timeout 0 --- inspect 960     950     830   .71 0  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i unknown 0 wit inspect 53    53    72 790   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 510    510    540 0     0   timeout 0 --- inspect 960     950     810   .69 0  
floats-cdfpl/square_4_true-unreach-call_true-termination.i unknown 0 wit inspect 87    87    66 1100   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 660    660    570 0     0   true 2 --- inspect 860     850     730   .68 0  
floats-cdfpl/square_5_true-unreach-call_true-termination.i unknown 0 wit inspect 41    41    67 580   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 490    490    500 0     0   timeout 0 --- inspect 960     950     760   .72 0  
floats-cdfpl/square_6_true-unreach-call_true-termination.i unknown 0 wit inspect 36    36    67 570   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 230    220    500 0     0   timeout 0 --- inspect 960     950     770   1.0  0  
floats-cdfpl/square_7_true-unreach-call_true-termination.i unknown 0 wit inspect 22    22    65 310   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    480 0     0   true 2 --- inspect 640     630     780   .71 0  
floats-cdfpl/square_8_true-unreach-call_true-termination.i unknown 0 wit inspect 17    17    65 270   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 64    63    360 0     0   true 2 --- inspect 80     74     610   .68 0  
floats-cbmc-regression/float-div1_true-unreach-call.i unknown 0 wit inspect 10    9.9  77 140   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  3.4  320 0     0   true 2 --- inspect 44     37     930   .71 0  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i unknown 0 wit inspect 1.0  .73 67 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    8.9  780 0     0   error (7) 0 --- inspect 14     7.9   280   .75 0  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i unknown 0 wit inspect .79 .53 65 9.1 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.1  250 0     0   true 2 --- inspect 16     9.1   300   .75 0  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i unknown 0 wit inspect 6.0  5.8  66 68   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    18    300 0     0   true 2 --- inspect 51     44     550   .68 0  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i unknown 0 wit inspect .77 .52 67 8.6 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0     0   true 2 --- inspect 13     7.6   300   .71 0  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i unknown 0 wit inspect .93 .67 67 9.5 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.6  270 0     0   true 2 --- inspect 18     10     440   .68 0  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i unknown 0 wit inspect .80 .55 66 8.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0     0   true 2 --- inspect 13     8.3   310   .68 0  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i unknown 0 wit inspect .79 .54 66 8.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.0  250 0     0   true 2 --- inspect 13     7.6   300   .71 0  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i unknown 0 wit inspect .82 .57 65 8.7 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0     0   error (7) 0 --- inspect 13     7.8   290   .75 0  
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 wit inspect .98 .72 66 13   26    0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 4.8  2.6  250 0     0   unknown 0 --- inspect 6.5   3.6   290   .62 0  
floats-cbmc-regression/float-to-double1_true-unreach-call.i unknown 0 wit inspect 1.4  1.1  66 16   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  260 0     0   true 2 --- inspect 37     29     450   .71 0  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i unknown 0 wit inspect .81 .52 67 8.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0     0   true 2 --- inspect 12     7.1   300   .75 0  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i unknown 0 wit inspect .82 .56 66 8.4 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0     0   true 2 --- inspect 14     8.2   310   .68 0  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i unknown 0 wit inspect .82 .57 66 9.1 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0     0   true 2 --- inspect 13     7.8   300   .68 0  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i unknown 0 wit inspect 1.2  .90 66 13   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0     0   true 2 --- inspect 18     13     300   .75 0  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i unknown 0 wit inspect .78 .53 66 8.1 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0     0   true 2 --- inspect 14     7.8   310   .68 0  
floats-cbmc-regression/float14_true-unreach-call.i unknown 0 wit inspect .82 .57 67 8.9 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.6  3.0  250 0     0   true 2 --- inspect 19     11     390   .68 0  
floats-cbmc-regression/float18_true-unreach-call.i unknown 0 --- inspect 900    900    2300 12000   110    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0  
floats-cbmc-regression/float19_true-unreach-call.i unknown 0 wit inspect 1.0  .77 66 11   30    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  260 0     0   true 2 --- inspect 16     9.7   390   .68 0  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i unknown 0 wit inspect .81 .54 66 9.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0     0   true 2 --- inspect 13     7.9   290   .71 0  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i unknown 0 wit inspect .94 .69 66 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0     0   true 2 --- inspect 20     15     370   .75 0  
floats-cbmc-regression/float21_true-unreach-call.i unknown 0 wit inspect 1.5  1.2  67 17   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    8.0  290 0     0   true 2 --- inspect 80     71     600   .71 0  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i unknown 0 wit inspect .97 .72 67 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.2  270 0     0   true 2 --- inspect 230     210     740   .71 0  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i unknown 0 wit inspect .89 .62 67 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0     0   true 2 --- inspect 13     8.2   310   .68 0  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i unknown 0 wit inspect .80 .54 67 8.7 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  270 0     0   true 2 --- inspect 16     11     320   .75 0  
floats-cbmc-regression/float4_true-unreach-call.i unknown 0 wit inspect 3.1  2.8  67 38   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 63    61    330 0     0   true 2 --- inspect 92     84     580   .68 0  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i unknown 0 wit inspect 1.4  1.1  65 16   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  260 0     0   true 2 --- inspect 29     24     300   .71 0  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i unknown 0 wit inspect .83 .59 66 8.5 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0     0   true 2 --- inspect 15     9.0   300   .68 0  
floats-cbmc-regression/float8_true-unreach-call.i unknown 0 wit inspect .84 .57 68 9.0 26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.0  6.0  270 0     0   true 2 --- inspect 16     9.1   390   .75 0  
floats-cbmc-regression/float_lib1_true-unreach-call.i unknown 0 wit inspect 2.7  2.4  67 30   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.7  260 0     0   error (7) 0 --- inspect 14     7.6   290   .75 0  
floats-cbmc-regression/float_lib2_true-unreach-call.i unknown 0 wit inspect .84 .59 67 9.1 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  260 0     0   true 2 --- inspect 18     10     430   .75 0  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .18 .17 33 1.6 1.0  0      true -32 wit inspect 4.5  2.5  250 0     0   false(unreach-call) 1 --- inspect 16     8.8   320   .75 0   unknown 0 --- inspect 3.5  2.0  240 0   0   error (2) 0 --- inspect .55   .56   20    .037 0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .21 .21 33 2.4 1.0  0      true -32 wit inspect 3.9  2.2  250 0     0   false(unreach-call) 1 --- inspect 14     8.5   310   .71 0   unknown 0 --- inspect 3.5  2.0  240 0   0   false(unreach-call) 1 --- inspect .60   .59   20    .053 0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .21 .21 34 2.8 .85 0      true -32 wit inspect 4.5  2.5  250 0     0   false(unreach-call) 1 --- inspect 14     8.5   300   .71 0   unknown 0 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .45 .45 36 4.9 1.0  0      false(unreach-call) 1 wit inspect 4.4  2.5  260 0     0   false(unreach-call) 1 --- inspect 13     7.7   300   .75 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 .0041 - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c unknown 0 --- inspect 890    900    300 13000   110    0      error (invalid witness file) 0 --- inspect .59 .37 40 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 48 0   0   error (invalid witness file) 0 --- inspect .0049 .0065 .53 0     0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c unknown 0 wit inspect 88    88    15000 960   31    0      unknown 0 wit inspect 17    15    530 .016 0   timeout 0 --- inspect 97     89     800   1.5  0   unknown 0 --- inspect .99 .64 50 0   0   error (1) 0 --- inspect .068  .067  12    0     0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 .37 36 5.2 .85 0      false(unreach-call) 1 wit inspect 4.2  2.4  260 0     0   false(unreach-call) 1 --- inspect 14     8.9   300   .71 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 .14 33 1.6 1.0  0      false(unreach-call) 1 wit inspect 3.8  2.1  250 0     0   false(unreach-call) 1 --- inspect 13     7.9   300   .68 0   unknown 0 --- inspect 3.6  2.1  250 0   0   error (2) 0 --- inspect .56   .56   20    .037 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13 .13 33 1.7 .85 0      false(unreach-call) 1 wit inspect 3.6  2.0  250 0     0   false(unreach-call) 1 --- inspect 13     7.7   300   .71 0   unknown 0 --- inspect 3.6  2.2  250 0   0   error (2) 0 --- inspect .55   .55   20    .037 0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.2  9.2  110 110   1.0  0      false(unreach-call) 1 wit inspect 6.8  4.1  330 0     0   false(unreach-call) 1 --- inspect 31     22     1000   .68 0   false(unreach-call) 1 --- inspect 4.5  2.5  270 0   0   false(unreach-call) 1 --- inspect .65   .65   20    .082 0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 58    58    150 840   .85 0      true -32 wit inspect 3.9  2.2  250 0     0   false(unreach-call) 1 --- inspect 25     19     610   .68 0   unknown 0 --- inspect 4.6  2.6  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .057 0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c unknown 0 wit inspect .99 .72 67 13   52    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1500 0     0   timeout 0 --- inspect 960     910     2600   .69 0  
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c unknown 0 --- inspect 900    900    1200 11000   290    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0  
float-benchs/Rump_double_true-unreach-call_true-termination.c unknown 0 wit inspect .78 .53 65 8.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0     0   true 2 --- inspect 32     26     1000   .71 0  
float-benchs/Rump_float_true-unreach-call_true-termination.c unknown 0 wit inspect .80 .53 67 8.9 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0     0   true 2 --- inspect 16     11     430   .75 0  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c unknown 0 wit inspect .80 .55 65 9.5 26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0     0   true 2 --- inspect 13     7.7   300   .75 0  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c unknown 0 wit inspect .78 .53 65 8.5 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0     0   true 2 --- inspect 13     8.0   300   .71 0  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c unknown 0 wit inspect .79 .54 66 8.8 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0     0   true 2 --- inspect 13     7.6   300   .75 0  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c unknown 0 wit inspect 780    780    510 8900   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    34    500 0     0   error (7) 0 --- inspect 130     130     2600   .71 0  
float-benchs/bary_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 890    900    200 11000   270    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0  
float-benchs/cast_float_union_true-unreach-call.c unknown 0 wit inspect .79 .53 67 9.5 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.4  270 0     0   true 2 --- inspect 6.7   4.2   300   .66 0  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c unknown 0 wit inspect 350    350    240 4900   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1200 0     0   timeout 0 --- inspect 960     950     3000   .71 0  
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 900    900    330 12000   870    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0     0   error (2) 0 --- inspect .021 .023 5.6 0    0  
float-benchs/divmul_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 900    900    330 11000   840    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 42 0     0   error (2) 0 --- inspect .022 .022 5.6 0    0  
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c unknown 0 wit inspect 9.5  9.2  67 120   300    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    23    410 0     0   true 2 --- inspect 320     310     640   .68 0  
float-benchs/drift_tenth_true-unreach-call_true-termination.c unknown 0 wit inspect 9.4  9.1  67 130   300    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    22    400 0     0   true 2 --- inspect 360     340     700   .68 0  
float-benchs/exp_loop_true-unreach-call.c unknown 0 wit inspect 670    670    300 8400   980    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 820    810    7000 0     0   timeout 0 --- inspect 960     950     1300   .69 0  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 900    900    250 11000   660    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0     0   error (2) 0 --- inspect .023 .025 5.6 0    0  
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c unknown 0 --- inspect 900    900    580 10000   260    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0     0   error (2) 0 --- inspect .022 .026 5.6 0    0  
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c out of memory 0 wit inspect 320    320    15000 3800   62    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 15    12    460 0     0   true 2 --- inspect 650     630     890   .71 0  
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c out of memory 0 wit inspect 340    340    15000 4300   62    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 13    11    450 0     0   true 2 --- inspect 480     470     910   .71 0  
float-benchs/filter1_true-unreach-call_true-termination.c unknown 0 wit inspect 900    900    680 12000   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.3  7.0  410 0     0   true 2 --- inspect 100     96     600   .71 0  
float-benchs/filter2_alt_true-unreach-call.c unknown 0 --- inspect 900    900    240 12000   110    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0     0   error (2) 0 --- inspect .020 .022 5.7 0    0  
float-benchs/filter2_iterated_true-unreach-call.c unknown 0 --- inspect 900    900    750 11000   21    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0     0   error (2) 0 --- inspect .021 .023 5.6 0    0  
float-benchs/filter2_reinit_true-unreach-call_true-termination.c unknown 0 --- inspect 890    900    390 11000   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0     0   error (2) 0 --- inspect .025 .026 5.7 0    0  
float-benchs/filter2_set_true-unreach-call_true-termination.c unknown 0 --- inspect 900    900    310 10000   21    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0     0   error (2) 0 --- inspect .024 .025 5.6 0    0  
float-benchs/filter2_true-unreach-call_true-termination.c unknown 0 --- inspect 900    900    310 9400   41    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0     0   error (2) 0 --- inspect .020 .021 5.6 0    0  
float-benchs/filter_iir_true-unreach-call.c unknown 0 --- inspect 900    900    480 9600   21    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0     0   error (2) 0 --- inspect .025 .026 5.6 0    0  
float-benchs/float_double_true-unreach-call_true-termination.c unknown 0 wit inspect .80 .54 66 8.9 26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0     0   true 2 --- inspect 12     7.6   300   .71 0  
float-benchs/image_filter_true-unreach-call.c unknown 0 wit inspect 900    900    510 10000   31    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 66    62    7000 0     0   timeout 0 --- inspect 960     950     1200   .63 0  
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c unknown 0 wit inspect 2.5  2.3  67 30   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 890    890    630 0     0   timeout 0 --- inspect 960     950     1600   .68 0  
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c unknown 0 wit inspect 9.2  8.9  100 100   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 75    72    570 0     0   timeout 0 --- inspect 960     950     1600   1.0  0  
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c unknown 0 wit inspect 2.6  2.4  67 33   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 42    40    450 0     0   timeout 0 --- inspect 960     950     1600   .72 0  
float-benchs/interpolation2_true-unreach-call_true-termination.c unknown 0 wit inspect 5.3  5.0  68 64   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 45    42    550 0     0   timeout 0 --- inspect 960     950     1600   .68 0  
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c unknown 0 wit inspect 1.9  1.6  67 24   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    29    480 0     0   timeout 0 --- inspect 960     950     1500   1.1  0  
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c unknown 0 wit inspect 4.2  3.9  79 55   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 84    82    480 0     0   timeout 0 --- inspect 960     950     1400   1.1  0  
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c unknown 0 wit inspect 2.0  1.7  67 24   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 30    27    400 0     0   timeout 0 --- inspect 960     950     1500   .68 0  
float-benchs/interpolation_true-unreach-call_true-termination.c unknown 0 wit inspect 2.1  1.8  67 26   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    20    470 0     0   timeout 0 --- inspect 960     950     1900   .72 0  
float-benchs/inv_Newton_true-unreach-call.c unknown 0 --- inspect 900    900    280 13000   110    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0     0   error (2) 0 --- inspect .022 .022 5.6 0    0  
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c unknown 0 wit inspect 9.7  9.4  65 110   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.2  4.5  310 0     0   true 2 --- inspect 85     78     790   .71 0  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c unknown 0 wit inspect 3.9  3.6  66 43   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.9  280 0     0   true 2 --- inspect 72     66     510   .71 0  
float-benchs/inv_square_int_true-unreach-call_true-termination.c unknown