Tool 2LS 0.3.4
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-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]]
Run set sv-comp16.Floats
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.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) 3.1   3.1   55 wit timeout 91   89   510 unknown 11   7.0 330
floats-cdfpl/newton_1_5_false-unreach-call.i false(reach) 2.8   2.8   55 wit false(reach) 40   38   1000 unknown 12   6.5 350
floats-cdfpl/newton_1_6_false-unreach-call.i false(reach) 3.2   3.2   56 wit false(reach) 12   10   380 unknown 10   6.4 330
floats-cdfpl/newton_1_7_false-unreach-call.i false(reach) 4.5   4.5   57 wit false(reach) 31   29   520 unknown 11   6.5 330
floats-cdfpl/newton_1_8_false-unreach-call.i false(reach) 2.4   2.4   54 wit false(reach) 14   12   410 unknown 11   6.2 340
floats-cdfpl/newton_2_6_false-unreach-call.i false(reach) 14     14     120 wit true 4.9 2.8 240 unknown 13   8.3 330
floats-cdfpl/newton_2_7_false-unreach-call.i false(reach) 20     20     140 wit true 4.8 2.8 230 unknown 13   8.1 360
floats-cdfpl/newton_2_8_false-unreach-call.i false(reach) 18     18     130 wit true 5.5 3.1 240 unknown 12   7.9 330
floats-cdfpl/newton_3_6_false-unreach-call.i false(reach) 35     35     190 wit true 5.4 3.1 250 unknown 14   7.3 350
floats-cdfpl/newton_3_7_false-unreach-call.i false(reach) 39     39     190 wit true 5.8 3.2 260 unknown 12   7.6 330
floats-cdfpl/newton_3_8_false-unreach-call.i false(reach) 13     13     140 wit true 6.1 3.3 250 unknown 13   9.5 340
floats-cdfpl/sine_1_false-unreach-call.i false(reach) 1.6   1.7   41 wit timeout 91   89   330 unknown 10   6.0 330
floats-cdfpl/sine_2_false-unreach-call.i false(reach) .50  .50  37 wit timeout 91   89   2500 unknown 9.2 5.5 330
floats-cdfpl/sine_3_false-unreach-call.i false(reach) 2.3   2.3   40 wit timeout 91   89   2600 unknown 11   5.8 330
floats-cdfpl/square_1_false-unreach-call.i false(reach) 1.5   1.5   39 wit timeout 91   89   1300 unknown 13   8.7 340
floats-cdfpl/square_2_false-unreach-call.i false(reach) 1.5   1.5   37 wit timeout (false(reach)) 91   89   1900 unknown 11   6.0 350
floats-cdfpl/square_3_false-unreach-call.i false(reach) 1.1   1.1   38 wit timeout 91   89   1400 unknown 11   6.7 330
floats-cdfpl/newton_1_1_true-unreach-call.i true 7.6   7.6   60 wit - -
floats-cdfpl/newton_1_2_true-unreach-call.i true 9.8   9.8   65 wit - -
floats-cdfpl/newton_1_3_true-unreach-call.i true 10     10     73 wit - -
floats-cdfpl/newton_2_1_true-unreach-call.i true 23     23     130 wit - -
floats-cdfpl/newton_2_2_true-unreach-call.i true 22     22     130 wit - -
floats-cdfpl/newton_2_3_true-unreach-call.i true 26     26     130 wit - -
floats-cdfpl/newton_2_4_true-unreach-call.i true 36     36     130 wit - -
floats-cdfpl/newton_2_5_true-unreach-call.i true 38     38     130 wit - -
floats-cdfpl/newton_3_1_true-unreach-call.i true 57     57     220 wit - -
floats-cdfpl/newton_3_2_true-unreach-call.i true 85     85     220 wit - -
floats-cdfpl/newton_3_3_true-unreach-call.i true 80     80     190 wit - -
floats-cdfpl/newton_3_4_true-unreach-call.i true 77     77     190 wit - -
floats-cdfpl/newton_3_5_true-unreach-call.i true 79     79     210 wit - -
floats-cdfpl/sine_4_true-unreach-call.i true 38     38     49 wit - -
floats-cdfpl/sine_5_true-unreach-call.i true 2.0   2.0   40 wit - -
floats-cdfpl/sine_6_true-unreach-call.i true 2.6   2.6   41 wit - -
floats-cdfpl/sine_7_true-unreach-call.i true 1.9   1.9   39 wit - -
floats-cdfpl/sine_8_true-unreach-call.i true 1.6   1.6   40 wit - -
floats-cdfpl/square_4_true-unreach-call.i true 190     190     90 wit - -
floats-cdfpl/square_5_true-unreach-call.i true 200     200     81 wit - -
floats-cdfpl/square_6_true-unreach-call.i true 72     72     78 wit - -
floats-cdfpl/square_7_true-unreach-call.i true 6.9   6.9   45 wit - -
floats-cdfpl/square_8_true-unreach-call.i true 1.1   1.1   37 wit - -
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true .67  .67  52 wit - -
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true .10  .10  22 wit - -
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2.2   2.2   37 wit - -
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true .12  .12  24 wit - -
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true .29  .29  31 wit - -
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true .081 .084 23 wit - -
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true .11  .11  23 wit - -
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true .28  .29  29 wit - -
floats-cbmc-regression/float-rounding1_true-unreach-call.i true .26  .27  29 wit - -
floats-cbmc-regression/float-to-double1_true-unreach-call.i true .27  .28  29 wit - -
floats-cbmc-regression/float-to-double2_true-unreach-call.i true .10  .10  22 wit - -
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true .13  .13  23 wit - -
floats-cbmc-regression/float11_true-unreach-call.i true .12  .13  23 wit - -
floats-cbmc-regression/float12_true-unreach-call.i true .15  .15  23 wit - -
floats-cbmc-regression/float13_true-unreach-call.i true .13  .13  24 wit - -
floats-cbmc-regression/float14_true-unreach-call.i true .18  .19  29 wit - -
floats-cbmc-regression/float18_true-unreach-call.i timeout 900     900     1200 wit - -
floats-cbmc-regression/float19_true-unreach-call.i true .24  .24  29 wit - -
floats-cbmc-regression/float1_true-unreach-call.i true .13  .13  23 wit - -
floats-cbmc-regression/float20_true-unreach-call.i true .15  .15  28 wit - -
floats-cbmc-regression/float22_true-unreach-call.i true .11  .11  23 wit - -
floats-cbmc-regression/float2_true-unreach-call.i true .079 .082 22 wit - -
floats-cbmc-regression/float3_true-unreach-call.i true .13  .13  25 wit - -
floats-cbmc-regression/float4_true-unreach-call.i true 25     25     65 wit - -
floats-cbmc-regression/float5_true-unreach-call.i true .17  .17  26 wit - -
floats-cbmc-regression/float6_true-unreach-call.i true .11  .11  24 wit - -
floats-cbmc-regression/float7_true-unreach-call.i true .12  .13  23 wit - -
floats-cbmc-regression/float8_true-unreach-call.i true .65  .65  29 wit - -
float-benchs/float_int_inv_square_false-unreach-call.c false(reach) .15  .15  29 wit false(reach) 5.1 3.0 240 unknown 11   6.7 340
float-benchs/inv_square_false-unreach-call.c false(reach) .18  .19  28 wit false(reach) 4.7 2.7 250 unknown 11   6.1 330
float-benchs/nan_double_false-unreach-call.c false(reach) .11  .11  23 wit false(reach) 4.2 2.5 230 false(reach) 9.9 5.8 320
float-benchs/nan_float_false-unreach-call.c false(reach) .11  .11  23 wit false(reach) 4.0 2.4 230 false(reach) 11   6.7 350
float-benchs/sin_interpolated_index_false-unreach-call.c false(reach) 5.9   5.9   270 wit unknown 5.3 3.0 240 error 10   5.9 320
float-benchs/inv_square_int_true-unreach-call.c true .12  .12  28 wit - -
float-benchs/inv_square_true-unreach-call.c true .17  .17  26 wit - -
float-benchs/nan_double_range_true-unreach-call.c true .14  .15  23 wit - -
float-benchs/nan_float_range_true-unreach-call.c true .13  .13  23 wit - -
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c true 870     870     320 wit - -
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c true 760     760     320 wit - -
float-benchs/sin_interpolated_index_true-unreach-call.c true 650     650     310 wit - -
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 900     900     310 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 5300 5300 7500 81 790   740   16000   81 250   150   7400  
    correct results 79 3500 3500 6000 14 790   740   16000   2 250   150   7400  
        correct true 57 3400 3400 4200 6 0   0   0   0 0   0   0  
        correct false 22 170 170 1800 8 790   740   16000   2 250   150   7400  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 140) 136
Run set sv-comp16.Floats