Tool ULTIMATE Kojak 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 11:04:44 CET 2018-12-09 20:15:59 CET 2018-12-09 20:59:07 CET 2018-12-09 21:01:30 CET 2018-12-12 21:11:08 CET 2018-12-09 19:35:17 CET 2018-12-09 20:36:45 CET
Run set ukojak.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-ukojak.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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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 error (7) 0 --- inspect 84   76   1100 800 .71 0      error (invalid witness file) 0 --- inspect .76 .46 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .65 48 0   0      error (invalid witness file) 0 --- inspect .0020 .0026 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i error (7) 0 --- inspect 77   68   1100 690 .71 0      error (invalid witness file) 0 --- inspect .74 .45 41 0   0     error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0      error (invalid witness file) 0 --- inspect .0047 .0054 .41 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i error (7) 0 --- inspect 81   73   1100 640 .71 0      error (invalid witness file) 0 --- inspect .74 .45 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0047 .0060 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i error (7) 0 --- inspect 80   72   1100 700 .70 0      error (invalid witness file) 0 --- inspect .90 .57 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 49 0   0      error (invalid witness file) 0 --- inspect .0060 .0075 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i error (7) 0 --- inspect 83   76   1100 720 .71 0      error (invalid witness file) 0 --- inspect .80 .49 41 0   0     error (2) 0 --- inspect .019 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .61 47 0   0      error (invalid witness file) 0 --- inspect .0042 .0069 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i error (7) 0 --- inspect 73   65   1500 710 .71 0      error (invalid witness file) 0 --- inspect .65 .40 41 0   0     error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 46 0   0      error (invalid witness file) 0 --- inspect .0053 .0065 .41 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i error (7) 0 --- inspect 65   57   1400 530 .71 0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 48 0   0      error (invalid witness file) 0 --- inspect .0060 .0095 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i error (7) 0 --- inspect 54   46   1400 520 .71 0      error (invalid witness file) 0 --- inspect .76 .47 41 0   0     error (2) 0 --- inspect .020 .032 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .64 49 0   0      error (invalid witness file) 0 --- inspect .0049 .0061 .41 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i error (7) 0 --- inspect 69   61   2000 640 .71 .17   error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .65 47 0   0      error (invalid witness file) 0 --- inspect .0056 .0085 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i error (7) 0 --- inspect 71   63   1900 540 .71 0      error (invalid witness file) 0 --- inspect .70 .43 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .63 47 0   0      error (invalid witness file) 0 --- inspect .0045 .0055 .41 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i error (7) 0 --- inspect 63   55   2000 520 .71 0      error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .64 47 0   0      error (invalid witness file) 0 --- inspect .0057 .0073 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i error (7) 0 --- inspect 34   27   590 260 .75 0      error (invalid witness file) 0 --- inspect .61 .37 42 0   0     error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .61 48 0   0      error (invalid witness file) 0 --- inspect .0017 .0022 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i error (7) 0 --- inspect 35   27   610 300 .75 0      error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .024 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .73 47 0   0      error (invalid witness file) 0 --- inspect .0052 .0071 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i error (7) 0 --- inspect 34   26   590 260 .75 0      error (invalid witness file) 0 --- inspect .72 .45 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .64 48 0   0      error (invalid witness file) 0 --- inspect .0061 .010  .48 0     0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i error (7) 0 --- inspect 29   21   370 210 .75 0      error (invalid witness file) 0 --- inspect .64 .39 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 47 0   0      error (invalid witness file) 0 --- inspect .0067 .0088 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i error (7) 0 --- inspect 29   21   370 230 .75 0      error (invalid witness file) 0 --- inspect .60 .38 40 0   0     error (2) 0 --- inspect .031 .034 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 48 0   0      error (invalid witness file) 0 --- inspect .0064 .0082 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i error (7) 0 --- inspect 29   21   370 240 .75 0      error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .68 48 0   0      error (invalid witness file) 0 --- inspect .0018 .0022 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i error (7) 0 --- inspect 78   70   1100 570 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .027 .029 5.5 0    0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i error (7) 0 --- inspect 77   69   1100 600 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i error (7) 0 --- inspect 80   72   1100 620 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 42 0   0      error (2) 0 --- inspect .021 .022 5.8 0    0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i error (7) 0 --- inspect 73   64   1500 690 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i error (7) 0 --- inspect 64   56   1500 500 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i error (7) 0 --- inspect 74   65   1600 610 .71 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i error (7) 0 --- inspect 80   72   1500 630 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 42 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i error (7) 0 --- inspect 64   56   1500 630 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i error (7) 0 --- inspect 62   53   2000 570 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i error (7) 0 --- inspect 70   62   2000 600 .71 .0041 - --- 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/newton_3_3_true-unreach-call_true-termination.i error (7) 0 --- inspect 63   55   2000 560 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 42 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i error (7) 0 --- inspect 73   65   2000 630 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i error (7) 0 --- inspect 65   56   1900 540 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i error (7) 0 --- inspect 34   26   600 280 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i error (7) 0 --- inspect 35   26   590 270 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0      error (2) 0 --- inspect .027 .027 5.5 0    0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i error (7) 0 --- inspect 34   27   590 310 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0      error (2) 0 --- inspect .023 .024 5.8 0    0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i error (7) 0 --- inspect 35   27   600 320 .75 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     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i error (7) 0 --- inspect 34   27   600 280 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i error (7) 0 --- inspect 28   21   360 210 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i error (7) 0 --- inspect 27   21   360 270 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i error (7) 0 --- inspect 28   21   370 210 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
floats-cdfpl/square_7_true-unreach-call_true-termination.i error (7) 0 --- inspect 28   20   360 260 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i error (7) 0 --- inspect 28   20   370 230 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0      error (2) 0 --- inspect .023 .025 5.7 0    0     
floats-cbmc-regression/float-div1_true-unreach-call.i error (7) 0 --- inspect 18   9.8 480 160 .74 .17   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i error (7) 0 --- inspect 13   4.5 340 100 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 13   5.1 340 98 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 13     8.1   300   .75 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i error (7) 0 --- inspect 15   6.4 400 160 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 12   4.9 340 97 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.2  1.8  250 0   0      true 2 --- inspect 13     7.2   300   .75 0     
floats-cbmc-regression/float-no-simp4_true-unreach-call.i error (7) 0 --- inspect 14   4.9 370 110 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0      error (2) 0 --- inspect .021 .023 5.7 0    0     
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 16   6.7 380 140 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0      true 2 --- inspect 16     9.7   310   .68 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 13   5.4 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   300   .75 0     
floats-cbmc-regression/float-no-simp8_true-unreach-call.i error (7) 0 --- inspect 13   4.4 340 100 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 42 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 --- inspect 7.3 2.3 340 54 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i error (7) 0 --- inspect 14   5.6 370 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 12   4.8 330 100 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0      true 2 --- inspect 12     7.0   290   .75 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 14   5.1 350 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 13     7.7   320   .71 0     
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 15   5.6 360 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 17     9.7   310   .71 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 18   10   350 160 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 23     16     300   .75 0     
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 16   6.3 370 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 17     10     310   .75 0     
floats-cbmc-regression/float14_true-unreach-call.i error (7) 0 --- inspect 14   5.0 360 110 .75 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     
floats-cbmc-regression/float18_true-unreach-call.i error (7) 0 --- inspect 13   4.0 330 100 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cbmc-regression/float19_true-unreach-call.i error (7) 0 --- inspect 14   5.2 360 120 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 13   5.3 360 94 .75 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  2.0  250 0   0      true 2 --- inspect 12     7.5   290   .75 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 49   41   520 540 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0      true 2 --- inspect 22     16     370   .71 0     
floats-cbmc-regression/float21_true-unreach-call.i error (7) 0 --- inspect 21   12   410 190 .75 .045  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i timeout 0 --- inspect 900   860   790 13000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 14   5.3 350 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0      true 2 --- inspect 17     10     300   .75 .0041
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 17   8.6 340 140 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  270 0   0      true 2 --- inspect 19     13     320   .71 0     
floats-cbmc-regression/float4_true-unreach-call.i error (7) 0 --- inspect 16   6.9 410 150 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0     
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 37   30   360 520 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  260 0   0      true 2 --- inspect 32     26     300   .71 0     
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 20   8.6 470 180 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  260 0   0      true 2 --- inspect 18     11     310   .75 0     
floats-cbmc-regression/float8_true-unreach-call.i error (7) 0 --- inspect 14   4.7 360 100 .74 .041  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
floats-cbmc-regression/float_lib1_true-unreach-call.i error (7) 0 --- inspect 13   4.3 340 100 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cbmc-regression/float_lib2_true-unreach-call.i error (7) 0 --- inspect 14   5.0 370 100 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   5.2 330 110 .75 0      false(unreach-call) 1 wit inspect 3.9  2.2  250 0   0     false(unreach-call) 1 --- inspect 16     9.1   310   .71 0   unknown 0 --- inspect 3.5  2.1  250 0   .0041 true -32 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 14   5.5 370 130 .75 0      false(unreach-call) 1 wit inspect 5.0  2.9  260 0   0     false(unreach-call) 1 --- inspect 14     8.7   310   .71 0   unknown 0 --- inspect 3.5  2.0  240 0   .0041 true -32 --- inspect .58   .58   20    .053 .0041 - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 15   7.4 360 130 .75 0      false(unreach-call) 1 wit inspect 5.0  2.8  270 0   0     false(unreach-call) 1 --- inspect 13     8.3   310   .68 0   unknown 0 --- inspect 3.7  2.2  250 0   .22   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 15   7.3 350 130 .75 0      false(unreach-call) 1 wit inspect 4.8  2.8  260 0   0     false(unreach-call) 1 --- inspect 12     8.2   300   .71 0   unknown 0 --- inspect 3.6  2.1  240 0   0      true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c error (7) 0 --- inspect 68   58   420 610 .71 0      error (invalid witness file) 0 --- inspect .73 .44 40 0   0     error (2) 0 --- inspect .031 .033 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .63 47 0   0      error (invalid witness file) 0 --- inspect .0051 .0061 .41 0     0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c error (7) 0 --- inspect 48   38   430 400 .71 0      error (invalid witness file) 0 --- inspect .76 .47 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 48 0   0      error (invalid witness file) 0 --- inspect .0052 .0064 .54 0     0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   5.8 330 110 .75 0      false(unreach-call) 1 wit inspect 5.0  2.8  260 0   0     false(unreach-call) 1 --- inspect 14     8.0   300   .68 0   unknown 0 --- inspect 3.5  2.1  250 0   0      true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   5.1 370 92 .75 0      false(unreach-call) 1 wit inspect 4.5  2.5  250 0   0     false(unreach-call) 1 --- inspect 12     7.5   300   .71 0   unknown 0 --- inspect 3.3  2.0  250 0   0      true -32 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   5.0 320 100 .75 0      false(unreach-call) 1 wit inspect 4.2  2.3  260 0   0     false(unreach-call) 1 --- inspect 13     7.8   300   .68 0   unknown 0 --- inspect 3.6  2.1  250 0   0      true -32 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c error (7) 0 --- inspect 49   34   1200 490 .75 0      error (invalid witness file) 0 --- inspect .70 .43 40 0   0     error (2) 0 --- inspect .028 .030 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .63 48 0   0      error (invalid witness file) 0 --- inspect .0056 .0076 .53 0     0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c error (7) 0 --- inspect 100   93   720 890 .71 0      error (invalid witness file) 0 --- inspect .57 .36 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .62 48 0   0      error (invalid witness file) 0 --- inspect .0057 .0070 .53 0     0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   860   1800 11000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .020 .022 5.6 0    0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 0 --- inspect 900   860   1900 10000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
float-benchs/Rump_double_true-unreach-call_true-termination.c error (7) 0 --- inspect 27   19   1600 240 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 41 0   0      error (2) 0 --- inspect .028 .028 5.6 0    0     
float-benchs/Rump_float_true-unreach-call_true-termination.c error (7) 0 --- inspect 24   16   580 180 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0      error (2) 0 --- inspect .023 .024 5.7 0    0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 15   7.8 330 140 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0      true 2 --- inspect 15     8.8   290   .71 .070 
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 13   5.2 370 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 13     8.0   310   .71 7.0   
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 13   5.7 360 98 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.1  250 0   0      true 2 --- inspect 16     9.4   300   .75 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c error (7) 0 --- inspect 77   69   890 610 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c error (7) 0 --- inspect 22   13   360 210 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 7.9 3.2 340 63 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 7.2   4.0   300   .62 0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c error (7) 0 --- inspect 150   140   980 1000 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 41 0   0      error (2) 0 --- inspect .021 .022 5.8 0    0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   760   5400 8400 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   760   5100 9000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c error (7) 0 --- inspect 31   19   510 300 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   700 8500 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
float-benchs/exp_loop_true-unreach-call.c error (7) 0 --- inspect 27   19   380 240 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   750   5200 9000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .38 40 0   0      error (2) 0 --- inspect .023 .023 5.7 0    0     
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c error (7) 0 --- inspect 49   39   460 540 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c error (7) 0 --- inspect 52   42   480 520 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 40 0   0      error (2) 0 --- inspect .024 .026 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c error (7) 0 --- inspect 66   56   540 610 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
float-benchs/filter1_true-unreach-call_true-termination.c error (7) 0 --- inspect 43   35   400 400 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
float-benchs/filter2_alt_true-unreach-call.c error (7) 0 --- inspect 22   14   350 190 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
float-benchs/filter2_iterated_true-unreach-call.c error (7) 0 --- inspect 23   13   2200 200 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .024 .026 5.7 0    0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c error (7) 0 --- inspect 53   46   450 510 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c error (7) 0 --- inspect 35   26   540 270 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0      error (2) 0 --- inspect .026 .027 5.7 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c error (7) 0 --- inspect 34   26   420 270 .75 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/filter_iir_true-unreach-call.c error (7) 0 --- inspect 220   200   1200 2100 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 12   5.0 330 93 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0      true 2 --- inspect 13     8.1   300   .68 0     
float-benchs/image_filter_true-unreach-call.c timeout 0 --- inspect 900   890   520 12000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .023 .024 5.7 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c error (7) 0 --- inspect 28   18   380 320 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 42 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c timeout 0 --- inspect 900   890   1500 7300 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 900   890   1500 8900 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
float-benchs/interpolation2_true-unreach-call_true-termination.c error (7) 0 --- inspect 27   17   380 230 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c error (7) 0 --- inspect 390   380   1100 3300 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c timeout 0 --- inspect 900   890   1500 6700 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 900   890   1300 7700 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 41 0   0      error (2) 0 --- inspect .028 .028 5.6 0    0     
float-benchs/interpolation_true-unreach-call_true-termination.c error (7) 0 --- inspect 190   180   790 2200 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 41 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
float-benchs/inv_Newton_true-unreach-call.c true 2 wit inspect 25   15   380 220 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    2000 0   0      true 2 --- inspect 260     250     1100   .71 0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c error (7) 0 --- inspect 34   25   440 290 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 40 0   0      error (2) 0 --- inspect .025 .027 5.7 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c error (7) 0 --- inspect 55   47   370 620 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 18   9.5 360 140 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  260 0   0      true 2 --- inspect 29     23     330   .71 0     
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 17   9.2 350 170 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  260 0   0      true 2 --- inspect 77     70     350   .71 0     
float-benchs/loop_true-unreach-call.c error (7) 0 --- inspect 110   100   660 1300 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0     
float-benchs/mea8000_true-unreach-call.c timeout 0 --- inspect 900   830   5500 11000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 14   4.9 370 100 .75 0      - --- inspect - --- inspect - --- inspect