Tool CBMC
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-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.Floats
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.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.3  9.3  54 wit timeout 91   89   340 unknown 13   7.2 340
floats-cdfpl/newton_1_5_false-unreach-call.i false(reach) 4.3  4.3  48 wit timeout 91   89   340 unknown 11   6.2 320
floats-cdfpl/newton_1_6_false-unreach-call.i false(reach) 7.2  7.2  52 wit timeout 91   89   340 unknown 12   6.7 340
floats-cdfpl/newton_1_7_false-unreach-call.i false(reach) 8.5  8.5  53 wit timeout 91   89   360 unknown 11   8.1 350
floats-cdfpl/newton_1_8_false-unreach-call.i false(reach) 9.3  9.3  55 wit timeout 91   89   350 unknown 11   7.0 330
floats-cdfpl/newton_2_6_false-unreach-call.i false(reach) 20    20    99 wit true 4.2 2.4 230 unknown 11   7.1 340
floats-cdfpl/newton_2_7_false-unreach-call.i false(reach) 80    80    180 wit true 4.9 2.8 230 unknown 11   8.2 330
floats-cdfpl/newton_2_8_false-unreach-call.i false(reach) 23    23    100 wit true 4.9 2.8 230 unknown 14   8.1 350
floats-cdfpl/newton_3_6_false-unreach-call.i false(reach) 140    140    300 wit true 4.5 2.6 230 unknown 11   6.2 350
floats-cdfpl/newton_3_7_false-unreach-call.i false(reach) 150    150    290 wit true 5.3 3.0 230 unknown 11   6.4 330
floats-cdfpl/newton_3_8_false-unreach-call.i false(reach) 120    120    250 wit true 5.0 2.9 230 unknown 13   8.2 330
floats-cdfpl/sine_1_false-unreach-call.i false(reach) .43 .44 35 wit false(reach) 11   9.1 290 unknown 11   7.1 330
floats-cdfpl/sine_2_false-unreach-call.i false(reach) 1.6  1.6  35 wit true 4.3 2.5 220 unknown 13   8.2 340
floats-cdfpl/sine_3_false-unreach-call.i false(reach) 1.8  1.8  35 wit true 3.9 2.3 210 unknown 12   6.6 350
floats-cdfpl/square_1_false-unreach-call.i false(reach) 1.2  1.2  35 wit true 3.9 2.3 220 unknown 12   6.6 360
floats-cdfpl/square_2_false-unreach-call.i false(reach) 1.8  1.8  34 wit true 4.1 2.4 220 unknown 9.9 5.4 320
floats-cdfpl/square_3_false-unreach-call.i false(reach) 8.5  8.5  45 wit true 4.7 3.0 220 unknown 9.7 6.1 330
floats-cdfpl/newton_1_1_true-unreach-call.i true 850    850    150 wit - -
floats-cdfpl/newton_1_2_true-unreach-call.i true 850    850    120 wit - -
floats-cdfpl/newton_1_3_true-unreach-call.i true 520    520    96 wit - -
floats-cdfpl/newton_2_1_true-unreach-call.i true 850    850    210 wit - -
floats-cdfpl/newton_2_2_true-unreach-call.i true 850    850    270 wit - -
floats-cdfpl/newton_2_3_true-unreach-call.i true 850    850    330 wit - -
floats-cdfpl/newton_2_4_true-unreach-call.i true 850    850    590 wit - -
floats-cdfpl/newton_2_5_true-unreach-call.i true 850    850    620 wit - -
floats-cdfpl/newton_3_1_true-unreach-call.i true 850    850    470 wit - -
floats-cdfpl/newton_3_2_true-unreach-call.i true 850    850    400 wit - -
floats-cdfpl/newton_3_3_true-unreach-call.i true 850    850    600 wit - -
floats-cdfpl/newton_3_4_true-unreach-call.i true 850    850    510 wit - -
floats-cdfpl/newton_3_5_true-unreach-call.i true 850    850    610 wit - -
floats-cdfpl/sine_4_true-unreach-call.i true 850    850    96 wit - -
floats-cdfpl/sine_5_true-unreach-call.i true 510    510    71 wit - -
floats-cdfpl/sine_6_true-unreach-call.i true 330    330    74 wit - -
floats-cdfpl/sine_7_true-unreach-call.i true 850    850    100 wit - -
floats-cdfpl/sine_8_true-unreach-call.i true 530    530    100 wit - -
floats-cdfpl/square_4_true-unreach-call.i true 850    850    120 wit - -
floats-cdfpl/square_5_true-unreach-call.i true 850    850    110 wit - -
floats-cdfpl/square_6_true-unreach-call.i true 420    420    78 wit - -
floats-cdfpl/square_7_true-unreach-call.i true 630    630    110 wit - -
floats-cdfpl/square_8_true-unreach-call.i true 14    14    36 wit - -
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 3.3  3.3  40 wit - -
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true 1.1  1.1  24 wit - -
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 14    14    35 wit - -
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true 1.1  1.2  24 wit - -
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2.6  2.7  31 wit - -
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true 1.1  1.1  24 wit - -
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true .99 1.0  24 wit - -
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2.0  2.1  30 wit - -
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2.3  2.4  31 wit - -
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2.4  2.4  31 wit - -
floats-cbmc-regression/float-to-double2_true-unreach-call.i true 1.1  1.2  24 wit - -
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true 1.2  1.2  24 wit - -
floats-cbmc-regression/float11_true-unreach-call.i true 1.1  1.1  24 wit - -
floats-cbmc-regression/float12_true-unreach-call.i true 1.2  1.2  24 wit - -
floats-cbmc-regression/float13_true-unreach-call.i true 1.1  1.1  24 wit - -
floats-cbmc-regression/float14_true-unreach-call.i true 2.1  2.2  30 wit - -
floats-cbmc-regression/float18_true-unreach-call.i true 1.4  1.5  30 wit - -
floats-cbmc-regression/float19_true-unreach-call.i true 1.8  1.8  31 wit - -
floats-cbmc-regression/float1_true-unreach-call.i true 1.0  1.1  24 wit - -
floats-cbmc-regression/float20_true-unreach-call.i true 1.2  1.2  26 wit - -
floats-cbmc-regression/float22_true-unreach-call.i true 1.1  1.1  24 wit - -
floats-cbmc-regression/float2_true-unreach-call.i true 1.1  1.2  24 wit - -
floats-cbmc-regression/float3_true-unreach-call.i true 1.4  1.4  27 wit - -
floats-cbmc-regression/float4_true-unreach-call.i true 64    64    51 wit - -
floats-cbmc-regression/float5_true-unreach-call.i true 1.1  1.1  27 wit - -
floats-cbmc-regression/float6_true-unreach-call.i true 1.1  1.1  27 wit - -
floats-cbmc-regression/float7_true-unreach-call.i true 1.0  1.0  24 wit - -
floats-cbmc-regression/float8_true-unreach-call.i true 5.0  5.1  30 wit - -
float-benchs/float_int_inv_square_false-unreach-call.c false(reach) .16 .17 25 wit false(reach) 4.7 2.8 230 unknown 12   7.8 360
float-benchs/inv_square_false-unreach-call.c false(reach) .14 .15 25 wit false(reach) 5.0 2.9 240 unknown 12   9.5 330
float-benchs/nan_double_false-unreach-call.c false(reach) .13 .14 24 wit false(reach) 4.5 2.7 230 false(reach) 12   6.9 330
float-benchs/nan_float_false-unreach-call.c false(reach) .11 .13 24 wit false(reach) 4.6 2.7 230 false(reach) 12   7.0 350
float-benchs/sin_interpolated_index_false-unreach-call.c false(reach) 3.5  3.5  200 wit unknown 5.4 3.0 250 error 9.8 5.3 340
float-benchs/inv_square_int_true-unreach-call.c true 1.3  1.3  27 wit - -
float-benchs/inv_square_true-unreach-call.c true 1.1  1.1  27 wit - -
float-benchs/nan_double_range_true-unreach-call.c true .97 1.0  24 wit - -
float-benchs/nan_float_range_true-unreach-call.c true 1.0  1.1  24 wit - -
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c error 850    850    670 wit - -
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c error 850    850    650 wit - -
float-benchs/sin_interpolated_index_true-unreach-call.c error 850    850    640 wit - -
float-benchs/sin_interpolated_smallrange_true-unreach-call.c true 850    850    4400 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 21000 21000 15000 81 540   500   5600   81 250   160   7500  
    correct results 78 18000 18000 13000 16 540   500   5600   2 250   160   7500  
        correct true 56 18000 18000 11000 11 0   0   0   0 0   0   0  
        correct false 22 600 600 2000 5 540   500   5600   2 250   160   7500  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 140) 134
Run set sv-comp16.Floats