Tool impara 0.45
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-23-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-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]]
Run set sv-comp16.Floats
Options --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.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) 9.2   9.2   73 wit false(reach) 70   68   1100 unknown 12 7.4 330
floats-cdfpl/newton_1_5_false-unreach-call.i false(reach) 10     10     76 wit false(reach) 87   85   2300 unknown 12 7.2 330
floats-cdfpl/newton_1_6_false-unreach-call.i false(reach) 15     15     85 wit false(reach) 27   25   560 unknown 13 8.7 340
floats-cdfpl/newton_1_7_false-unreach-call.i false(reach) 12     12     80 wit false(reach) 21   19   500 unknown 11 6.7 330
floats-cdfpl/newton_1_8_false-unreach-call.i false(reach) 20     20     92 wit false(reach) 14   12   400 unknown 10 6.4 320
floats-cdfpl/newton_2_6_false-unreach-call.i false(reach) 180     180     350 wit timeout 91   89   430 unknown 12 7.1 330
floats-cdfpl/newton_2_7_false-unreach-call.i false(reach) 92     92     240 wit timeout 91   89   440 unknown 12 7.3 350
floats-cdfpl/newton_2_8_false-unreach-call.i false(reach) 50     50     180 wit timeout 91   89   450 unknown 11 6.7 330
floats-cdfpl/newton_3_6_false-unreach-call.i false(reach) 680     680     1000 wit timeout 91   88   580 unknown 11 6.1 350
floats-cdfpl/newton_3_7_false-unreach-call.i false(reach) 530     530     870 wit timeout 91   89   550 unknown 12 7.9 330
floats-cdfpl/newton_3_8_false-unreach-call.i false(reach) 310     310     650 wit timeout 91   89   600 unknown 11 6.3 330
floats-cdfpl/sine_1_false-unreach-call.i false(reach) 3.2   3.2   46 wit true 4.1 2.4 220 unknown 11 7.9 330
floats-cdfpl/sine_2_false-unreach-call.i false(reach) 7.1   7.1   62 wit true 4.3 2.5 220 unknown 12 7.5 330
floats-cdfpl/sine_3_false-unreach-call.i false(reach) 7.4   7.4   53 wit true 4.4 2.6 220 unknown 11 7.3 330
floats-cdfpl/square_1_false-unreach-call.i false(reach) 4.3   4.3   49 wit true 3.9 2.3 220 unknown 12 6.7 360
floats-cdfpl/square_2_false-unreach-call.i false(reach) 5.2   5.2   50 wit true 4.1 2.5 210 unknown 10 7.7 340
floats-cdfpl/square_3_false-unreach-call.i false(reach) 6.4   6.4   53 wit true 4.3 2.6 220 unknown 10 6.3 330
floats-cdfpl/newton_1_1_true-unreach-call.i true 16     16     66 wit - -
floats-cdfpl/newton_1_2_true-unreach-call.i true 22     22     69 wit - -
floats-cdfpl/newton_1_3_true-unreach-call.i true 22     22     82 wit - -
floats-cdfpl/newton_2_1_true-unreach-call.i true 100     100     150 wit - -
floats-cdfpl/newton_2_2_true-unreach-call.i true 120     120     180 wit - -
floats-cdfpl/newton_2_3_true-unreach-call.i true 120     120     200 wit - -
floats-cdfpl/newton_2_4_true-unreach-call.i true 120     120     180 wit - -
floats-cdfpl/newton_2_5_true-unreach-call.i true 200     200     300 wit - -
floats-cdfpl/newton_3_1_true-unreach-call.i true 340     340     430 wit - -
floats-cdfpl/newton_3_2_true-unreach-call.i true 270     270     440 wit - -
floats-cdfpl/newton_3_3_true-unreach-call.i true 190     190     320 wit - -
floats-cdfpl/newton_3_4_true-unreach-call.i true 340     340     460 wit - -
floats-cdfpl/newton_3_5_true-unreach-call.i true 400     400     480 wit - -
floats-cdfpl/sine_4_true-unreach-call.i true 740     740     130 wit - -
floats-cdfpl/sine_5_true-unreach-call.i true 73     73     90 wit - -
floats-cdfpl/sine_6_true-unreach-call.i true 8.9   8.9   53 wit - -
floats-cdfpl/sine_7_true-unreach-call.i true 4.5   4.5   47 wit - -
floats-cdfpl/sine_8_true-unreach-call.i true 150     150     130 wit - -
floats-cdfpl/square_4_true-unreach-call.i true 200     200     170 wit - -
floats-cdfpl/square_5_true-unreach-call.i true 190     190     200 wit - -
floats-cdfpl/square_6_true-unreach-call.i true 56     56     120 wit - -
floats-cdfpl/square_7_true-unreach-call.i true 58     58     120 wit - -
floats-cdfpl/square_8_true-unreach-call.i true 2.2   2.2   40 wit - -
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true .57  .57  38 wit - -
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true .10  .11  22 wit - -
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 1.6   1.6   34 wit - -
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true .14  .14  22 wit - -
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true .35  .36  30 wit - -
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true .14  .14  23 wit - -
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true .095 .098 22 wit - -
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true .23  .24  29 wit - -
floats-cbmc-regression/float-rounding1_true-unreach-call.i true .33  .34  29 wit - -
floats-cbmc-regression/float-to-double1_true-unreach-call.i true .34  .35  29 wit - -
floats-cbmc-regression/float-to-double2_true-unreach-call.i true .14  .14  23 wit - -
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true .11  .11  23 wit - -
floats-cbmc-regression/float11_true-unreach-call.i true .15  .15  23 wit - -
floats-cbmc-regression/float12_true-unreach-call.i true .17  .17  23 wit - -
floats-cbmc-regression/float13_true-unreach-call.i true .16  .17  23 wit - -
floats-cbmc-regression/float14_true-unreach-call.i true .17  .18  29 wit - -
floats-cbmc-regression/float18_true-unreach-call.i true 4.7   4.7   33 wit - -
floats-cbmc-regression/float19_true-unreach-call.i true .28  .29  30 wit - -
floats-cbmc-regression/float1_true-unreach-call.i true .11  .12  23 wit - -
floats-cbmc-regression/float20_true-unreach-call.i true .28  .28  25 wit - -
floats-cbmc-regression/float22_true-unreach-call.i true .15  .15  23 wit - -
floats-cbmc-regression/float2_true-unreach-call.i true .11  .11  23 wit - -
floats-cbmc-regression/float3_true-unreach-call.i true .14  .14  22 wit - -
floats-cbmc-regression/float4_true-unreach-call.i true 7.3   7.3   37 wit - -
floats-cbmc-regression/float5_true-unreach-call.i true .14  .15  26 wit - -
floats-cbmc-regression/float6_true-unreach-call.i true .30  .30  25 wit - -
floats-cbmc-regression/float7_true-unreach-call.i true .12  .12  22 wit - -
floats-cbmc-regression/float8_true-unreach-call.i true .73  .73  31 wit - -
float-benchs/float_int_inv_square_false-unreach-call.c false(reach) .24  .25  25 wit false(reach) 5.3 3.2 240 unknown 11 7.6 330
float-benchs/inv_square_false-unreach-call.c false(reach) .19  .19  24 wit false(reach) 5.4 3.2 240 unknown 11 6.1 340
float-benchs/nan_double_false-unreach-call.c false(reach) .13  .14  23 wit false(reach) 4.4 2.7 230 false(reach) 11 6.2 330
float-benchs/nan_float_false-unreach-call.c false(reach) .10  .11  23 wit false(reach) 4.0 2.3 230 false(reach) 11 7.0 330
float-benchs/sin_interpolated_index_false-unreach-call.c false(reach) .32  .32  27 wit unknown 5.7 3.2 250 error 11 7.4 340
float-benchs/inv_square_int_true-unreach-call.c true .21  .22  27 wit - -
float-benchs/inv_square_true-unreach-call.c true .18  .19  24 wit - -
float-benchs/nan_double_range_true-unreach-call.c true .098 .10  23 wit - -
float-benchs/nan_float_range_true-unreach-call.c true .17  .17  23 wit - -
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c timeout 900     900     220 wit - -
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c timeout 900     900     230 wit - -
float-benchs/sin_interpolated_index_true-unreach-call.c timeout 900     900     180 wit - -
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 900     900     380 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 9300 9300 10000 81 810   770   10000   81 250   160   7300  
    correct results 77 5700 5700 9400 15 810   770   10000   2 250   160   7300  
        correct true 55 3800 3800 5300 6 0   0   0   0 0   0   0  
        correct false 22 1900 1900 4200 9 810   770   10000   2 250   160   7300  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 140) 132
Run set sv-comp16.Floats