Tool Ceagle 1.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus02; zeus04; zeus05; zeus06; zeus07; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus17; zeus19; zeus20; zeus21; 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-03 23:39:46 CET [[ 2016-01-15 08:27:56 CET ]] [[ 2016-01-15 21:58:29 CET ]]
Run set sv-comp16
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ceagle.2016-01-03_2339.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ceagle.2016-01-03_2339.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) .46  .54  8.0 wit true 4.6 2.6 230 true 10 5.9 340
floats-cdfpl/newton_1_5_false-unreach-call.i false(reach) .55  .62  8.0 wit true 4.6 2.6 230 true 10 5.7 330
floats-cdfpl/newton_1_6_false-unreach-call.i false(reach) .40  .47  8.1 wit true 4.1 2.5 220 true 11 6.5 320
floats-cdfpl/newton_1_7_false-unreach-call.i false(reach) .33  .39  8.0 wit true 4.3 2.5 220 true 11 6.3 330
floats-cdfpl/newton_1_8_false-unreach-call.i false(reach) .30  .37  8.2 wit true 4.2 2.5 220 true 11 6.5 330
floats-cdfpl/newton_2_6_false-unreach-call.i false(reach) .57  .63  9.2 wit true 4.3 2.5 220 true 11 6.4 330
floats-cdfpl/newton_2_7_false-unreach-call.i false(reach) .86  .93  9.3 wit true 4.6 2.6 220 true 11 6.6 330
floats-cdfpl/newton_2_8_false-unreach-call.i false(reach) .88  .95  9.5 wit true 4.8 2.8 230 true 11 6.2 330
floats-cdfpl/newton_3_6_false-unreach-call.i false(reach) 150     150     45   wit true 4.3 2.6 220 true 13 6.8 350
floats-cdfpl/newton_3_7_false-unreach-call.i false(reach) 150     150     45   wit true 4.5 2.7 230 true 13 6.9 360
floats-cdfpl/newton_3_8_false-unreach-call.i false(reach) 150     150     44   wit true 4.8 2.8 230 true 11 6.5 330
floats-cdfpl/sine_1_false-unreach-call.i unknown .047 .073 6.1 wit - -
floats-cdfpl/sine_2_false-unreach-call.i unknown .051 .084 6.2 wit - -
floats-cdfpl/sine_3_false-unreach-call.i unknown .086 .12  5.9 wit - -
floats-cdfpl/square_1_false-unreach-call.i false(reach) 21     21     110   wit true 4.7 2.8 230 true 11 6.3 320
floats-cdfpl/square_2_false-unreach-call.i false(reach) 8.0   8.0   100   wit true 4.5 2.6 230 true 10 5.7 310
floats-cdfpl/square_3_false-unreach-call.i false(reach) 81     81     110   wit true 4.6 2.6 230 true 10 6.1 300
floats-cdfpl/newton_1_1_true-unreach-call.i true .19  .21  8.1 wit - -
floats-cdfpl/newton_1_2_true-unreach-call.i true .15  .17  7.9 wit - -
floats-cdfpl/newton_1_3_true-unreach-call.i true .14  .17  8.0 wit - -
floats-cdfpl/newton_2_1_true-unreach-call.i true .43  .45  9.6 wit - -
floats-cdfpl/newton_2_2_true-unreach-call.i true .41  .43  9.5 wit - -
floats-cdfpl/newton_2_3_true-unreach-call.i true .29  .33  11   wit - -
floats-cdfpl/newton_2_4_true-unreach-call.i true .41  .43  9.3 wit - -
floats-cdfpl/newton_2_5_true-unreach-call.i true .10  .14  6.4 wit - -
floats-cdfpl/newton_3_1_true-unreach-call.i true 150     150     42   wit - -
floats-cdfpl/newton_3_2_true-unreach-call.i true 150     150     43   wit - -
floats-cdfpl/newton_3_3_true-unreach-call.i true 150     150     43   wit - -
floats-cdfpl/newton_3_4_true-unreach-call.i true 150     150     44   wit - -
floats-cdfpl/newton_3_5_true-unreach-call.i true 150     150     46   wit - -
floats-cdfpl/sine_4_true-unreach-call.i true 350     350     200   wit - -
floats-cdfpl/sine_5_true-unreach-call.i true 380     380     200   wit - -
floats-cdfpl/sine_6_true-unreach-call.i true 390     390     200   wit - -
floats-cdfpl/sine_7_true-unreach-call.i true 220     220     190   wit - -
floats-cdfpl/sine_8_true-unreach-call.i true 240     240     190   wit - -
floats-cdfpl/square_4_true-unreach-call.i true 250     250     120   wit - -
floats-cdfpl/square_5_true-unreach-call.i true 200     200     120   wit - -
floats-cdfpl/square_6_true-unreach-call.i true 150     150     120   wit - -
floats-cdfpl/square_7_true-unreach-call.i true 150     150     110   wit - -
floats-cdfpl/square_8_true-unreach-call.i true 59     59     110   wit - -
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true .19  .22  6.6 wit - -
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true .11  .13  7.6 wit - -
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true .58  .27  32   wit - -
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true .13  .16  7.7 wit - -
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true .82  .75  18   wit - -
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true .14  .17  7.6 wit - -
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true .085 .11  7.5 wit - -
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true .23  .27  7.5 wit - -
floats-cbmc-regression/float-rounding1_true-unreach-call.i true .083 .11  6.6 wit - -
floats-cbmc-regression/float-to-double1_true-unreach-call.i true .49  .45  8.1 wit - -
floats-cbmc-regression/float-to-double2_true-unreach-call.i true .065 .097 7.3 wit - -
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true .081 .10  6.2 wit - -
floats-cbmc-regression/float11_true-unreach-call.i true .073 .095 6.2 wit - -
floats-cbmc-regression/float12_true-unreach-call.i true .32  .56  15   wit - -
floats-cbmc-regression/float13_true-unreach-call.i true .47  .51  8.0 wit - -
floats-cbmc-regression/float14_true-unreach-call.i true .37  .35  7.8 wit - -
floats-cbmc-regression/float18_true-unreach-call.i true .59  .64  8.4 wit - -
floats-cbmc-regression/float19_true-unreach-call.i true .22  .23  7.5 wit - -
floats-cbmc-regression/float1_true-unreach-call.i true .15  .18  7.7 wit - -
floats-cbmc-regression/float20_true-unreach-call.i true .49  .52  25   wit - -
floats-cbmc-regression/float22_true-unreach-call.i true .11  .14  6.3 wit - -
floats-cbmc-regression/float2_true-unreach-call.i true .22  .26  7.7 wit - -
floats-cbmc-regression/float3_true-unreach-call.i true .18  .21  7.8 wit - -
floats-cbmc-regression/float4_true-unreach-call.i true 3.1   .62  97   wit - -
floats-cbmc-regression/float5_true-unreach-call.i true .46  .49  17   wit - -
floats-cbmc-regression/float6_true-unreach-call.i true 1.0   1.1   16   wit - -
floats-cbmc-regression/float7_true-unreach-call.i true .093 .12  7.4 wit - -
floats-cbmc-regression/float8_true-unreach-call.i true .16  .19  9.0 wit - -
float-benchs/float_int_inv_square_false-unreach-call.c false(reach) .14  .20  7.6 wit true 4.4 2.6 220 true 11 6.0 330
float-benchs/inv_square_false-unreach-call.c false(reach) .46  .52  12   wit true 4.4 2.5 230 true 10 6.2 310
float-benchs/nan_double_false-unreach-call.c false(reach) .14  .18  7.9 wit true 4.1 2.5 210 true 11 6.3 320
float-benchs/nan_float_false-unreach-call.c false(reach) .18  .22  7.8 wit true 4.2 2.5 210 true 11 6.0 310
float-benchs/sin_interpolated_index_false-unreach-call.c unknown .12  .15  6.4 wit - -
float-benchs/inv_square_int_true-unreach-call.c true .30  .32  14   wit - -
float-benchs/inv_square_true-unreach-call.c true .84  .87  14   wit - -
float-benchs/nan_double_range_true-unreach-call.c true .18  .20  8.5 wit - -
float-benchs/nan_float_range_true-unreach-call.c true .18  .20  13   wit - -
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c true .10  .13  6.0 wit - -
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c true .17  .20  6.4 wit - -
float-benchs/sin_interpolated_index_true-unreach-call.c true .20  .23  6.2 wit - -
float-benchs/sin_interpolated_smallrange_true-unreach-call.c true .10  .13  6.1 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 3700 3700 2900 81 80   47   4000   81 200   110   5900  
local summary 900
    correct results 77 3700 3700 2900 18 80   47   4000   18 200   110   5900  
        correct true 59 3200 3200 2300 18 0   0   0   18 0   0   0  
        correct false 18 570 570 560 0 80   47   4000   0 200   110   5900  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 140) 136
Run set sv-comp16