Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [apollon004; apollon069; apollon137; apollon154] 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-06 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 02:16:29 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options -s kinduction -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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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 25     25     93 350    .85 0   false(unreach-call) 1 wit inspect 51    49    350 0     0   false(unreach-call) 1 --- inspect 35     29     680   .68 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .053 .0041 - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 33     33     93 440    .85 0   false(unreach-call) 1 wit inspect 12    10    350 0     0   timeout 0 --- inspect 97     91     700   1.8  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_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 41     41     92 520    1.0  0   false(unreach-call) 1 wit inspect 41    39    350 0     0   false(unreach-call) 1 --- inspect 70     65     700   .68 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    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 8.8   8.8   92 120    1.0  0   false(unreach-call) 1 wit inspect 12    9.8  350 0     0   timeout 0 --- inspect 97     91     700   1.7  0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 39     39     91 460    1.0  0   false(unreach-call) 1 wit inspect 11    9.5  350 0     0   false(unreach-call) 1 --- inspect 26     21     680   .71 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 130     130     190 1700    1.0  0   true -32 wit inspect 4.6  2.6  250 0     0   timeout 0 --- inspect 97     91     790   2.3  0   false(unreach-call) 1 --- inspect 3.6  2.2  240 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     190 1400    .85 0   true -32 wit inspect 4.1  2.3  250 0     0   timeout 0 --- inspect 97     90     800   1.9  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
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 61     61     190 730    1.0  0   true -32 wit inspect 4.0  2.2  250 0     0   false(unreach-call) 1 --- inspect 38     32     820   .68 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .59   .59   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 100     100     290 1400    .85 0   true -32 wit inspect 4.3  2.4  250 0     0   timeout 0 --- inspect 97     91     880   1.7  0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0    false(unreach-call) 1 --- inspect .61   .61   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 1500    1.0  0   true -32 wit inspect 4.3  2.4  250 0     0   false(unreach-call) 1 --- inspect 55     49     910   .68 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_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 130     130     300 1600    1.0  0   true -32 wit inspect 4.5  2.5  250 0     0   timeout 0 --- inspect 97     90     930   1.9  0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .61   .61   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 20     20     64 280    1.0  0   true -32 wit inspect 4.0  2.2  250 0     0   timeout 0 --- inspect 97     91     590   1.0  0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 20     20     64 300    .85 0   true -32 wit inspect 3.5  2.0  250 0     0   timeout 0 --- inspect 97     92     580   .98 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
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19     19     64 240    1.0  0   true -32 wit inspect 4.2  2.4  250 0     0   timeout 0 --- inspect 97     92     600   2.1  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
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.7   4.7   57 55    .85 0   true -32 wit inspect 3.7  2.1  250 0     0   timeout (false(unreach-call)) 0 --- inspect 96     90     460   .68 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0    false(unreach-call) 1 --- inspect .61   .61   20    .049 .0041 - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.8   6.8   55 78    1.0  0   true -32 wit inspect 4.0  2.2  250 0     0   timeout 0 --- inspect 97     91     440   1.7  0   false(unreach-call) 1 --- inspect 3.5  2.1  240 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.5   7.5   55 95    1.0  0   true -32 wit inspect 3.9  2.1  250 0     0   timeout 0 --- inspect 97     91     470   1.6  0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 2 wit inspect 36     36     93 480    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0     timeout 0 --- inspect 960     950     950   .75 0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 2 wit inspect 39     39     94 570    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0     timeout 0 --- inspect 960     950     780   .72 0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 2 wit inspect 44     44     93 650    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    570 0   0     timeout 0 --- inspect 960     950     970   .73 0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 2 wit inspect 160     160     190 1900    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    520 0   0     timeout 0 --- inspect 960     950     900   .70 0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 2 wit inspect 170     170     190 2000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    810 0   0     timeout 0 --- inspect 960     950     970   .74 0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 2 wit inspect 160     160     190 1800    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    520 0   0     timeout 0 --- inspect 960     950     990   .78 0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 2 wit inspect 160     160     190 2100    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0     timeout 0 --- inspect 960     950     1000   .73 0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i true 2 wit inspect 180     180     190 2100    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    530 0   0     timeout 0 --- inspect 960     950     880   .73 0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i true 2 wit inspect 450     450     290 5100    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    590 0   0     timeout 0 --- inspect 960     950     1100   2.0  0     
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 2 wit inspect 700     700     300 11000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0     timeout 0 --- inspect 960     950     1000   1.6  0     
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i true 2 wit inspect 460     460     300 6500    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    680 0   0     timeout 0 --- inspect 960     950     1100   .72 0     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i true 2 wit inspect 630     630     300 7000    .85 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 true 2 wit inspect 620     620     310 6000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0     timeout 0 --- inspect 960     950     1000   1.9  0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i true 2 wit inspect 34     34     64 450    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    500 0   0     timeout 0 --- inspect 960     950     790   .81 0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 2 wit inspect 17     17     64 220    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    490 0   0     timeout 0 --- inspect 960     950     830   .73 0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 20     20     64 300    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    650 0   0     timeout 0 --- inspect 960     950     820   1.8  0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 14     14     64 150    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 790    790    590 0   0     timeout 0 --- inspect 960     950     850   .71 0     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 17     17     63 220    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 570    570    540 0   0     timeout 0 --- inspect 960     950     810   .74 0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 29     29     57 330    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 680    680    570 0   0     timeout 0 --- inspect 960     950     670   1.8  0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 13     13     59 180    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 530    530    510 0   0     timeout 0 --- inspect 960     950     760   1.4  0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 12     12     55 180    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 290    280    500 0   0     timeout 0 --- inspect 960     950     760   1.7  0     
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 7.1   7.1   61 110    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    480 0   0     true 2 --- inspect 620     620     780   .71 0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 5.5   5.5   62 71    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 67    65    360 0   0     true 2 --- inspect 83     78     610   .71 0     
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 3.2   3.2   68 42    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.9  3.7  320 0   0     true 2 --- inspect 44     38     950   .68 0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect .14  .14  28 1.5  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    8.8  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 .075 .076 26 .90 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0     true 2 --- inspect 15     9.1   300   .75 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 1.8   1.8   36 27    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    17    300 0   0     true 2 --- inspect 57     48     530   .71 0     
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect .080 .082 26 1.1  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0     true 2 --- inspect 13     7.4   300   .75 0     
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect .14  .14  27 1.4  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  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 .10  .10  26 .79 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.1  250 0   0     true 2 --- inspect 17     10     300   .75 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect .085 .085 26 .74 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0     true 2 --- inspect 16     9.7   300   .75 0     
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .087 .087 26 .88 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   .033 error (7) 0 --- inspect 16     8.8   290   .75 0     
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .14  .14  27 1.6  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 4.8  2.6  260 0   0     unknown 0 --- inspect 6.4   3.5   280   .65 0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .28  .28  27 3.1  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  3.0  260 0   0     true 2 --- inspect 36     28     460   .71 0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect .094 .097 26 .71 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0     true 2 --- inspect 12     7.2   300   .75 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect .085 .087 26 .86 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  250 0   0     true 2 --- inspect 19     11     300   .75 0     
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect .095 .096 26 .97 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0     true 2 --- inspect 15     8.9   300   .75 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect .20  .20  26 2.6  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0     true 2 --- inspect 20     14     300   .75 0     
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect .081 .082 26 .80 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  250 0   0     true 2 --- inspect 16     9.6   300   .75 0     
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .092 .092 26 .96 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.5  3.1  260 0   0     true 2 --- inspect 16     9.0   390   .68 0     
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 270     270     1200 3100    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 48    41    610 0   0     error (7) 0 --- inspect 11     6.7   290   .75 0     
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .16  .16  26 1.8  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  3.0  260 0   0     true 2 --- inspect 18     11     390   .75 0     
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect .081 .081 26 .78 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0     true 2 --- inspect 14     8.6   300   .75 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect .13  .13  30 1.4  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0     true 2 --- inspect 25     18     380   .75 0     
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect .32  .33  27 3.5  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.3  6.9  290 0   0     true 2 --- inspect 68     60     580   .71 0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect .19  .19  26 1.9  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.9  270 0   0     true 2 --- inspect 220     200     740   .68 0     
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect .10  .10  26 1.1  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0     true 2 --- inspect 15     8.5   310   .68 0     
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect .10  .11  26 .81 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  270 0   0     true 2 --- inspect 16     11     320   .75 0     
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect .83  .83  31 10    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 88    85    330 0   0     true 2 --- inspect 93     85     570   .71 0     
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect .28  .28  27 3.5  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  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 .096 .096 26 1.0  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.2  260 0   0     true 2 --- inspect 15     8.9   310   .75 0     
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect .11  .11  26 1.0  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.4  7.0  270 0   0     true 2 --- inspect 19     11     390   .75 0     
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect .54  .54  27 7.0  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.8  3.1  260 0   0     error (7) 0 --- inspect 13     7.7   290   .75 0     
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect .097 .098 27 1.1  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  2.9  250 0   0     true 2 --- inspect 22     12     420   .71 0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .094 .095 26 1.0  .85 0   true -32 wit inspect 4.1  2.2  250 0     0   false(unreach-call) 1 --- inspect 18     11     300   .68 0   unknown 0 --- inspect 3.4  1.9  250 0   0    error (2) 0 --- inspect .58   .58   20    .037 0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17  .17  26 1.6  1.0  0   true -32 wit inspect 4.0  2.3  250 0     0   false(unreach-call) 1 --- inspect 14     8.7   310   .68 0   unknown 0 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15  .16  27 1.7  .85 0   true -32 wit inspect 4.3  2.3  250 0     0   false(unreach-call) 1 --- inspect 14     8.6   320   .68 0   unknown 0 --- inspect 4.7  2.6  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36  .36  28 5.4  1.0  0   false(unreach-call) 1 wit inspect 4.2  2.4  260 0     0   false(unreach-call) 1 --- inspect 14     8.4   300   .71 0   false(unreach-call) 1 --- inspect 3.6  2.1  240 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 --- inspect 900     900     300 7600    1.0  0   error (invalid witness file) 0 --- inspect .75 .46 41 0     0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 48 0   0    error (invalid witness file) 0 --- inspect .0056 .0073 .53 0     0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c true -32 wit inspect 450     450     530 4300    .85 0   unknown 0 wit inspect 19    16    530 .016 0   timeout 0 --- inspect 97     89     780   1.9  0   unknown 0 --- inspect 1.0  .66 50 0   0    error (1) 0 --- inspect .079  .079  11    0     0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .30  .30  28 3.9  1.0  0   false(unreach-call) 1 wit inspect 4.6  2.6  260 0     0   false(unreach-call) 1 --- inspect 14     8.8   300   .71 0   false(unreach-call) 1 --- inspect 4.3  2.6  240 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .083 .085 26 .97 1.0  0   false(unreach-call) 1 wit inspect 4.0  2.3  250 0     0   false(unreach-call) 1 --- inspect 13     7.7   300   .71 0   unknown 0 --- inspect 3.5  2.0  250 0   0    error (2) 0 --- inspect .55   .55   20    .037 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .076 .077 26 .93 1.0  0   false(unreach-call) 1 wit inspect 4.4  2.4  260 0     0   false(unreach-call) 1 --- inspect 13     8.2   300   .71 0   unknown 0 --- inspect 3.5  2.1  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   100 120    .85 0   false(unreach-call) 1 wit inspect 6.3  4.0  310 0     0   false(unreach-call) 1 --- inspect 33     24     1000   .68 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0    false(unreach-call) 1 --- inspect .59   .59   20    .082 0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 58     58     150 800    1.0  0   true -32 wit inspect 4.6  2.5  270 0     0   false(unreach-call) 1 --- inspect 24     18     600   .68 0   unknown 0 --- inspect 4.2  2.3  250 0   0    false(unreach-call) 1 --- inspect .60   .59   20    .057 0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .10  .10  26 .81 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1500 0   0     timeout 0 --- inspect 960     900     2500   1.5  0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect 21     21     260 280    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1600 0   0     timeout 0 --- inspect 960     900     4400   .70 0     
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect .087 .087 26 .90 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.3  250 0   0     true 2 --- inspect 33     27     1000   .71 0     
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect .10  .11  26 .83 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0     true 2 --- inspect 18     12     430   .75 0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect .085 .086 26 .98 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0     true 2 --- inspect 16     10     290   .75 0     
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect .098 .10  26 1.5  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0     true 2 --- inspect 15     8.9   300   .75 0     
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect .075 .076 26 .75 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  250 0   0     true 2 --- inspect 14     7.8   300   .75 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 250     250     490 3100    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    31    500 0   0     error (7) 0 --- inspect 130     120     2600   .71 0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     330 12000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0     error (2) 0 --- inspect .028 .030 5.6 0    0     
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .11  .11  26 .78 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0     true 2 --- inspect 9.1   5.2   310   .66 0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 2 wit inspect 120     120     240 1400    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1300 0   0     timeout 0 --- inspect 960     950     2900   .72 0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     5200 10000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .51 41 0   0     error (2) 0 --- inspect .023 .024 5.7 0    0     
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     8300 11000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .51 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 .42  .42  30 5.2  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    25    410 0   0     true 2 --- inspect 350     330     650   .71 0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect .43  .43  29 4.9  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 29    26    410 0   0     true 2 --- inspect 300     280     610   .71 0     
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 12     12     67 170    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 820    800    7000 0   0     timeout 0 --- inspect 960     950     1300   1.8  0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     8400 8900    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 41 0   0     error (2) 0 --- inspect .027 .029 5.7 0    0     
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900     900     1100 10000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0     error (2) 0 --- inspect .022 .024 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c true 2 wit inspect 56     56     140 780    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 13    11    450 0   0     true 2 --- inspect 600     590     930   .68 0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 59     59     140 740    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 13    11    450 0   0     true 2 --- inspect 760     750     970   .71 0     
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 50     50     100 760    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.2  6.8  400 0   0     true 2 --- inspect 110     99     610   .71 0     
float-benchs/filter2_alt_true-unreach-call.c timeout 0 --- inspect 900     900     250 10000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .38 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0     
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 --- inspect 900     900     1100 12000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0     error (2) 0 --- inspect .021 .023 5.6 0    0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     400 12000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .50 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     380 8800    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     350 12000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0    0     
float-benchs/filter_iir_true-unreach-call.c timeout 0 --- inspect 900     900     560 12000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect .076 .077 26 .68 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0     true 2 --- inspect 14     8.3   290   .75 0     
float-benchs/image_filter_true-unreach-call.c timeout 0 --- inspect 900     900     1900 9300    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 40 0   0     error (2) 0 --- inspect .024 .025 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 3.0   3.0   49 39    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    640 0   0     timeout 0 --- inspect 960     950     1500   .74 0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 3.1   3.1   50 48    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 84    80    570 0   0     timeout 0 --- inspect 960     950     1600   .74 0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 2.6   2.6   59 32    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 42    40    450 0   0     timeout 0 --- inspect 960     950     1600   .79 0     
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect 4.2   4.2   45 47    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 48    45    560 0   0     timeout 0 --- inspect 960     950     1500   .71 0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 2.0   2.0   41 29    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 47    44    470 0   0     timeout 0 --- inspect 960     950     1400   .72 0     
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 2.0   2.0   41 29    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 84    81    480 0   0     timeout 0 --- inspect 960     950     1500   .71 0     
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 1.7   1.7   48 26    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    28    400 0   0     timeout 0 --- inspect 960     950     1400   .72 0     
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect 2.2   2.2   39 33    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    24    470 0   0     timeout 0 --- inspect 960     950     1600   .72 0     
float-benchs/inv_Newton_true-unreach-call.c timeout 0 --- inspect 900     900     300 10000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .43 41 0   0     error (2) 0 --- inspect .026 .028 5.6 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 4.5   4.5   48 58    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.8  5.7  310 0   0     true 2 --- inspect 85     78     790   .71 0     
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect 1.1   1.1   40 14    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect