Tool Pinaka 0.1 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-06 20:14:43 CET 2018-12-07 17:00:25 CET 2018-12-07 18:15:01 CET 2018-12-07 18:51:03 CET 2018-12-12 20:55:30 CET 2018-12-07 16:17:05 CET 2018-12-07 17:47:50 CET
Run set pinaka.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-pinaka.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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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 3.9  3.9  72 46   0      0     false(unreach-call) 1 wit inspect 47    46    350 0   0   false(unreach-call) 1 --- inspect 38     32     680   .71 0     false(unreach-call) 1 --- inspect 4.4 2.5  250 0     0     false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.2  4.2  73 51   0      0     false(unreach-call) 1 wit inspect 13    11    350 0   0   timeout 0 --- inspect 97     91     690   .74 0     false(unreach-call) 1 --- inspect 3.7 2.1  250 0     0     false(unreach-call) 1 --- inspect .60   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.8  1.8  72 25   0      0     false(unreach-call) 1 wit inspect 35    33    350 0   0   false(unreach-call) 1 --- inspect 65     60     690   .71 0     false(unreach-call) 1 --- inspect 3.5 2.1  250 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.1  3.1  73 43   0      0     false(unreach-call) 1 wit inspect 11    9.1  350 0   0   timeout 0 --- inspect 97     91     690   .72 0     false(unreach-call) 1 --- inspect 3.5 2.0  250 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .053 .0041 - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.9  1.9  72 28   0      0     false(unreach-call) 1 wit inspect 12    9.8  350 0   0   false(unreach-call) 1 --- inspect 30     24     680   .75 0     false(unreach-call) 1 --- inspect 4.0 2.3  250 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 22    22    96 260   0      0     timeout 0 wit inspect 92    90    440 0   0   timeout 0 --- inspect 97     91     810   .72 0     false(unreach-call) 1 --- inspect 4.8 2.8  250 0     0     false(unreach-call) 1 --- inspect .59   .59   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 23    23    97 270   0      0     false(unreach-call) 1 wit inspect 67    65    440 0   0   timeout 0 --- inspect 97     91     790   .72 0     false(unreach-call) 1 --- inspect 4.6 2.6  250 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 20    20    95 290   0      0     false(unreach-call) 1 wit inspect 19    18    450 0   0   false(unreach-call) 1 --- inspect 40     34     820   .71 0     false(unreach-call) 1 --- inspect 3.8 2.2  250 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 73    73    150 770   0      0     timeout 0 wit inspect 92    90    550 0   0   timeout 0 --- inspect 97     90     880   .72 0     false(unreach-call) 1 --- inspect 3.7 2.1  250 0     0     false(unreach-call) 1 --- inspect .60   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 42    42    120 460   0      0     false(unreach-call) 1 wit inspect 62    60    550 0   0   false(unreach-call) 1 --- inspect 60     53     920   .71 0     false(unreach-call) 1 --- inspect 4.6 2.7  250 0     0     false(unreach-call) 1 --- inspect .58   .59   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 32    32    130 360   0      0     timeout 0 wit inspect 92    90    550 0   0   timeout 0 --- inspect 97     91     920   .72 0     false(unreach-call) 1 --- inspect 3.5 2.0  250 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .053 .0041 - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.9  1.9  65 30   0      0     true -32 wit inspect 3.6  2.0  250 0   0   timeout 0 --- inspect 97     90     590   .72 0     false(unreach-call) 1 --- inspect 3.7 2.1  250 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .47 .47 61 4.3 0      0     false(unreach-call) 1 wit inspect 5.7  4.1  310 0   0   timeout 0 --- inspect 97     91     570   .72 0     false(unreach-call) 1 --- inspect 3.5 2.0  250 0     0     false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.8  1.8  65 20   0      0     true -32 wit inspect 3.7  2.0  250 0   0   timeout 0 --- inspect 97     91     610   .76 0     false(unreach-call) 1 --- inspect 4.1 2.3  250 0     0     false(unreach-call) 1 --- inspect .57   .57   20    .049 .070  - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .80 .80 61 8.8 0      0     true -32 wit inspect 3.6  2.0  250 0   0   timeout 0 --- inspect 97     91     430   1.2  0     false(unreach-call) 1 --- inspect 3.9 2.3  240 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 1.2  1.2  64 13   0      0     true -32 wit inspect 4.5  2.5  250 0   0   timeout 0 --- inspect 97     91     420   .72 0     true -32 --- inspect 4.0 2.3  250 0     0     true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 1.3  1.3  65 19   0      0     true -32 wit inspect 3.5  2.0  250 0   0   timeout 0 --- inspect 97     90     440   .72 0     true -32 --- inspect 3.6 2.1  250 0     0     true -32 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 2 wit inspect 4.9  4.9  78 62   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    610 0   0      timeout 0 --- inspect 960     950     950   .70 0   
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 2 wit inspect 5.7  5.7  78 85   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    590 0   0      timeout 0 --- inspect 960     950     780   .71 0   
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 2 wit inspect 6.2  6.2  79 81   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    610 0   0      timeout 0 --- inspect 960     950     960   .68 0   
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 2 wit inspect 15    15    120 200   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    540 0   0      timeout 0 --- inspect 960     950     900   .75 0   
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 2 wit inspect 16    16    110 200   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    850 0   0      timeout 0 --- inspect 960     950     970   1.7  0   
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 2 wit inspect 17    17    100 180   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    540 0   0      timeout 0 --- inspect 960     950     1000   .68 0   
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 2 wit inspect 15    15    100 180   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    610 0   0      timeout 0 --- inspect 960     950     1100   .77 0   
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i true 2 wit inspect 21    21    110 250   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    610 0   0      timeout 0 --- inspect 960     950     900   1.5  0   
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i true 2 wit inspect 43    43    150 440   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    590 0   0      timeout 0 --- inspect 960     950     1100   .68 0   
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 2 wit inspect 35    35    150 490   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0      timeout 0 --- inspect 960     950     1100   .68 0   
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i true 2 wit inspect 50    50    130 510   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    700 0   0      timeout 0 --- inspect 960     950     1100   .76 0   
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i true 2 wit inspect 46    46    140 580   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    700 0   0      timeout 0 --- inspect 960     950     1000   .76 0   
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i true 2 wit inspect 54    54    130 680   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0      timeout 0 --- inspect 960     950     1000   .73 0   
floats-cdfpl/sine_4_true-unreach-call_true-termination.i true 2 wit inspect 39    39    74 520   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    500 0   0      timeout 0 --- inspect 960     950     790   .73 0   
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 2 wit inspect 2.6  2.6  70 36   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    490 0   0      timeout 0 --- inspect 960     950     830   .71 0   
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 2.5  2.5  70 35   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    650 0   0      timeout 0 --- inspect 960     950     830   1.4  0   
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 2.0  2.0  71 25   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 760    760    590 0   0      timeout 0 --- inspect 960     950     850   .18 0   
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 2.6  2.6  70 38   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 490    490    540 0   0      timeout 0 --- inspect 960     950     810   .71 0   
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 190    190    86 2400   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 560    550    570 0   0      timeout (true) 0 --- inspect 950     940     780   .71 0   
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 130    130    89 1700   0      .057 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 460    450    510 0   0      timeout 0 --- inspect 960     950     760   .77 0   
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 25    25    75 330   0      .057 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 250    250    500 0   0      timeout 0 --- inspect 960     950     770   1.7  0   
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 5.9  5.9  74 72   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 880    870    480 0   0      true 2 --- inspect 590     590     780   .71 0   
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 1.3  1.3  68 16   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 59    58    360 0   0      true 2 --- inspect 85     79     610   .18 0   
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect .96 .96 81 10   .0082 .090 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  3.3  320 0   0      true 2 --- inspect 43     36     960   .71 0   
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect .95 .95 85 11   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    8.3  780 0   0      error (7) 0 --- inspect 12     7.4   290   .71 0   
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 58 3.2 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 12     7.2   300   .75 0   
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 1.5  1.5  68 20   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    18    300 0   0      true 2 --- inspect 56     47     530   .71 0   
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect .34 .34 58 3.2 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 13     8.1   290   .75 0   
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect .86 .86 69 7.5 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  270 0   0      true 2 --- inspect 20     11     450   .50 0   
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect .35 .35 58 3.3 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0      true 2 --- inspect 14     8.7   310   .68 0   
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect .35 .35 58 3.5 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0      true 2 --- inspect 12     7.1   300   .68 0   
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .74 .74 68 6.3 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  260 0   0      error (7) 0 --- inspect 14     7.7   280   .75 0   
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .73 .73 68 7.1 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 4.6  2.5  260 0   0      unknown 0 --- inspect 7.2   4.3   280   .62 0   
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .74 .74 68 7.1 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  260 0   0      true 2 --- inspect 34     27     450   .75 0   
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect .34 .34 58 3.3 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0      true 2 --- inspect 12     7.5   300   .68 0   
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 58 3.2 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 15     9.3   300   .68 0   
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 58 3.7 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 13     8.0   310   .75 0   
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 58 2.7 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  260 0   0      true 2 --- inspect 18     13     310   .68 0   
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect .37 .37 58 3.9 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 13     7.6   310   .71 0   
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .70 .70 67 8.3 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.9  2.6  280 0   0      true 2 --- inspect 15     8.4   390   .68 0   
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect .74 .75 67 6.0 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    34    630 0   0      error (7) 0 --- inspect 12     7.1   290   .75 0   
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .72 .71 67 7.2 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.9  2.7  260 0   0      true 2 --- inspect 19     11     390   .71 0   
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 58 3.0 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 13     7.3   300   .68 0   
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 59 4.2 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0      true 2 --- inspect 24     18     370   .75 0   
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect .84 .84 69 9.4 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    7.9  290 0   0      true 2 --- inspect 73     64     560   .71 0   
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect .39 .39 59 2.9 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.3  280 0   0      true 2 --- inspect 180     170     740   .68 0   
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 58 3.8 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 16     10     300   .68 0   
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect .35 .35 58 3.9 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.3  270 0   0      true 2 --- inspect 18     12     310   .75 0   
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 4.2  4.2  100 58   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 91    88    330 0   0      true 2 --- inspect 96     87     590   .71 0   
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 58 3.1 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  260 0   0      true 2 --- inspect 32     26     300   .75 0   
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect .37 .37 59 3.4 0      .057 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0      true 2 --- inspect 18     11     300   .71 0   
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 1.1  1.1  67 12   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.7  5.8  270 0   0      true 2 --- inspect 17     9.8   390   .68 0   
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect .81 .81 69 9.0 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.9  2.6  260 0   0      error (7) 0 --- inspect 12     6.9   280   .68 0   
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect .85 .85 68 7.1 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  260 0   0      true 2 --- inspect 17     10     430   .68 0   
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 .37 59 4.5 .0041 0     true -32 wit inspect 3.7  2.0  240 0   0   false(unreach-call) 1 --- inspect 15     9.2   310   .68 0     unknown 0 --- inspect 3.6 2.1  240 0     0     false(unreach-call) 1 --- inspect .60   .60   20    .057 0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c error (8) 0 --- inspect .38 .38 59 3.0 .0041 0     error (invalid witness file) 0 --- inspect .71 .44 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2 .74 47 0     0     error (invalid witness file) 0 --- inspect .0056 .0078 .53 0     0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c error (8) 0 --- inspect .36 .37 59 3.4 .0041 0     error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .026 .027 5.8 0    0     error (invalid witness file) 0 --- inspect 1.2 .77 47 0     0     error (invalid witness file) 0 --- inspect .0045 .0057 .53 0     0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 .37 59 3.3 .0041 0     false(unreach-call) 1 wit inspect 3.7  2.0  260 0   0   false(unreach-call) 1 --- inspect 14     8.5   310   .68 0     false(unreach-call) 1 --- inspect 3.6 2.1  240 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 --- inspect 900    900    270 6400   .016  0     error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0 .65 46 0     0     error (invalid witness file) 0 --- inspect .0035 .0050 .52 0     0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900    900    480 8200   .016  0     error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2 .75 48 0     0     error (invalid witness file) 0 --- inspect .0057 .0071 .58 0     0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 .37 59 3.7 .0041 0     false(unreach-call) 1 wit inspect 3.7  2.1  260 0   0   false(unreach-call) 1 --- inspect 13     8.2   300   .71 0     false(unreach-call) 1 --- inspect 3.5 2.0  250 0     0     false(unreach-call) 1 --- inspect .59   .59   20    .053 .0041 - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36 .36 59 3.7 .0041 0     false(unreach-call) 1 wit inspect 3.8  2.1  260 0   0   false(unreach-call) 1 --- inspect 13     7.5   300   .75 0     unknown 0 --- inspect 4.4 2.6  250 0     0     error (2) 0 --- inspect .58   .57   20    .037 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36 .37 59 3.0 .0041 0     false(unreach-call) 1 wit inspect 3.7  2.1  250 0   0   false(unreach-call) 1 --- inspect 16     9.6   300   .75 0     unknown 0 --- inspect 4.1 2.4  250 0     0     error (2) 0 --- inspect .56   .56   20    .037 0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .55 .55 62 6.7 .0041 .057 false(unreach-call) 1 wit inspect 7.9  5.4  380 0   0   false(unreach-call) 1 --- inspect 32     24     1000   .68 0     false(unreach-call) 1 --- inspect 4.7 2.7  260 0     0     false(unreach-call) 1 --- inspect .62   .64   20    .070 .0082 - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect .66 .66 69 7.0 .0041 0     assertion 0 --- inspect 2.9  1.6  200 0   0   false(unreach-call) 1 --- inspect 20     14     590   .71 0     assertion 0 --- inspect 3.8 2.2  200 0     0     error (2) 0 --- inspect .58   .58   20    .037 0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .47 .47 59 4.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1500 0   0      timeout 0 --- inspect 960     910     2600   .69 0   
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect .44 .45 58 3.9 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1700 0   0      timeout 0 --- inspect 960     900     4500   1.5  0   
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect .37 .37 59 3.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 30     24     990   .71 0   
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect .37 .38 59 3.2 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 16     11     430   .68 0   
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect .38 .38 59 3.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  2.0  250 0   0      true 2 --- inspect 13     7.9   300   .75 0   
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect .36 .36 59 3.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 13     7.5   300   .75 0   
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect .37 .37 59 3.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 13     7.8   290   .75 0   
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 5.2  5.2  250 78   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    26    500 0   0      error (7) 0 --- inspect 140     130     2600   .71 0   
float-benchs/bary_diverge_true-unreach-call_true-termination.c out of memory 0 --- inspect 110    110    15000 1300   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .025 .026 5.7 0    0   
float-benchs/cast_float_union_true-unreach-call.c error (8) 0 --- inspect .39 .39 59 3.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0   
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 2 wit inspect 18    18    520 200   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1300 0   0      timeout 0 --- inspect 960     950     3000   1.2  0   
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900    900    4700 6900   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 42 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0   
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900    900    4800 6100   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0   
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .36 .36 59 3.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    22    410 0   0      true 2 --- inspect 350     340     670   .71 0   
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect .36 .36 59 3.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    19    400 0   0      true 2 --- inspect 680     670     790   .71 0   
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 1.3  1.3  240 15   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 830    810    7000 0   0      timeout 0 --- inspect 960     950     1300   .73 0   
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 900    900    300 12000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0   
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 900    900    860 9300   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0   
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c timeout 0 --- inspect 900    900    1000 12000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0   
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 900    900    980 11000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0   
float-benchs/filter1_true-unreach-call_true-termination.c timeout 0 --- inspect 900    900    900 6100   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0   
float-benchs/filter2_alt_true-unreach-call.c timeout 0 --- inspect 900    900    260 10000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0   
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 --- inspect 900    900    10000 13000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0   
float-benchs/filter2_reinit_true-unreach-call_true-termination.c out of memory 0 --- inspect 630    630    15000 8200   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .020 .022 5.6 0    0   
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 --- inspect 900    900    810 10000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0   
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 --- inspect 900    900    590 9500   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .34 40 0   0      error (2) 0 --- inspect .025 .027 5.6 0    0   
float-benchs/filter_iir_true-unreach-call.c timeout 0 --- inspect 900    900    1100 11000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0   
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect .37 .37 59 3.4 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0      true 2 --- inspect 15     8.7   300   .75 0   
float-benchs/image_filter_true-unreach-call.c timeout 0 --- inspect 900    900    12000 6700   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0   
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .59 .60 75 6.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    640 0   0      timeout 0 --- inspect 960     950     1600   .74 0   
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect .61 .61 76 5.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 64    62    570 0   0      timeout 0 --- inspect 960     950     1500   .71 0   
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect .62 .62 76 6.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    39    440 0   0      timeout 0 --- inspect 960     950     1600   .69 0   
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect .57 .57 66 6.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    38    550 0   0      timeout 0 --- inspect 960     950     1500   .72 0   
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect .47 .47 66 3.9 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    26    480 0   0      timeout 0 --- inspect 960     950     1500   1.5  0   
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect .47 .48 66 5.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 70    68    480 0   0      timeout 0 --- inspect 960     950     1400   .72 0   
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect .48 .48 67 5.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    24    400 0   0      timeout 0 --- inspect 960     950     1500   1.8  0   
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect .45 .45 61 4.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    19    470 0   0      timeout 0 --- inspect 960     950     1800   .68 0   
float-benchs/inv_Newton_true-unreach-call.c timeout 0 --- inspect 900    900    220 5500   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0   
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect .73 .73 71 7.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.1  4.4  310 0   0      true 2 --- inspect 91     83     1300   .68 0   
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect .76 .76 61 9.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.6  280 0   0      true 2 --- inspect 86     78     510   .71 0   
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect .40 .40 59 3.3 .0041 0     - --- inspect - --- inspect - ---