Tool VeriFuzz 1.0.0 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-09 02:47:33 CET 2018-12-09 17:43:44 CET 2018-12-09 18:26:53 CET 2018-12-09 18:31:36 CET 2018-12-12 22:04:17 CET 2018-12-09 17:35:51 CET 2018-12-09 18:23:50 CET
Run set verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-verifuzz.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/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/verifuzz.2018-12-09_0247.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/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/verifuzz.2018-12-09_0247.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 15   14   150 170 .61  .0082 false(unreach-call) 1 wit inspect 83    81    350 0   0      true -32 --- inspect 6.4   3.6   310   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  250 0     0      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 6.0 4.8 150 66 .61  .0082 false(unreach-call) 1 wit inspect 60    58    360 0   .15   true -32 --- inspect 6.8   3.8   300   .62 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_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 8.8 7.5 150 84 .61  .016  false(unreach-call) 1 wit inspect 49    48    360 0   .18   true -32 --- inspect 6.7   3.8   300   .66 0      false(unreach-call) 1 --- inspect 3.5  2.0  240 0     0      false(unreach-call) 1 --- inspect .58   .59   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 11   9.5 150 140 .61  .0082 false(unreach-call) 1 wit inspect 24    23    350 0   0      true -32 --- inspect 6.6   4.2   300   .62 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.9 5.6 150 83 .61  .0082 false(unreach-call) 1 wit inspect 17    15    340 0   0      true -32 --- inspect 7.4   4.2   300   .62 0      false(unreach-call) 1 --- inspect 4.4  2.5  250 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 60   59   150 890 .61  .0082 timeout 0 wit inspect 92    90    450 0   0      true -32 --- inspect 6.3   4.0   300   .62 0      false(unreach-call) 1 --- inspect 3.7  2.1  250 0     .029  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 24   23   150 310 .61  .0082 false(unreach-call) 1 wit inspect 89    88    440 0   0      true -32 --- inspect 6.8   3.8   310   .66 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_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19   18   200 200 .61  48      false(unreach-call) 1 wit inspect 49    47    440 0   .13   true -32 --- inspect 6.3   4.0   300   .66 0      false(unreach-call) 1 --- inspect 3.8  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 74   73   220 750 .61  .0082 timeout 0 wit inspect 92    90    550 0   0      true -32 --- inspect 6.7   4.2   300   .62 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0     0      false(unreach-call) 1 --- inspect .63   .63   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 67   65   230 570 .61  .053  timeout 0 wit inspect 92    90    550 0   .0041 true -32 --- inspect 6.8   4.3   300   .62 0      false(unreach-call) 1 --- inspect 3.5  2.1  240 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 37   36   200 320 .61  .025  timeout 0 wit inspect 92    90    560 0   .15   true -32 --- inspect 6.8   3.8   300   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0     .029  false(unreach-call) 1 --- inspect .60   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.4 6.1 150 77 .60  .0082 false(unreach-call) 1 wit inspect 12    10    320 0   0      timeout 0 --- inspect 97     91     620   1.5  0      false(unreach-call) 1 --- inspect 3.5  2.0  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .049 .0041 - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.5 3.1 150 47 .59  .0082 false(unreach-call) 1 wit inspect 56    54    340 0   0      timeout 0 --- inspect 97     92     570   .68 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/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.3 5.0 150 67 .60  .0082 timeout 0 wit inspect 92    90    380 0   0      timeout 0 --- inspect 97     92     610   .72 0      false(unreach-call) 1 --- inspect 3.6  2.1  240 0     .22   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.4 6.1 150 94 .59  .0082 false(unreach-call) 1 wit inspect 25    23    330 0   0      false(unreach-call) 1 --- inspect 82     77     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 76   77   150 1000 .62  .53   timeout 0 wit inspect 91    90    370 0   0      false(unreach-call) 1 --- inspect 89     84     450   .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
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.2 8.1 150 120 .59  .012  false(unreach-call) 1 wit inspect 67    65    340 0   0      timeout 0 --- inspect 97     91     470   1.6  0      false(unreach-call) 1 --- inspect 3.5  2.0  250 0     0      false(unreach-call) 1 --- inspect .58   .58   20    .049 .0041 - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 11000 .64  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0    
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 12000 .47  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 10000 .70  .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0    
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 10000 .68  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 10000 .69  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0    
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 12000 .68  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .44 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 11000 .64  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.7 0   0    
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 11000 .62  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0   0    
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   230 12000 .59  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .96 .58 41 0   0   error (2) 0 --- inspect .019 .020 5.8 0   0    
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   230 12000 .68  .033  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   270 10000 .62  45      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   240 9900 .68  .041  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0    
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i error (1) 0 --- inspect 870   880   230 10000 .67  .033  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cdfpl/sine_4_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 12000 .67  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 40 0   0   error (2) 0 --- inspect .045 .046 5.5 0   0    
floats-cdfpl/sine_5_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 10000 .71  .074  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0    
floats-cdfpl/sine_6_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 10000 .66  .041  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0    
floats-cdfpl/sine_7_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 12000 .68  .62   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cdfpl/sine_8_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 11000 .64  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0   0    
floats-cdfpl/square_4_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 10000 .71  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cdfpl/square_5_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 11000 .67  .033  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cdfpl/square_6_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 12000 .57  .033  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cdfpl/square_7_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 12000 .67  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cdfpl/square_8_true-unreach-call_true-termination.i error (1) 0 --- inspect 860   880   150 10000 .68  .070  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float-div1_true-unreach-call.i timeout 0 --- inspect 900   920   180 11000 .61  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i timeout 0 --- inspect 900   920   180 13000 .54  .27   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 10000 .84  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .42 42 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0    
floats-cbmc-regression/float-no-simp2_true-unreach-call.i error (1) 0 --- inspect 870   880   180 12000 .27  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 11000 .80  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0    
floats-cbmc-regression/float-no-simp4_true-unreach-call.i timeout 0 --- inspect 900   920   180 11000 .41  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 12000 .69  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .43 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 12000 .82  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float-no-simp8_true-unreach-call.i timeout 0 --- inspect 900   920   170 13000 .59  .033  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float-rounding1_true-unreach-call.i timeout 0 --- inspect 900   920   180 12000 .62  .045  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float-to-double1_true-unreach-call.i timeout 0 --- inspect 900   920   180 11000 .60  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 10000 .83  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 12000 .72  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .51 43 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float11_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   200 11000 .84  46      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float12_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 11000 .79  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float13_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 13000 .84  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .39 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float14_true-unreach-call.i timeout 0 --- inspect 900   920   190 12000 .63  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0    
floats-cbmc-regression/float18_true-unreach-call.i timeout 0 --- inspect 900   920   180 13000 .64  .49   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0    
floats-cbmc-regression/float19_true-unreach-call.i timeout 0 --- inspect 900   920   180 12000 .69  .029  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float1_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 11000 .88  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float20_true-unreach-call_true-termination.i timeout 0 --- inspect 900   900   150 9300 .67  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float21_true-unreach-call.i timeout 0 --- inspect 900   920   180 13000 .61  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float22_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 12000 .87  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0    
floats-cbmc-regression/float2_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 11000 .81  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0    
floats-cbmc-regression/float3_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 11000 .84  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float4_true-unreach-call.i error (1) 0 --- inspect 860   880   180 11000 .50  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .45 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
floats-cbmc-regression/float5_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 9800 .81  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float6_true-unreach-call_true-termination.i timeout 0 --- inspect 900   920   150 13000 .78  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float8_true-unreach-call.i timeout 0 --- inspect 900   920   180 12000 .52  .029  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   .029
floats-cbmc-regression/float_lib1_true-unreach-call.i timeout 0 --- inspect 900   920   180 12000 .59  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
floats-cbmc-regression/float_lib2_true-unreach-call.i timeout 0 --- inspect 900   920   180 11000 .32  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.7 2.4 150 35 .67  0      false(unreach-call) 1 wit inspect 4.1  2.3  260 0   0      false(unreach-call) 1 --- inspect 15     9.4   310   .68 0      unknown 0 --- inspect 3.7  2.1  240 0     0      error (2) 0 --- inspect .56   .58   20    .037 0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.8 2.2 150 38 .69  0      false(unreach-call) 1 wit inspect 4.0  2.3  260 0   0      false(unreach-call) 1 --- inspect 13     7.6   300   .75 0      false(unreach-call) 1 --- inspect 4.0  2.3  250 0     0      false(unreach-call) 1 --- inspect .59   .59   20    .053 0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 2.1 150 33 .59  0      false(unreach-call) 1 wit inspect 4.1  2.4  260 0   0      false(unreach-call) 1 --- inspect 14     7.8   310   .75 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 2.2 150 39 .66  0      false(unreach-call) 1 wit inspect 3.8  2.2  260 0   0      false(unreach-call) 1 --- inspect 13     8.1   300   .71 0      false(unreach-call) 1 --- inspect 3.5  2.0  250 0     0      false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c false(unreach-call) 1 wit inspect 27   26   150 350 .63  .0082 false(unreach-call) 1 wit inspect 6.8  5.0  340 0   0      true -32 --- inspect 7.0   4.3   300   .66 0      false(unreach-call) 1 --- inspect 3.8  2.2  240 0     0      false(unreach-call) 1 --- inspect .58   .58   20    .057 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c false(unreach-call) 1 wit inspect 11   10   150 140 .68  .0082 false(unreach-call) 1 wit inspect 6.4  4.6  340 0   0      true -32 --- inspect 7.5   4.2   310   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0     0      false(unreach-call) 1 --- inspect .60   .60   20    .057 0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .79  0      error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .92 .59 47 0     0      error (invalid witness file) 0 --- inspect .0049 .0062 .50 0     0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 2.3 150 39 .59  0      false(unreach-call) 1 wit inspect 3.7  2.0  250 0   .14   false(unreach-call) 1 --- inspect 12     7.2   300   .71 0      unknown 0 --- inspect 3.3  2.0  250 0     0      error (2) 0 --- inspect .57   .57   20    .037 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.7 2.5 200 35 .70  46      false(unreach-call) 1 wit inspect 3.6  2.0  250 0   0      false(unreach-call) 1 --- inspect 12     7.2   290   .71 6.6    unknown 0 --- inspect 3.7  2.2  250 0     0      error (2) 0 --- inspect .58   .58   20    .037 0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.0 5.3 280 71 .78  .086  false(unreach-call) 1 wit inspect 6.3  4.0  320 0   0      true -32 --- inspect 8.3   4.5   320   .66 0      false(unreach-call) 1 --- inspect 4.4  2.5  270 0     .0082 false(unreach-call) 1 --- inspect .59   .60   20    .082 0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 4.1 2.6 150 38 .61  .078  false(unreach-call) 1 wit inspect 13    11    420 0   0      true -32 --- inspect 7.0   4.4   300   .66 .0041 false(unreach-call) 1 --- inspect 3.9  2.2  250 0     0      false(unreach-call) 1 --- inspect .62   .62   20    .057 0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   920   150 11000 .82  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 13000 .69  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .46 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0    
float-benchs/Rump_double_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .82  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/Rump_float_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 10000 .84  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 13000 .79  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 12000 .85  .041  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 13000 .74  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/arctan_Pade_true-unreach-call_true-termination.c error (1) 0 --- inspect 870   880   260 12000 .53  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .45 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 13000 1.2   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0    
float-benchs/cast_float_union_true-unreach-call.c timeout 0 --- inspect 900   920   150 12000 .86  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/cos_polynomial_true-unreach-call_true-termination.c error (1) 0 --- inspect 860   880   150 12000 .75  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c error (1) 0 --- inspect 860   880   150 12000 .93  .029  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/divmul_diverge_true-unreach-call_true-termination.c error (1) 0 --- inspect 860   880   150 11000 .94  .070  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 40 0   0   error (2) 0 --- inspect .020 .021 5.8 0   0    
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   920   150 14000 .79  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 42 0   0   error (2) 0 --- inspect .020 .021 5.7 0   0    
float-benchs/drift_tenth_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .88  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0    
float-benchs/exp_loop_true-unreach-call.c timeout 0 --- inspect 900   920   150 10000 .84  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0    
float-benchs/feedback_diverge_true-unreach-call_true-termination.c error (1) 0 --- inspect 860   880   150 11000 .95  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   920   150 10000 .91  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c timeout 0 --- inspect 900   920   160 11000 1.0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 900   920   160 11000 1.0   .074  - --- 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    
float-benchs/filter1_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 1.1   .41   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0    
float-benchs/filter2_alt_true-unreach-call.c timeout 0 --- inspect 900   920   160 11000 .93  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/filter2_iterated_true-unreach-call.c error (1) 0 --- inspect 7.5 6.2 150 96 .41  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 43 0   0   error (2) 0 --- inspect .020 .021 5.7 0   0    
float-benchs/filter2_reinit_true-unreach-call_true-termination.c error (1) 0 --- inspect 860   880   150 12000 .93  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/filter2_set_true-unreach-call_true-termination.c error (1) 0 --- inspect 860   880   150 11000 .59  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/filter2_true-unreach-call_true-termination.c error (1) 0 --- inspect 860   880   150 12000 .82  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0   error (2) 0 --- inspect .032 .033 5.5 0   0    
float-benchs/filter_iir_true-unreach-call.c error (1) 0 --- inspect 860   880   210 9600 .84  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/float_double_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .76  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0   error (2) 0 --- inspect .021 .022 5.5 0   0    
float-benchs/image_filter_true-unreach-call.c error (1) 0 --- inspect 870   880   400 9600 .79  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   920   160 12000 .78  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c timeout 0 --- inspect 900   920   160 14000 .80  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0   error (2) 0 --- inspect .020 .022 5.6 0   0    
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 900   920   160 11000 .84  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/interpolation2_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .78  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   920   160 12000 .82  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c timeout 0 --- inspect 900   930   150 11000 .77  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0    
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 900   920   160 11000 .74  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/interpolation_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   200 11000 .82  45      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/inv_Newton_true-unreach-call.c timeout 0 --- inspect 900   920   150 11000 .84  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .44 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c timeout 0 --- inspect 900   920   150 14000 .85  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c error (1) 0 --- inspect 860   880   150 11000 .75  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0   0    
float-benchs/inv_square_int_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .79  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0    
float-benchs/inv_square_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .79  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0    
float-benchs/loop_true-unreach-call.c timeout 0 --- inspect 900   900   150 11000 .54  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0    
float-benchs/mea8000_true-unreach-call.c error (1) 0 --- inspect 4.5 2.6 160 45 .32  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0    
float-benchs/nan_double_range_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 12000 .81  0      - --- inspect - --- inspect - --- inspect - ---