Tool CPAchecker 1.4-svcomp16c
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 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]]
Run set sv-comp16.Floats
Options -sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.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) 370   370   8600 wit false(reach) 9.8 7.7 320 unknown 11 9.1 330
floats-cdfpl/newton_1_5_false-unreach-call.i false(reach) 56   54   480 wit false(reach) 10   8.0 380 unknown 12 6.5 330
floats-cdfpl/newton_1_6_false-unreach-call.i false(reach) 43   41   1200 wit false(reach) 9.7 7.7 320 unknown 14 7.8 360
floats-cdfpl/newton_1_7_false-unreach-call.i false(reach) 11   9.4 420 wit false(reach) 10   7.8 320 unknown 12 7.0 340
floats-cdfpl/newton_1_8_false-unreach-call.i false(reach) 11   8.5 400 wit false(reach) 8.7 6.8 370 unknown 12 6.7 350
floats-cdfpl/newton_2_6_false-unreach-call.i false(reach) 160   150   2900 wit false(reach) 14   12   430 unknown 13 9.5 340
floats-cdfpl/newton_2_7_false-unreach-call.i false(reach) 360   350   8800 wit false(reach) 15   13   430 unknown 12 6.7 330
floats-cdfpl/newton_2_8_false-unreach-call.i false(reach) 470   470   11000 wit false(reach) 16   14   560 unknown 11 6.5 330
floats-cdfpl/newton_3_6_false-unreach-call.i false(reach) 870   870   14000 wit false(reach) 22   20   690 unknown 12 6.4 330
floats-cdfpl/newton_3_7_false-unreach-call.i out of memory 580   580   15000 wit - -
floats-cdfpl/newton_3_8_false-unreach-call.i false(reach) 74   72   1500 wit false(reach) 22   19   690 unknown 12 6.9 340
floats-cdfpl/sine_1_false-unreach-call.i false(reach) 77   75   350 wit false(reach) 7.7 5.7 280 unknown 11 6.5 320
floats-cdfpl/sine_2_false-unreach-call.i false(reach) 160   160   5800 wit false(reach) 7.1 5.2 280 unknown 12 7.0 350
floats-cdfpl/sine_3_false-unreach-call.i false(reach) 320   320   11000 wit true 4.1 2.4 220 unknown 12 6.8 350
floats-cdfpl/square_1_false-unreach-call.i false(reach) 96   94   2200 wit true 4.5 2.6 220 unknown 11 9.2 320
floats-cdfpl/square_2_false-unreach-call.i false(reach) 79   77   1900 wit false(reach) 6.3 4.4 290 unknown 11 6.1 340
floats-cdfpl/square_3_false-unreach-call.i false(reach) 83   81   2000 wit false(reach) 6.4 4.5 280 unknown 11 6.1 330
floats-cdfpl/newton_1_1_true-unreach-call.i out of memory 660   660   15000 wit - -
floats-cdfpl/newton_1_2_true-unreach-call.i out of memory 660   660   15000 wit - -
floats-cdfpl/newton_1_3_true-unreach-call.i out of memory 610   610   15000 wit - -
floats-cdfpl/newton_2_1_true-unreach-call.i out of memory 600   600   15000 wit - -
floats-cdfpl/newton_2_2_true-unreach-call.i out of memory 650   640   15000 wit - -
floats-cdfpl/newton_2_3_true-unreach-call.i out of memory 610   610   15000 wit - -
floats-cdfpl/newton_2_4_true-unreach-call.i out of memory 630   630   15000 wit - -
floats-cdfpl/newton_2_5_true-unreach-call.i out of memory 620   620   15000 wit - -
floats-cdfpl/newton_3_1_true-unreach-call.i out of memory 600   600   15000 wit - -
floats-cdfpl/newton_3_2_true-unreach-call.i out of memory 630   630   15000 wit - -
floats-cdfpl/newton_3_3_true-unreach-call.i out of memory 570   570   15000 wit - -
floats-cdfpl/newton_3_4_true-unreach-call.i out of memory 620   610   15000 wit - -
floats-cdfpl/newton_3_5_true-unreach-call.i out of memory 610   610   15000 wit - -
floats-cdfpl/sine_4_true-unreach-call.i timeout 900   900   500 wit - -
floats-cdfpl/sine_5_true-unreach-call.i timeout 900   900   480 wit - -
floats-cdfpl/sine_6_true-unreach-call.i true 260   250   370 wit - -
floats-cdfpl/sine_7_true-unreach-call.i timeout 900   900   500 wit - -
floats-cdfpl/sine_8_true-unreach-call.i true 500   500   450 wit - -
floats-cdfpl/square_4_true-unreach-call.i true 340   340   410 wit - -
floats-cdfpl/square_5_true-unreach-call.i true 670   660   490 wit - -
floats-cdfpl/square_6_true-unreach-call.i true 270   270   410 wit - -
floats-cdfpl/square_7_true-unreach-call.i true 290   290   470 wit - -
floats-cdfpl/square_8_true-unreach-call.i true 32   30   310 wit - -
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i false(reach) 10   4.3 460 wit - -
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true 3.5 1.6 210 wit - -
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 7.1 4.6 260 wit - -
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true 3.5 1.6 220 wit - -
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 4.5 1.9 240 wit - -
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true 3.1 1.4 220 wit - -
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true 3.5 1.7 210 wit - -
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 4.8 2.1 240 wit - -
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 4.1 1.7 220 wit - -
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 4.2 1.8 230 wit - -
floats-cbmc-regression/float-to-double2_true-unreach-call.i true 3.5 1.7 210 wit - -
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true 4.0 1.9 230 wit - -
floats-cbmc-regression/float11_true-unreach-call.i true 3.0 1.4 210 wit - -
floats-cbmc-regression/float12_true-unreach-call.i true 2.8 1.3 220 wit - -
floats-cbmc-regression/float13_true-unreach-call.i true 3.6 1.7 220 wit - -
floats-cbmc-regression/float14_true-unreach-call.i true 4.1 1.7 230 wit - -
floats-cbmc-regression/float18_true-unreach-call.i true 5.8 2.4 260 wit - -
floats-cbmc-regression/float19_true-unreach-call.i true 4.0 1.7 230 wit - -
floats-cbmc-regression/float1_true-unreach-call.i true 3.0 1.4 210 wit - -
floats-cbmc-regression/float20_true-unreach-call.i true 3.9 2.0 240 wit - -
floats-cbmc-regression/float22_true-unreach-call.i true 4.1 1.7 230 wit - -
floats-cbmc-regression/float2_true-unreach-call.i true 3.6 1.7 210 wit - -
floats-cbmc-regression/float3_true-unreach-call.i false(reach) 3.8 1.9 240 wit - -
floats-cbmc-regression/float4_true-unreach-call.i true 14   12   260 wit - -
floats-cbmc-regression/float5_true-unreach-call.i true 3.1 1.5 220 wit - -
floats-cbmc-regression/float6_true-unreach-call.i true 3.9 1.9 220 wit - -
floats-cbmc-regression/float7_true-unreach-call.i false(reach) 3.7 1.8 230 wit - -
floats-cbmc-regression/float8_true-unreach-call.i true 4.7 2.3 230 wit - -
float-benchs/float_int_inv_square_false-unreach-call.c false(reach) 3.7 1.8 240 wit true 4.1 2.4 210 true 11 6.4 330
float-benchs/inv_square_false-unreach-call.c false(reach) 4.2 2.0 240 wit true 5.3 3.1 230 true 13 7.9 340
float-benchs/nan_double_false-unreach-call.c false(reach) 3.3 1.6 230 wit false(reach) 4.4 2.7 240 false(reach) 10 6.0 330
float-benchs/nan_float_false-unreach-call.c false(reach) 3.8 1.8 230 wit false(reach) 4.6 2.7 230 true 11 6.7 330
float-benchs/sin_interpolated_index_false-unreach-call.c unknown 3.8 1.6 220 wit - -
float-benchs/inv_square_int_true-unreach-call.c true 3.0 1.5 220 wit - -
float-benchs/inv_square_true-unreach-call.c true 3.1 1.5 220 wit - -
float-benchs/nan_double_range_true-unreach-call.c true 3.0 1.5 210 wit - -
float-benchs/nan_float_range_true-unreach-call.c true 2.8 1.3 210 wit - -
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c unknown 4.0 1.7 210 wit - -
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c unknown 3.4 1.5 210 wit - -
float-benchs/sin_interpolated_index_true-unreach-call.c unknown 3.3 1.5 210 wit - -
float-benchs/sin_interpolated_smallrange_true-unreach-call.c unknown 3.4 1.5 210 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 17000 17000   300000 81 190   150   7000   81 230   140   6700  
    correct results 55 5700 5600   83000 20 190   150   7000   4 230   140   6700  
        correct true 35 2500 2400   9200 4 0   0   0   3 0   0   0  
        correct false 20 3200 3200   73000 16 190   150   7000   1 230   140   6700  
    incorrect results 3 18 8.0 930 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 3 18 8.0 930 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 140) 42
Run set sv-comp16.Floats