Tool 2LS 0.7.2-sv-comp19 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-04 22:44:17 CET 2018-12-06 09:36:46 CET 2018-12-06 10:26:50 CET 2018-12-06 10:31:50 CET 2018-12-12 19:28:33 CET 2018-12-06 06:59:33 CET 2018-12-06 09:46:05 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options --graphml-witness witness.graphml -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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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 6.8   6.8   61 84    0      0     false(unreach-call) 1 wit inspect 55    53    350 0   0   false(unreach-call) 1 --- inspect 33     28     680   .71 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.3   6.3   60 68    0      0     false(unreach-call) 1 wit inspect 13    11    350 0   0   timeout (false(unreach-call)) 0 --- inspect 94     89     700   .68 0   false(unreach-call) 1 --- inspect 3.5  2.1  240 0   0    false(unreach-call) 1 --- inspect .60   .59   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.6   2.5   51 32    0      0     false(unreach-call) 1 wit inspect 37    36    350 0   0   false(unreach-call) 1 --- inspect 65     59     690   .68 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.4   2.4   50 25    0      0     false(unreach-call) 1 wit inspect 12    11    350 0   0   timeout 0 --- inspect 97     91     710   .69 0   false(unreach-call) 1 --- inspect 3.6  2.1  240 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.9   3.9   53 41    0      0     false(unreach-call) 1 wit inspect 12    9.5  350 0   0   false(unreach-call) 1 --- inspect 24     20     680   .68 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .053 .0041 - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.5   3.4   90 32    0      0     timeout 0 wit inspect 92    90    440 0   0   timeout 0 --- inspect 97     91     810   .83 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0    false(unreach-call) 1 --- inspect .58   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.7   6.7   94 63    0      0     false(unreach-call) 1 wit inspect 74    72    440 0   0   timeout 0 --- inspect 97     91     800   .68 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 17     17     120 170    0      0     false(unreach-call) 1 wit inspect 23    20    450 0   0   false(unreach-call) 1 --- inspect 40     34     830   .71 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 40     40     210 400    0      0     true -32 wit inspect 5.0  2.7  250 0   0   timeout 0 --- inspect 97     91     880   .72 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .61   .61   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 64     64     220 680    0      0     true -32 wit inspect 4.8  2.7  250 0   0   false(unreach-call) 1 --- inspect 53     47     920   .68 0   false(unreach-call) 1 --- inspect 3.6  2.1  240 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 35     35     190 440    0      0     true -32 wit inspect 4.9  2.7  250 0   0   timeout 0 --- inspect 97     92     920   .68 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .74  .74  24 8.4  0      0     timeout 0 wit inspect 92    90    330 0   0   timeout 0 --- inspect 97     91     620   .69 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0    false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .58  .57  24 7.1  0      0     false(unreach-call) 1 wit inspect 7.2  5.2  310 0   0   timeout 0 --- inspect 97     91     570   .83 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.6   1.6   31 19    0      0     false(unreach-call) 1 wit inspect 7.0  5.1  310 0   0   timeout 0 --- inspect 97     92     600   .68 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .049 .0041 - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .90  .90  26 11    0      0     false(unreach-call) 1 wit inspect 11    9.4  310 0   0   true -32 --- inspect 6.6   3.8   300   .62 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .99  .98  26 12    0      0     false(unreach-call) 1 wit inspect 58    55    340 0   0   true -32 --- inspect 6.3   3.6   290   .62 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .049 .17   - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .71  .70  24 8.2  0      0     false(unreach-call) 1 wit inspect 21    19    320 0   0   true -32 --- inspect 6.5   3.7   290   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 2 wit inspect 8.6   8.6   63 90    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    610 0   0   timeout 0 --- inspect 960     950     980   .72 0  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 2 wit inspect 7.8   7.8   63 110    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0   timeout 0 --- inspect 960     950     790   .70 0  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 2 wit inspect 10     10     64 110    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0   timeout 0 --- inspect 960     950     960   .74 0  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 2 wit inspect 21     21     130 240    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    530 0   0   timeout 0 --- inspect 960     950     900   .70 0  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 2 wit inspect 32     32     130 280    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    810 0   0   timeout 0 --- inspect 960     950     970   .72 0  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 2 wit inspect 27     27     130 280    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    510 0   0   timeout 0 --- inspect 960     950     1000   .70 0  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 2 wit inspect 33     33     130 330    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0   timeout 0 --- inspect 960     950     1100   1.5  0  
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i true 2 wit inspect 51     51     130 470    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    550 0   0   timeout 0 --- inspect 960     950     890   .71 0  
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i true 2 wit inspect 81     81     220 940    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    590 0   0   timeout 0 --- inspect 960     950     1100   .72 0  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 2 wit inspect 73     73     210 580    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    550 0   0   timeout 0 --- inspect 960     950     1100   1.8  0  
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i true 2 wit inspect 74     74     190 740    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    680 0   0   timeout 0 --- inspect 960     950     1100   .74 0  
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i true 2 wit inspect 110     110     210 980    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    700 0   0   timeout 0 --- inspect 960     950     1000   .70 0  
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i true 2 wit inspect 74     74     220 720    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0   timeout 0 --- inspect 960     950     1000   .68 0  
floats-cdfpl/sine_4_true-unreach-call_true-termination.i true 2 wit inspect 25     25     41 290    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    500 0   0   timeout 0 --- inspect 960     950     790   2.1  0  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 2 wit inspect 1.7   1.7   33 21    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    490 0   0   timeout 0 --- inspect 960     950     830   .81 0  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 1.9   1.9   31 23    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    650 0   0   timeout 0 --- inspect 960     950     820   .70 0  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 1.2   1.2   27 17    0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 760    760    590 0   0   timeout 0 --- inspect 960     950     820   1.7  0  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 1.7   1.7   31 24    0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 500    500    540 0   0   timeout 0 --- inspect 960     950     810   .70 0  
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 55     55     50 800    0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 680    680    570 0   0   timeout (true) 0 --- inspect 940     930     810   .68 0  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 25     25     50 360    0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 510    510    510 0   0   timeout 0 --- inspect 960     950     760   .73 0  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 79     79     68 1100    0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 280    280    500 0   0   timeout 0 --- inspect 960     950     770   .69 0  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 85     85     68 1000    0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 810    810    480 0   0   true 2 --- inspect 560     560     780   .68 0  
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect .79  .79  25 10    0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 78    76    360 0   0   true 2 --- inspect 85     79     610   .71 0  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect .30  .30  38 3.3  .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.0  4.3  320 0   0   true 2 --- inspect 45     38     940   .71 0  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect .92  .92  120 12    .0082 .090 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 12    9.4  780 0   0   error (7) 0 --- inspect 13     8.0   300   .75 0  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect .097 .094 23 .73 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 12     6.9   300   .68 0  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect .69  .69  29 10    .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    17    300 0   0   true 2 --- inspect 52     45     540   .71 0  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect .10  .099 23 1.1  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0   true 2 --- inspect 13     7.2   300   .71 0  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect .31  .31  37 3.4  .0082 .090 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.7  3.6  280 0   0   true 2 --- inspect 18     10     440   .71 0  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect .090 .088 24 .91 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 14     8.0   300   .71 0  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect .10  .10  23 .87 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0   true 2 --- inspect 13     7.6   290   .68 0  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .22  .22  28 1.6  .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  260 0   0   error (7) 0 --- inspect 12     7.0   290   .68 0  
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .21  .21  28 1.7  .0082 .30  - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 5.6  3.0  260 0   0   unknown 0 --- inspect 6.5   3.9   280   .62 0  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .22  .21  28 2.1  .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.5  3.0  270 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 .086 .085 24 .90 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.2  1.9  250 0   0   true 2 --- inspect 13     8.2   290   .75 0  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect .12  .12  24 .85 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0   true 2 --- inspect 13     7.9   310   .68 0  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect .096 .094 24 .88 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0   true 2 --- inspect 15     9.0   310   .75 0  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect .096 .094 24 .96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  260 0   0   true 2 --- inspect 19     14     290   .68 0  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect .14  .14  24 1.3  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  250 0   0   true 2 --- inspect 14     8.2   310   .68 0  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .18  .18  28 2.2  .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  260 0   0   true 2 --- inspect 14     8.3   390   .67 0  
floats-cbmc-regression/float18_true-unreach-call.i timeout 0 --- inspect 900     900     2400 10000    .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 41 0   0   error (2) 0 --- inspect .023 .024 5.7 0    0  
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .21  .20  28 1.8  .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  260 0   0   true 2 --- inspect 16     9.7   400   .68 0  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect .091 .089 24 .70 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 14     8.8   290   .75 0  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect .14  .13  24 1.3  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  250 0   0   true 2 --- inspect 21     14     380   .68 0  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect .25  .25  31 2.8  .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 10    7.5  290 0   0   true 2 --- inspect 63     55     570   .68 0  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect .12  .11  24 .70 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.6  3.1  270 0   0   true 2 --- inspect 210     190     710   .68 0  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect .091 .089 24 1.3  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0   true 2 --- inspect 13     7.8   310   .68 0  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect .15  .15  24 .93 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  270 0   0   true 2 --- inspect 20     13     310   .75 0  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 9.5   9.5   46 120    .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 93    90    330 0   0   true 2 --- inspect 92     84     590   .68 0  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect .11  .11  24 .78 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  260 0   0   true 2 --- inspect 28     23     300   .68 0  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect .11  .10  24 .99 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0   true 2 --- inspect 15     8.6   310   .68 0  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect .53  .53  28 6.3  .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.5  6.2  270 0   0   true 2 --- inspect 14     8.8   390   .68 0  
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 6.6   6.6   35 66    .0082 .090 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.1  3.3  260 0   0   error (7) 0 --- inspect 12     7.4   290   .71 0  
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect .23  .22  29 2.1  .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  250 0   0   true 2 --- inspect 17     10     430   .71 0  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c error (134) 0 --- inspect .096 .095 24 1.2  0      0     error (invalid witness file) 0 --- inspect .71 .45 41 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .94 .62 47 0   0    error (invalid witness file) 0 --- inspect .0038 .0049 .54 0     0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .12  24 1.5  0      0     false(unreach-call) 1 wit inspect 4.7  2.7  260 0   0   false(unreach-call) 1 --- inspect 13     8.3   300   .71 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .057 0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  .12  24 1.5  0      0     false(unreach-call) 1 wit inspect 4.3  2.4  260 0   0   false(unreach-call) 1 --- inspect 14     8.3   310   .71 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0    false(unreach-call) 1 --- inspect .59   .59   20    .057 0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  .13  24 1.4  0      0     false(unreach-call) 1 wit inspect 3.8  2.1  260 0   0   false(unreach-call) 1 --- inspect 13     8.2   310   .71 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .61   .61   20    .053 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 --- inspect 900     900     1300 9400    .012  0     error (invalid witness file) 0 --- inspect .74 .44 42 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .62 47 0   0    error (invalid witness file) 0 --- inspect .0023 .0028 .41 0     0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c error (6) 0 --- inspect .083 .083 24 .82 0      0     error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .63 47 0   0    error (invalid witness file) 0 --- inspect .0053 .0069 .53 0     0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  .13  24 1.3  0      0     false(unreach-call) 1 wit inspect 3.7  2.1  260 0   0   false(unreach-call) 1 --- inspect 15     8.7   310   .75 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .59   .60   20    .053 0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .10  24 1.0  0      0     false(unreach-call) 1 wit inspect 4.8  2.7  260 0   0   false(unreach-call) 1 --- inspect 12     7.0   300   .68 0   unknown 0 --- inspect 3.6  2.1  250 0   0    error (2) 0 --- inspect .56   .56   20    .037 .0041 - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .098 24 1.1  0      0     false(unreach-call) 1 wit inspect 3.6  2.0  250 0   0   false(unreach-call) 1 --- inspect 12     7.5   290   .68 0   unknown 0 --- inspect 3.7  2.2  250 0   0    error (2) 0 --- inspect .55   .57   20    .037 .0041 - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3   3.2   260 34    0      0     true -32 wit inspect 6.5  3.4  280 0   0   false(unreach-call) 1 --- inspect 27     19     990   .68 0   false(unreach-call) 1 --- inspect 4.8  2.7  280 0   0    false(unreach-call) 1 --- inspect .63   .63   20    .086 0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect .56  .54  41 6.2  0      0     true -32 wit inspect 4.0  2.2  250 0   0   false(unreach-call) 1 --- inspect 23     17     600   .68 0   false(unreach-call) 1 --- inspect 4.1  2.4  250 0   0    false(unreach-call) 1 --- inspect .64   .63   20    .061 0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c error (6) 0 --- inspect .10  .10  24 .92 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     820 8100    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect .15  .15  24 1.5  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0   true 2 --- inspect 27     21     990   .71 0  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect .12  .12  24 .93 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 17     11     430   .71 0  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect .15  .14  24 .77 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 13     8.3   300   .71 0  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect .094 .093 24 .96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0   true 2 --- inspect 12     7.5   290   .63 0  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect .11  .11  24 .58 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0   true 2 --- inspect 12     7.2   300   .68 0  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 59     59     260 660    0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    36    500 0   0   error (7) 0 --- inspect 120     120     2600   .71 0  
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     420 7800    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .11  .11  24 .84 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 7.0   4.4   310   .62 0  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 2 wit inspect 7.0   7.0   110 61    0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1300 0   0   timeout 0 --- inspect 960     950     3000   .72 0  
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     410 9100    .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 42 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     380 10000    .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .56  .56  24 6.4  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    23    410 0   0   true 2 --- inspect 330     320     660   .68 0  
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect .60  .60  24 7.5  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    24    410 0   0   true 2 --- inspect 440     430     740   .68 0  
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 20     20     240 240    0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 670    650    7000 0   0   timeout 0 --- inspect 960     950     1100   2.1  0  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     2100 9400    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0   error (2) 0 --- inspect .036 .039 5.4 0    0  
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c error (6) 0 --- inspect .086 .087 24 .97 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0  
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c error (6) 0 --- inspect .10  .10  24 .83 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 42 0   0   error (2) 0 --- inspect .054 .055 5.6 0    0  
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c error (6) 0 --- inspect .11  .11  25 .90 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0  
float-benchs/filter1_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     1800 11000    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .024 .025 5.5 0    0  
float-benchs/filter2_alt_true-unreach-call.c timeout 0 --- inspect 900     900     210 10000    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 --- inspect 900     900     610 7300    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     780 7500    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     560 5000    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .35 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0  
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 --- inspect 900     900     680 8200    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
float-benchs/filter_iir_true-unreach-call.c timeout 0 --- inspect 900     900     310 9000    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .43 41 0   0   error (2) 0 --- inspect .020 .022 5.6 0    0  
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect .13  .13  24 .72 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0   true 2 --- inspect 13     8.0   300   .25 0  
float-benchs/image_filter_true-unreach-call.c timeout 0 --- inspect 900     900     1000 9300    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .40 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c error (6) 0 --- inspect .093 .093 24 .86 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0  
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c error (6) 0 --- inspect .082 .081 24 .91 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c error (6) 0 --- inspect .092 .093 25 .78 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0  
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect .39  .38  24 3.6  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 50    47    550 0   0   timeout 0 --- inspect 960     950     1600   .73 0  
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c error (6) 0 --- inspect .11  .11  24 .81 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c error (6) 0 --- inspect .090 .091 24 .65 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0  
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c error (6) 0 --- inspect .093 .093 24 .88 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0   error (2) 0 --- inspect .025 .027 5.7 0    0  
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect .20  .20  24 2.9  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    24    470 0   0   timeout 0 --- inspect 960     950     1700   .77 0  
float-benchs/inv_Newton_true-unreach-call.c timeout 0 --- inspect 900     900     1000 8500    .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 43 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0  
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c error (6) 0 --- inspect .088 .089 24 .72 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect .28  .28  24 3.7  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  3.2  280 0   0   true 2 --- inspect 71     65     500   .71 0  
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect .13  .12  24 1.2  0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  260 0   0   true 2 --- inspect 52     47     350   .68 0  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect .12  .12  24 1.3  0      0     -