Tool ULTIMATE Taipan 0.1.23-635dfa2a 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-08 14:19:36 CET 2018-12-09 20:52:23 CET 2018-12-09 21:15:16 CET 2018-12-09 21:17:48 CET 2018-12-12 21:23:28 CET 2018-12-09 20:12:13 CET 2018-12-09 20:55:36 CET
Run set utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options --full-output -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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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 32   24   700 270 .74 0      false(unreach-call) 1 wit inspect 49    47    350 0   0      false(unreach-call) 1 --- inspect 35     30     680   .68 .0041 unknown 0 --- inspect 4.2  2.4  250 0   0      true -32 --- inspect .57   .64   20    .053  .0041 - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 91   84   720 760 .71 0      false(unreach-call) 1 wit inspect 11    9.0  350 0   0      timeout (false(unreach-call)) 0 --- inspect 94     88     710   .68 .0041 unknown 0 --- inspect 5.0  2.8  250 0   0      true -32 --- inspect .58   .58   20    .053  .0041 - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 64   56   710 490 .71 0      false(unreach-call) 1 wit inspect 38    36    350 0   0      false(unreach-call) 1 --- inspect 80     73     690   .68 0      unknown 0 --- inspect 4.2  2.5  240 0   0      true -32 --- 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 250   240   760 1800 .71 0      false(unreach-call) 1 wit inspect 12    10    350 0   0      timeout 0 --- inspect 97     91     700   .70 0      unknown 0 --- inspect 3.8  2.2  250 0   0      true -32 --- inspect .61   .61   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 24   17   700 220 .75 .0041 false(unreach-call) 1 wit inspect 10    8.6  360 0   0      false(unreach-call) 1 --- inspect 25     20     680   .68 0      unknown 0 --- inspect 4.8  2.7  250 0   0      true -32 --- inspect .61   .63   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 120   120   860 850 .71 0      timeout 0 wit inspect 92    90    450 0   .0041 timeout 0 --- inspect 97     90     790   .70 0      unknown 0 --- inspect 4.1  2.4  250 0   0      true -32 --- inspect .60   .61   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 330   320   920 2700 .71 .0041 false(unreach-call) 1 wit inspect 67    65    450 0   0      timeout 0 --- inspect 97     91     810   .70 0      unknown 0 --- inspect 4.0  2.3  250 0   0      true -32 --- 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 34   26   840 290 .75 0      false(unreach-call) 1 wit inspect 20    18    450 0   0      false(unreach-call) 1 --- inspect 35     30     820   .68 0      unknown 0 --- inspect 4.3  2.5  260 0   0      true -32 --- inspect .58   .58   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 8200 .72 0      error (invalid witness file) 0 --- inspect .60 .38 40 0   0      error (2) 0 --- inspect .031 .031 5.6 0    0      error (invalid witness file) 0 --- inspect .93 .66 47 0   0      error (invalid witness file) 0 --- inspect .0016 .0021 .54 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 49   41   940 470 .71 0      false(unreach-call) 1 wit inspect 70    68    550 0   0      false(unreach-call) 1 --- inspect 47     42     910   .68 0      unknown 0 --- inspect 4.2  2.4  250 0   0      true -32 --- inspect .61   .61   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 610   610   1100 4500 .71 0      timeout 0 wit inspect 92    90    560 0   0      timeout 0 --- inspect 97     91     930   .70 0      unknown 0 --- inspect 3.9  2.3  250 0   0      true -32 --- inspect .58   .60   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 200   190   700 1600 .71 0      timeout 0 wit inspect 91    90    340 0   0      timeout 0 --- inspect 97     90     610   1.0  0      unknown 0 --- inspect 3.7  2.2  250 0   0      true -32 --- inspect .58   .58   20    .049  0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 380   370   810 3000 .71 0      false(unreach-call) 1 wit inspect 52    50    320 0   .0041 timeout 0 --- inspect 97     91     570   .70 0      unknown 0 --- inspect 3.6  2.2  250 0   0      true -32 --- inspect .58   .58   20    .049  0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 360   350   740 3600 .71 .0041 false(unreach-call) 1 wit inspect 8.7  7.0  300 0   0      timeout 0 --- inspect 97     91     600   .69 .0041 unknown 0 --- inspect 3.5  2.1  240 0   0      true -32 --- inspect .58   .58   20    .049  .0041 - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 81   73   460 660 .71 0      false(unreach-call) 1 wit inspect 10    8.5  310 0   0      timeout (false(unreach-call)) 0 --- inspect 94     89     430   .68 0      unknown 0 --- inspect 4.2  2.5  240 0   0      true -32 --- inspect .59   .59   20    .049  .10   - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 86   79   460 780 .71 0      false(unreach-call) 1 wit inspect 45    44    340 0   0      timeout 0 --- inspect 97     90     430   .71 0      unknown 0 --- inspect 3.6  2.1  250 0   0      true -32 --- inspect .57   .57   20    .049  .0041 - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 180   170   550 1400 .71 0      false(unreach-call) 1 wit inspect 19    18    320 0   0      timeout 0 --- inspect 97     92     460   .75 0      unknown 0 --- inspect 4.1  2.4  250 0   0      true -32 --- inspect .58   .58   20    .049  .0041 - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1000 5500 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   820 6400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   980 5400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 42 0   0      error (2) 0 --- inspect .022 .023 5.5 0    0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   920 6300 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1000 6600 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1000 6500 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1200 6400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 42 0   0      error (2) 0 --- inspect .023 .025 5.6 0    0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   910 8600 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 5400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 41 0   0      error (2) 0 --- inspect .053 .054 5.5 0    0     
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 6500 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 6700 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 41 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 6000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 5200 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   810 6100 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 41 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   860 7300 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   850 6300 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   880 6500 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 43 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   840 7600 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 810   800   780 6000 .71 6.6    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 680    680    570 0   0      true 2 --- inspect 830     820     730   .68 0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 880   870   830 6600 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 550    550    510 0   0      timeout 0 --- inspect 960     950     840   .72 0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   790 6500 .72 6.1    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 510   500   800 4600 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    480 0   0      true 2 --- inspect 590     580     770   .68 0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 73   66   630 520 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 77    75    360 0   0      true 2 --- inspect 78     73     610   .71 0     
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 43   33   940 360 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.5  320 0   0      true 2 --- inspect 47     39     940   .68 0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i error (7) 0 --- inspect 13   4.2 330 95 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .022 .025 5.7 0    0     
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 12   5.0 340 100 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 13     7.2   310   .68 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 47   37   480 530 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 16    14    300 0   0      true 2 --- inspect 51     43     530   .68 0     
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 12   4.8 360 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 13     7.4   300   .71 .0041
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 15   5.5 370 130 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.6  3.6  260 0   0      true 2 --- inspect 17     9.2   440   .75 0     
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 14   5.8 360 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  250 0   0      true 2 --- inspect 14     8.8   300   .68 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 13   5.3 370 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 14     8.2   300   .68 0     
floats-cbmc-regression/float-no-simp8_true-unreach-call.i error (7) 0 --- inspect 14   4.9 330 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 --- inspect 7.2 2.5 330 59 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .50 40 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 25   16   400 280 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  2.9  260 0   0      true 2 --- inspect 35     28     450   .71 0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 13   4.9 360 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 15     8.9   290   .71 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 12   5.0 340 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 14     8.0   320   .71 0     
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 13   5.3 370 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  250 0   0      true 2 --- inspect 14     8.2   310   .71 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 18   9.4 350 180 .75 1.2    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 18     13     300   .71 0     
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 14   5.0 370 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.3  250 0   0      true 2 --- inspect 13     7.8   310   .71 0     
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 14   4.9 370 110 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.5  3.0  260 0   .041  true 2 --- inspect 16     9.5   380   .75 0     
floats-cbmc-regression/float18_true-unreach-call.i error (7) 0 --- inspect 12   4.0 320 110 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 15   5.7 370 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.1  260 0   0      true 2 --- inspect 15     8.9   390   .75 0     
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 13   4.9 360 110 .75 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0      true 2 --- inspect 12     7.5   300   .71 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 18   11   390 160 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  3.0  250 0   0      true 2 --- inspect 21     16     370   .71 0     
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 56   45   500 650 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    8.0  300 0   0      true 2 --- inspect 73     65     590   .68 0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 200   180   750 2400 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  270 0   0      true 2 --- inspect 220     200     770   .68 0     
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 13   5.1 360 120 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0      true 2 --- inspect 13     8.1   310   .71 0     
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 17   8.5 360 160 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  270 0   0      true 2 --- inspect 16     11     320   .71 0     
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 87   76   510 1000 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 77    75    330 0   0      true 2 --- inspect 93     86     570   .68 .045 
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 23   16   360 240 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  260 0   0      true 2 --- inspect 28     22     290   .68 0     
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 15   5.6 380 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.9  260 0   0      true 2 --- inspect 15     8.8   310   .75 0     
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 15   5.8 390 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.7  7.1  270 0   0      true 2 --- inspect 17     10     390   .75 0     
floats-cbmc-regression/float_lib1_true-unreach-call.i error (7) 0 --- inspect 12   4.4 310 98 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 15   5.1 380 120 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.1  3.2  250 0   0      true 2 --- inspect 16     9.8   430   .68 0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 14   6.1 330 120 .75 0      false(unreach-call) 1 wit inspect 4.0  2.2  260 0   0      false(unreach-call) 1 --- inspect 17     9.4   310   .68 0      unknown 0 --- inspect 3.7  2.2  250 0   0      true -32 --- inspect .57   .57   20    .049  0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 14   5.4 370 110 .75 0      false(unreach-call) 1 wit inspect 4.0  2.3  260 0   .0041 false(unreach-call) 1 --- inspect 15     8.6   310   .68 .0041 unknown 0 --- inspect 4.2  2.5  250 0   0      true -32 --- inspect .57   .58   20    .053  0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   5.2 330 100 .75 0      false(unreach-call) 1 wit inspect 4.2  2.4  270 0   0      false(unreach-call) 1 --- inspect 13     8.3   310   .68 0      unknown 0 --- inspect 3.9  2.3  250 0   0      true -32 --- inspect .58   .58   20    .049  0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   5.8 360 110 .75 0      false(unreach-call) 1 wit inspect 3.8  2.2  260 0   0      false(unreach-call) 1 --- inspect 12     7.5   300   .68 0      unknown 0 --- inspect 4.8  2.8  240 0   0      true -32 --- inspect .58   .58   20    .049  0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 --- inspect 900   890   2000 7100 .72 0      error (invalid witness file) 0 --- inspect .61 .38 42 0   0      error (2) 0 --- inspect .026 .027 5.7 0    0      error (invalid witness file) 0 --- inspect 1.0  .64 47 0   0      error (invalid witness file) 0 --- inspect .0057 .014  .46 0      0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   890   1800 6100 .72 0      error (invalid witness file) 0 --- inspect .67 .41 41 0   0      error (2) 0 --- inspect .028 .030 5.7 0    0      error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0      error (invalid witness file) 0 --- inspect .0056 .0072 .54 0      0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   5.3 370 120 .75 0      false(unreach-call) 1 wit inspect 4.1  2.3  270 0   0      false(unreach-call) 1 --- inspect 14     8.6   310   .68 0      unknown 0 --- inspect 3.8  2.3  240 0   .0041 true -32 --- inspect .58   .58   20    .049  0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   4.7 350 100 .75 0      false(unreach-call) 1 wit inspect 3.8  2.1  260 0   0      false(unreach-call) 1 --- inspect 13     8.0   290   .68 0      unknown 0 --- inspect 3.7  2.2  250 0   0      true -32 --- inspect .57   .57   20    .045  0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   4.7 350 110 .75 .0041 false(unreach-call) 1 wit inspect 3.6  2.0  260 0   0      false(unreach-call) 1 --- inspect 15     8.8   310   .68 0      unknown 0 --- inspect 4.0  2.4  250 0   0      true -32 --- inspect .59   .59   20    .045  0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 410   400   2100 4400 .71 0      true -32 wit inspect 5.5  2.9  280 0   0      false(unreach-call) 1 --- inspect 32     23     1000   .68 0      unknown 0 --- inspect 4.5  2.5  260 0   .053  true -32 --- inspect .63   .62   20    .082  0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 0 wit inspect 19   11   600 160 .75 0      error (invalid witness file) 0 --- inspect 2.8  1.6  190 0   0      false(unreach-call) 1 --- inspect 18     13     590   .68 0      error (invalid witness file) 0 --- inspect 3.4  2.0  210 0   0      true -32 --- inspect .58   .58   21    .057  0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   890   5600 12000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 40 0   0      error (2) 0 --- inspect .024 .027 5.7 0    0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   7700 9700 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 24   16   1000 210 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0      true 2 --- inspect 29     23     990   .71 0     
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 16   7.3 450 130 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0      true 2 --- inspect 16     10     430   .71 0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 13   5.1 340 110 .75 6.8    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0      true 2 --- inspect 13     8.0   300   .71 0     
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 13   5.0 360 95 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  250 0   0      true 2 --- inspect 13     7.4   300   .71 0     
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 13   5.3 360 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 14     8.1   290   .71 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c error (7) 0 --- inspect 120   110   2600 1200 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   1000 9500 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .023 .024 5.7 0    0     
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 7.7 3.1 350 58 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0      true 2 --- inspect 7.2   4.4   310   .62 0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   3000 7100 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 41 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   880   2600 8000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 40 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0     
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   880   3600 11000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 770   760   920 7600 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    23    410 0   0      true 2 --- inspect 290     280     640   .71 0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 900   890   960 7000 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    22    410 0   0      true 2 --- inspect 360     350     660   .68 0     
float-benchs/exp_loop_true-unreach-call.c timeout 0 --- inspect 900   890   1400 8800 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   880   2100 7500 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   890   1100 11000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c timeout 0 --- inspect 900   890   1200 10000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 900   890   1100 8700 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .41 41 0   0      error (2) 0 --- inspect .055 .056 5.5 0    0     
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 220   210   780 1900 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.8  6.4  410 0   0      true 2 --- inspect 100     96     610   .71 0     
float-benchs/filter2_alt_true-unreach-call.c timeout 0 --- inspect 900   890   1000 8200 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
float-benchs/filter2_iterated_true-unreach-call.c error (7) 0 --- inspect 40   31   2200 480 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .022 .025 5.7 0    0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   2500 8900 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0      error (2) 0 --- inspect .022 .022 5.7 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c error (7) 0 --- inspect 600   590   3900 4800 .71 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   2700 9300 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 42 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
float-benchs/filter_iir_true-unreach-call.c timeout 0 --- inspect 900   880   2600 8400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 14   5.8 360 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 14     8.2   300   .75 0     
float-benchs/image_filter_true-unreach-call.c timeout 0 --- inspect 900   890   630 13000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 40 0   0      error (2) 0 --- inspect .024 .026 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   890   1600 7300 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c timeout 0 --- inspect 900   890   1600 7300 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .022 .024 5.7 0    0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 900   890   1700 7400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
float-benchs/interpolation2_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   1600 8000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .48 42 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   890   1500 6200 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0      error (2) 0 --- inspect .022 .024 5.7 0    0     
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c timeout 0 --- inspect 900   890   1500 7800 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 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   890   1500 6400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
float-benchs/interpolation_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   1600 7000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0      error (2) 0 --- inspect .029 .031 5.6 0    0     
float-benchs/inv_Newton_true-unreach-call.c error (7) 0 --- inspect 550   540   1900 3900 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .42 41 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c error (7) 0 --- inspect 120   110   1700 890 .71 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/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect 110   100   1800 930 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.6  280 0   0      true 2 --- inspect 71     65     510   .71 0     
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 21   13   370 230 .75 .13   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.7  260 0   0      true 2 --- inspect 90     84     360   .68 0     
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 67   59   370 790 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  260 0   0      true 2 --- inspect 64     59     340   .68 0     
float-benchs/loop_true-unreach-call.c true 2