Tool Ceagle AbsRef 1.0.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-04 05:59:47 CET [[ 2016-01-15 08:28:20 CET ]] [[ 2016-01-15 21:58:46 CET ]]
Run set sv-comp16.Floats
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ceagle-absref.2016-01-04_0559.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ceagle-absref.2016-01-04_0559.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
floats-cdfpl/newton_1_4_false-unreach-call.i false(reach) .089 .12  5.7 wit true 4.4 2.7 220 true 11 6.8 340
floats-cdfpl/newton_1_5_false-unreach-call.i false(reach) .10  .13  5.9 wit true 4.2 2.5 210 true 12 7.6 330
floats-cdfpl/newton_1_6_false-unreach-call.i false(reach) .091 .11  5.9 wit true 4.6 2.7 230 true 13 7.3 360
floats-cdfpl/newton_1_7_false-unreach-call.i false(reach) .14  .17  5.7 wit true 4.4 2.6 230 true 11 6.6 320
floats-cdfpl/newton_1_8_false-unreach-call.i false(reach) .093 .11  5.9 wit true 4.4 2.6 220 true 11 7.5 320
floats-cdfpl/newton_2_6_false-unreach-call.i false(reach) .38  .41  7.8 wit true 4.3 2.6 220 true 11 5.8 330
floats-cdfpl/newton_2_7_false-unreach-call.i false(reach) .28  .31  8.1 wit true 4.4 2.6 220 true 10 6.6 320
floats-cdfpl/newton_2_8_false-unreach-call.i false(reach) .37  .40  7.8 wit true 4.6 2.8 230 true 11 7.5 320
floats-cdfpl/newton_3_6_false-unreach-call.i timeout 900     900     150   wit - -
floats-cdfpl/newton_3_7_false-unreach-call.i timeout 900     900     150   wit - -
floats-cdfpl/newton_3_8_false-unreach-call.i timeout 900     900     180   wit - -
floats-cdfpl/sine_1_false-unreach-call.i false(reach) 4.0   4.0   110   wit true 4.6 2.7 220 true 10 6.0 320
floats-cdfpl/sine_2_false-unreach-call.i false(reach) 52     52     380   wit true 4.5 2.7 220 true 11 6.5 320
floats-cdfpl/sine_3_false-unreach-call.i false(reach) 50     50     380   wit true 4.6 2.6 220 true 11 6.1 310
floats-cdfpl/square_1_false-unreach-call.i false(reach) 55     55     140   wit true 4.1 2.5 220 true 11 6.5 320
floats-cdfpl/square_2_false-unreach-call.i false(reach) 65     65     140   wit true 4.2 2.5 220 true 11 7.2 310
floats-cdfpl/square_3_false-unreach-call.i false(reach) 60     60     140   wit true 4.4 2.7 230 true 11 6.7 320
floats-cdfpl/newton_1_1_true-unreach-call.i true .099 .12  5.7 wit - -
floats-cdfpl/newton_1_2_true-unreach-call.i true .078 .10  5.9 wit - -
floats-cdfpl/newton_1_3_true-unreach-call.i true .18  .26  21   wit - -
floats-cdfpl/newton_2_1_true-unreach-call.i true .40  .43  8.9 wit - -
floats-cdfpl/newton_2_2_true-unreach-call.i true .43  .46  8.9 wit - -
floats-cdfpl/newton_2_3_true-unreach-call.i true .46  .49  8.9 wit - -
floats-cdfpl/newton_2_4_true-unreach-call.i true .40  .43  9.0 wit - -
floats-cdfpl/newton_2_5_true-unreach-call.i true .41  .44  8.9 wit - -
floats-cdfpl/newton_3_1_true-unreach-call.i timeout 900     900     150   wit - -
floats-cdfpl/newton_3_2_true-unreach-call.i timeout 900     900     150   wit - -
floats-cdfpl/newton_3_3_true-unreach-call.i timeout 900     900     150   wit - -
floats-cdfpl/newton_3_4_true-unreach-call.i timeout 900     900     150   wit - -
floats-cdfpl/newton_3_5_true-unreach-call.i timeout 900     900     160   wit - -
floats-cdfpl/sine_4_true-unreach-call.i true 470     470     400   wit - -
floats-cdfpl/sine_5_true-unreach-call.i true 240     240     400   wit - -
floats-cdfpl/sine_6_true-unreach-call.i true 220     220     400   wit - -
floats-cdfpl/sine_7_true-unreach-call.i true 160     160     400   wit - -
floats-cdfpl/sine_8_true-unreach-call.i true 180     180     390   wit - -
floats-cdfpl/square_4_true-unreach-call.i true 210     210     150   wit - -
floats-cdfpl/square_5_true-unreach-call.i true 170     170     140   wit - -
floats-cdfpl/square_6_true-unreach-call.i true 200     200     140   wit - -
floats-cdfpl/square_7_true-unreach-call.i true 160     160     140   wit - -
floats-cdfpl/square_8_true-unreach-call.i true 77     77     130   wit - -
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 1.5   1.5   19   wit - -
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true .082 .10  5.9 wit - -
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 4.4   4.4   120   wit - -
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true .077 .10  5.7 wit - -
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 1.1   1.1   11   wit - -
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true .094 .12  5.9 wit - -
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true .072 .093 5.9 wit - -
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true .17  .20  6.1 wit - -
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown .10  .13  6.1 wit - -
floats-cbmc-regression/float-to-double1_true-unreach-call.i true .23  .25  31   wit - -
floats-cbmc-regression/float-to-double2_true-unreach-call.i true .058 .080 5.9 wit - -
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true .078 .10  5.7 wit - -
floats-cbmc-regression/float11_true-unreach-call.i true .082 .11  6.0 wit - -
floats-cbmc-regression/float12_true-unreach-call.i true .54  .57  54   wit - -
floats-cbmc-regression/float13_true-unreach-call.i true .23  .25  5.9 wit - -
floats-cbmc-regression/float14_true-unreach-call.i true .12  .14  6.0 wit - -
floats-cbmc-regression/float18_true-unreach-call.i true .15  .17  6.0 wit - -
floats-cbmc-regression/float19_true-unreach-call.i true .32  .35  17   wit - -
floats-cbmc-regression/float1_true-unreach-call.i true .076 .10  5.9 wit - -
floats-cbmc-regression/float20_true-unreach-call.i true .35  .38  17   wit - -
floats-cbmc-regression/float22_true-unreach-call.i true .19  .22  5.9 wit - -
floats-cbmc-regression/float2_true-unreach-call.i true .070 .091 6.1 wit - -
floats-cbmc-regression/float3_true-unreach-call.i true .49  .52  94   wit - -
floats-cbmc-regression/float4_true-unreach-call.i true 44     44     150   wit - -
floats-cbmc-regression/float5_true-unreach-call.i true .17  .20  32   wit - -
floats-cbmc-regression/float6_true-unreach-call.i true 1.7   1.7   12   wit - -
floats-cbmc-regression/float7_true-unreach-call.i true .13  .16  17   wit - -
floats-cbmc-regression/float8_true-unreach-call.i true .15  .17  6.5 wit - -
float-benchs/float_int_inv_square_false-unreach-call.c false(reach) .085 .10  5.6 wit true 4.8 2.8 230 true 12 6.5 330
float-benchs/inv_square_false-unreach-call.c false(reach) .083 .11  9.3 wit true 4.3 2.5 210 true 11 7.5 320
float-benchs/nan_double_false-unreach-call.c false(reach) .055 .081 5.9 wit true 4.1 2.5 210 true 10 7.6 310
float-benchs/nan_float_false-unreach-call.c false(reach) .076 .10  5.9 wit true 4.0 2.4 210 true 11 7.5 320
float-benchs/sin_interpolated_index_false-unreach-call.c unknown .24  .26  6.1 wit - -
float-benchs/inv_square_int_true-unreach-call.c true .13  .15  5.7 wit - -
float-benchs/inv_square_true-unreach-call.c true .33  .35  11   wit - -
float-benchs/nan_double_range_true-unreach-call.c true .11  .13  6.4 wit - -
float-benchs/nan_float_range_true-unreach-call.c true .16  .18  28   wit - -
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c true .20  .22  6.0 wit - -
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c true .29  .32  5.7 wit - -
float-benchs/sin_interpolated_index_true-unreach-call.c true .26  .28  5.6 wit - -
float-benchs/sin_interpolated_smallrange_true-unreach-call.c true .26  .29  6.0 wit - -
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 81 9600 9600 6100 81 79   47   4000   81 200   120   5800  
    correct results 71 2400 2400 4900 18 79   47   4000   18 200   120   5800  
        correct true 53 2100 2200 3500 18 0   0   0   18 0   0   0  
        correct false 18 290 290 1400 0 79   47   4000   0 200   120   5800  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 140) 124
Run set sv-comp16.Floats