Tool ULTIMATE Automizer 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 07:42:40 CET 2018-12-09 20:30:54 CET 2018-12-09 21:05:03 CET 2018-12-09 21:08:07 CET 2018-12-12 21:10:19 CET 2018-12-09 16:43:04 CET 2018-12-09 20:42:29 CET
Run set uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-uautomizer.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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.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 260 .75 0      false(unreach-call) 1 wit inspect 55    52    360 0   0      false(unreach-call) 1 --- inspect 36     29     680   .68 0      unknown 0 --- inspect 3.9  2.2  250 0   .0041 true -32 --- inspect .58   .58   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 94   86   730 640 .71 0      false(unreach-call) 1 wit inspect 13    11    350 0   0      timeout (false(unreach-call)) 0 --- inspect 95     90     700   .68 0      unknown 0 --- inspect 3.9  2.2  250 0   0      true -32 --- inspect .58   .58   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 64   57   710 480 .71 0      false(unreach-call) 1 wit inspect 38    36    360 0   0      false(unreach-call) 1 --- inspect 64     59     680   .68 0      unknown 0 --- inspect 4.2  2.5  250 0   0      true -32 --- inspect .58   .57   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 250   250   760 1500 .71 0      false(unreach-call) 1 wit inspect 14    12    350 0   0      timeout 0 --- inspect 97     91     700   .68 0      unknown 0 --- inspect 3.9  2.3  250 0   0      true -32 --- inspect .59   .59   20    .053  .0041 - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 25   17   710 220 .75 0      false(unreach-call) 1 wit inspect 12    9.8  360 0   0      false(unreach-call) 1 --- inspect 25     20     680   .68 .0041 unknown 0 --- inspect 4.7  2.7  270 0   0      true -32 --- inspect .61   .61   20    .053  .0041 - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 130   120   860 980 .71 0      timeout 0 wit inspect 92    90    450 0   0      timeout 0 --- inspect 97     92     810   .70 0      unknown 0 --- inspect 4.4  2.5  250 0   0      true -32 --- inspect .60   .60   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 330   320   910 2300 .71 0      false(unreach-call) 1 wit inspect 77    75    460 0   .0041 timeout 0 --- inspect 97     91     800   .73 .0041 unknown 0 --- inspect 4.2  2.4  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   850 290 .75 0      false(unreach-call) 1 wit inspect 23    21    450 0   0      false(unreach-call) 1 --- inspect 36     30     820   .68 0      unknown 0 --- inspect 5.1  2.9  250 0   0      true -32 --- inspect .59   .59   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 6800 .72 0      error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .028 .028 5.6 0    0      error (invalid witness file) 0 --- inspect .98 .63 47 0   0      error (invalid witness file) 0 --- inspect .0065 .0081 .54 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 47   38   930 390 .71 0      false(unreach-call) 1 wit inspect 75    72    550 0   0      false(unreach-call) 1 --- inspect 48     42     910   .71 0      unknown 0 --- inspect 4.4  2.5  250 0   .0041 true -32 --- inspect .57   .57   20    .053  0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 610   600   1100 5200 .71 0      timeout 0 wit inspect 92    89    560 0   0      timeout 0 --- inspect 97     91     920   .73 0      unknown 0 --- inspect 4.3  2.4  250 0   0      true -32 --- inspect .58   .58   20    .053  .0041 - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 200   190   700 1700 .70 0      timeout 0 wit inspect 92    90    330 0   0      timeout 0 --- inspect 97     91     620   .74 0      unknown 0 --- inspect 3.8  2.2  250 0   0      true -32 --- inspect .57   .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 3600 .71 0      false(unreach-call) 1 wit inspect 57    55    320 0   .0041 timeout 0 --- inspect 97     92     570   1.3  0      unknown 0 --- inspect 3.5  2.1  240 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   360   760 2900 .71 0      false(unreach-call) 1 wit inspect 11    8.6  310 0   0      timeout 0 --- inspect 97     92     610   .70 0      unknown 0 --- inspect 3.6  2.2  250 0   0      true -32 --- inspect .59   .59   20    .049  0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 80   73   460 670 .71 0      false(unreach-call) 1 wit inspect 11    9.4  310 0   0      false(unreach-call) 1 --- inspect 87     82     450   .68 0      unknown 0 --- inspect 4.0  2.4  250 0   .0041 true -32 --- inspect .60   .59   20    .049  0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 88   80   460 700 .71 0      false(unreach-call) 1 wit inspect 53    51    340 0   0      timeout (false(unreach-call)) 0 --- inspect 94     89     440   .71 0      unknown 0 --- inspect 3.7  2.2  250 0   0      true -32 --- inspect .60   .59   20    .049  0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 180   170   570 1400 .71 0      false(unreach-call) 1 wit inspect 22    20    330 0   0      timeout 0 --- inspect 97     91     470   1.4  0      unknown 0 --- inspect 4.0  2.3  250 0   0      true -32 --- inspect .60   .60   20    .049  0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1000 7600 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   810 6200 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0      error (2) 0 --- inspect .028 .030 5.6 0    0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   990 7200 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .38 40 0   0      error (2) 0 --- inspect .020 .022 5.7 0    0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   920 5900 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1000 6100 .72 6.2    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 6800 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 42 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1200 7800 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0      error (2) 0 --- inspect .033 .035 5.6 0    0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   920 8000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 5900 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
floats-cdfpl/newton_3_2_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 .62 .38 41 0   0      error (2) 0 --- inspect .027 .029 5.6 0    0     
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 6100 .72 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     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 5700 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 42 0   0      error (2) 0 --- inspect .021 .024 5.6 0    0     
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1100 5900 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   810 8000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   860 5900 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   850 7700 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   900 9200 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   840 6300 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 840   830   760 5400 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 690    690    570 0   0      true 2 --- inspect 900     890     760   .71 0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 880   870   860 6300 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 510    510    510 0   0      timeout 0 --- inspect 960     950     760   .72 0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   790 6300 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .022 .025 5.6 0    0     
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 530   520   850 4600 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    480 0   0      true 2 --- inspect 610     610     790   .71 0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 74   65   640 580 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 77    75    360 0   0      true 2 --- inspect 76     71     610   .68 0     
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 42   33   890 400 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  3.3  320 0   0      true 2 --- inspect 46     38     950   .68 0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i error (7) 0 --- inspect 13   4.2 340 100 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .46 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 13   5.6 350 100 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 13     7.5   310   .71 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 48   38   480 510 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    19    300 0   0      true 2 --- inspect 52     44     550   .68 0     
floats-cbmc-regression/float-no-simp3_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.8  2.1  250 0   .0041 true 2 --- inspect 13     7.1   300   .71 0     
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 15   5.2 390 140 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.7  270 0   0      true 2 --- inspect 22     12     440   .71 0     
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 14   5.4 360 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0      true 2 --- inspect 14     8.5   310   .75 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 12   4.9 330 100 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 13     7.8   300   .75 .0041
floats-cbmc-regression/float-no-simp8_true-unreach-call.i error (7) 0 --- inspect 13   4.1 350 110 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 --- inspect 7.3 2.3 330 61 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 23   13   390 270 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  260 0   0      true 2 --- inspect 33     27     450   .71 0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 13   4.9 360 100 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 13     8.0   300   .75 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 13   5.4 350 97 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  250 0   0      true 2 --- inspect 14     8.3   310   .68 .0041
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 13   4.9 340 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   .26   true 2 --- inspect 15     8.8   300   .71 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 17   9.3 360 170 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  250 0   .0041 true 2 --- inspect 21     15     300   .71 0     
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 14   5.0 370 100 .75 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   .0041 true 2 --- inspect 14     7.8   310   .75 0     
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 14   5.5 370 110 .75 .041  - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.7  260 0   0      true 2 --- inspect 18     10     390   .71 0     
floats-cbmc-regression/float18_true-unreach-call.i error (7) 0 --- inspect 12   4.4 340 98 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0      error (2) 0 --- inspect .027 .029 5.7 0    0     
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 15   5.5 390 110 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  260 0   0      true 2 --- inspect 16     9.8   390   .71 0     
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 13   4.8 360 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 14     8.2   290   .71 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 19   10   390 180 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0      true 2 --- inspect 20     15     380   .75 .0041
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 59   48   500 620 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 10    7.7  290 0   0      true 2 --- inspect 85     75     590   .71 0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 170   160   780 2100 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  270 0   0      true 2 --- inspect 200     190     780   .71 0     
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 14   5.3 360 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 15     9.0   300   .75 0     
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 16   8.7 350 160 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.1  270 0   0      true 2 --- inspect 17     11     310   .71 0     
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 86   75   510 1200 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 92    89    330 0   0      true 2 --- inspect 94     86     580   .71 0     
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 23   15   330 260 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.1  260 0   .16   true 2 --- inspect 28     22     300   .68 0     
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 15   5.4 370 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  2.9  260 0   0      true 2 --- inspect 15     9.0   300   .75 0     
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 15   6.1 370 120 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.9  5.9  270 0   0      true 2 --- inspect 16     9.4   400   .75 0     
floats-cbmc-regression/float_lib1_true-unreach-call.i error (7) 0 --- inspect 12   4.5 310 90 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .87 .54 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 15   5.2 370 140 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  260 0   0      true 2 --- inspect 21     12     430   .75 0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 16   6.0 370 130 .75 0      false(unreach-call) 1 wit inspect 5.2  2.9  260 0   0      false(unreach-call) 1 --- inspect 15     9.6   300   .71 0      unknown 0 --- inspect 4.1  2.4  250 0   0      true -32 --- inspect .58   .58   20    .049  0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   5.4 350 99 .75 0      false(unreach-call) 1 wit inspect 5.8  3.2  260 0   0      false(unreach-call) 1 --- inspect 14     8.1   310   .75 0      unknown 0 --- inspect 3.8  2.3  250 0   0      true -32 --- inspect .61   .61   20    .053  0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 14   5.5 370 110 .75 0      false(unreach-call) 1 wit inspect 4.9  2.8  270 0   0      false(unreach-call) 1 --- inspect 14     8.4   300   .68 0      unknown 0 --- inspect 4.1  2.4  250 0   0      true -32 --- 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 14   5.9 370 120 .75 0      false(unreach-call) 1 wit inspect 4.1  2.3  260 0   0      false(unreach-call) 1 --- inspect 13     8.0   300   .71 0      unknown 0 --- inspect 4.6  2.7  250 0   0      true -32 --- inspect .59   .59   20    .049  0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 --- inspect 900   890   2000 6400 .73 .012  error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0      error (invalid witness file) 0 --- inspect 1.1  .69 48 0   0      error (invalid witness file) 0 --- inspect .0058 .0070 .40 0      0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   890   1800 6600 .72 0      error (invalid witness file) 0 --- inspect .73 .44 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0      error (invalid witness file) 0 --- inspect 1.1  .71 47 0   0      error (invalid witness file) 0 --- inspect .0044 .0056 .54 0      0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   5.5 330 110 .75 0      false(unreach-call) 1 wit inspect 4.9  2.8  260 0   0      false(unreach-call) 1 --- inspect 14     8.8   300   .71 0      unknown 0 --- inspect 3.9  2.3  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.2 360 110 .75 0      false(unreach-call) 1 wit inspect 4.7  2.6  260 0   0      false(unreach-call) 1 --- inspect 13     7.3   300   .75 0      unknown 0 --- inspect 3.6  2.1  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 13   4.8 370 100 .75 0      false(unreach-call) 1 wit inspect 3.7  2.1  260 0   0      false(unreach-call) 1 --- inspect 13     7.2   300   .68 0      unknown 0 --- inspect 3.8  2.2  250 0   0      true -32 --- inspect .56   .56   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 4100 .71 0      true -32 wit inspect 5.9  3.2  250 0   0      false(unreach-call) 1 --- inspect 33     23     1000   .71 0      unknown 0 --- inspect 4.8  2.7  270 0   0      true -32 --- inspect .60   .60   20    .082  0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 0 wit inspect 19   11   600 170 .75 0      error (invalid witness file) 0 --- inspect 3.2  1.8  200 0   .0041 false(unreach-call) 1 --- inspect 21     15     590   .68 0      error (invalid witness file) 0 --- inspect 4.0  2.3  210 0   0      true -32 --- inspect .59   .58   20    .057  0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   840   2800 9700 .69 6.6    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 0 --- inspect 900   850   4500 9100 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .026 .026 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.6  2.6  250 0   0      true 2 --- inspect 27     21     1000   .68 0     
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 15   7.5 450 120 .75 7.0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 16     11     430   .75 0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 13   5.2 370 99 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0      true 2 --- inspect 16     9.6   300   .75 0     
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 13   5.3 360 110 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0      true 2 --- inspect 14     7.6   300   .75 0     
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 13   5.2 360 120 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 16     9.2   300   .75 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c error (7) 0 --- inspect 120   110   2600 1100 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   1100 8600 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0      error (2) 0 --- inspect .023 .023 5.7 0    0     
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 7.6 2.6 350 58 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 8.4   4.6   300   .66 0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   3000 5900 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   740   2600 12000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 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   740   2600 13000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0      error (2) 0 --- inspect .026 .027 5.7 0    0     
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   890   910 9000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 43 0   0      error (2) 0 --- inspect .025 .027 5.7 0    0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   900 7400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .36 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
float-benchs/exp_loop_true-unreach-call.c timeout 0 --- inspect 900   890   1300 9000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0      error (2) 0 --- inspect .022 .025 5.7 0    0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900   740   2600 11000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0      error (2) 0 --- inspect .022 .024 5.7 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 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c timeout 0 --- inspect 900   890   1100 8700 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 870   850   1100 11000 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 14    11    460 0   0      true 2 --- inspect 550     540     910   .68 .0041
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 220   210   720 2800 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.7  5.6  410 0   0      true 2 --- inspect 110     100     600   .71 0     
float-benchs/filter2_alt_true-unreach-call.c timeout 0 --- inspect 900   890   1000 7800 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0     
float-benchs/filter2_iterated_true-unreach-call.c error (7) 0 --- inspect 38   31   2200 430 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   2500 8400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   3800 8100 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   2900 10000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .49 42 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
float-benchs/filter_iir_true-unreach-call.c timeout 0 --- inspect 900   880   2700 8400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .39 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 13   5.2 370 130 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.8  250 0   0      true 2 --- inspect 16     9.4   300   .68 0     
float-benchs/image_filter_true-unreach-call.c timeout 0 --- inspect 900   890   620 12000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   890   1600 6700 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c timeout 0 --- inspect 900   890   1600 6000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 900   890   1600 7900 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 42 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0     
float-benchs/interpolation2_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   1600 7400 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900   890   1500 9800 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .022 .022 5.5 0    0     
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c timeout 0 --- inspect 900   890   1500 7600 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 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 8100 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0     
float-benchs/interpolation_true-unreach-call_true-termination.c timeout 0 --- inspect 900   890   1700 7600 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .34 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
float-benchs/inv_Newton_true-unreach-call.c error (7) 0 --- inspect 500   490   1600 4900 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c error (7) 0 --- inspect 120   110   1700 950 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 41 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect 110   100   1800 1000 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.7  280 0   0      true 2 --- inspect 72     66     500   .68 0     
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 20   12   340 190 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  260 0   .14   true 2 --- inspect 57     51     340   .71 0     
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 66   58   370 870 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit