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 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.Floats
Options -sv-comp16 -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-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.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) 16   14   300 wit false(reach) 85   83   1400 unknown 12   7.9 340
floats-cdfpl/newton_1_5_false-unreach-call.i false(reach) 16   14   300 wit false(reach) 29   27   440 unknown 13   9.7 340
floats-cdfpl/newton_1_6_false-unreach-call.i false(reach) 7.4 5.4 300 wit false(reach) 22   19   570 unknown 11   6.1 330
floats-cdfpl/newton_1_7_false-unreach-call.i false(reach) 8.5 6.5 300 wit false(reach) 48   45   970 unknown 12   6.8 330
floats-cdfpl/newton_1_8_false-unreach-call.i false(reach) 7.1 5.0 300 wit false(reach) 16   14   440 unknown 11   6.2 320
floats-cdfpl/newton_2_6_false-unreach-call.i false(reach) 12   10   400 wit timeout 91   89   1900 unknown 12   6.5 340
floats-cdfpl/newton_2_7_false-unreach-call.i false(reach) 8.2 6.4 400 wit timeout 91   89   1800 unknown 11   8.1 320
floats-cdfpl/newton_2_8_false-unreach-call.i false(reach) 8.4 6.5 400 wit timeout 91   89   2000 unknown 13   10   360
floats-cdfpl/newton_3_6_false-unreach-call.i false(reach) 21   19   510 wit timeout 91   89   2100 unknown 12   6.6 340
floats-cdfpl/newton_3_7_false-unreach-call.i false(reach) 19   17   510 wit false(reach) 61   58   990 unknown 12   6.9 320
floats-cdfpl/newton_3_8_false-unreach-call.i false(reach) 68   65   530 wit timeout 91   88   550 unknown 12   6.5 330
floats-cdfpl/sine_1_false-unreach-call.i false(reach) 39   37   300 wit timeout 91   89   660 unknown 12   8.8 330
floats-cdfpl/sine_2_false-unreach-call.i false(reach) 4.4 2.7 270 wit false(reach) 55   53   1300 unknown 11   6.0 340
floats-cdfpl/sine_3_false-unreach-call.i false(reach) 33   32   280 wit timeout 91   89   950 unknown 11   6.3 330
floats-cdfpl/square_1_false-unreach-call.i false(reach) 87   84   500 wit false(reach) 6.3 4.5 290 unknown 13   9.0 340
floats-cdfpl/square_2_false-unreach-call.i false(reach) 87   84   490 wit false(reach) 6.2 4.4 300 unknown 12   6.5 340
floats-cdfpl/square_3_false-unreach-call.i false(reach) 78   75   480 wit false(reach) 6.4 4.4 270 unknown 11   6.7 330
floats-cdfpl/newton_1_1_true-unreach-call.i timeout 900   900   530 wit - -
floats-cdfpl/newton_1_2_true-unreach-call.i timeout 900   900   640 wit - -
floats-cdfpl/newton_1_3_true-unreach-call.i timeout 900   900   640 wit - -
floats-cdfpl/newton_2_1_true-unreach-call.i timeout 900   900   590 wit - -
floats-cdfpl/newton_2_2_true-unreach-call.i timeout 900   900   690 wit - -
floats-cdfpl/newton_2_3_true-unreach-call.i timeout 900   900   700 wit - -
floats-cdfpl/newton_2_4_true-unreach-call.i timeout 900   900   740 wit - -
floats-cdfpl/newton_2_5_true-unreach-call.i timeout 900   900   600 wit - -
floats-cdfpl/newton_3_1_true-unreach-call.i timeout 900   900   730 wit - -
floats-cdfpl/newton_3_2_true-unreach-call.i timeout 900   900   710 wit - -
floats-cdfpl/newton_3_3_true-unreach-call.i timeout 900   900   800 wit - -
floats-cdfpl/newton_3_4_true-unreach-call.i timeout 900   900   660 wit - -
floats-cdfpl/newton_3_5_true-unreach-call.i timeout 900   900   680 wit - -
floats-cdfpl/sine_4_true-unreach-call.i timeout 900   900   580 wit - -
floats-cdfpl/sine_5_true-unreach-call.i timeout 900   900   450 wit - -
floats-cdfpl/sine_6_true-unreach-call.i true 410   410   400 wit - -
floats-cdfpl/sine_7_true-unreach-call.i timeout 900   900   540 wit - -
floats-cdfpl/sine_8_true-unreach-call.i timeout 900   900   570 wit - -
floats-cdfpl/square_4_true-unreach-call.i true 680   680   470 wit - -
floats-cdfpl/square_5_true-unreach-call.i timeout 900   900   620 wit - -
floats-cdfpl/square_6_true-unreach-call.i true 310   300   430 wit - -
floats-cdfpl/square_7_true-unreach-call.i true 330   330   500 wit - -
floats-cdfpl/square_8_true-unreach-call.i true 73   71   340 wit - -
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i false(reach) 300   290   930 wit - -
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true 2.6 1.2 180 wit - -
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 15   9.8 350 wit - -
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true 3.2 1.5 180 wit - -
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 9.8 2.9 370 wit - -
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true 3.1 1.4 180 wit - -
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true 3.1 1.4 180 wit - -
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 7.4 2.4 330 wit - -
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 9.7 3.0 400 wit - -
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 8.5 2.7 370 wit - -
floats-cbmc-regression/float-to-double2_true-unreach-call.i true 3.1 1.4 180 wit - -
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true 3.2 1.5 190 wit - -
floats-cbmc-regression/float11_true-unreach-call.i true 3.2 1.5 190 wit - -
floats-cbmc-regression/float12_true-unreach-call.i true 4.4 1.9 230 wit - -
floats-cbmc-regression/float13_true-unreach-call.i true 3.2 1.5 180 wit - -
floats-cbmc-regression/float14_true-unreach-call.i true 4.3 1.7 200 wit - -
floats-cbmc-regression/float18_true-unreach-call.i true 4.5 1.8 210 wit - -
floats-cbmc-regression/float19_true-unreach-call.i true 8.4 2.7 330 wit - -
floats-cbmc-regression/float1_true-unreach-call.i true 3.1 1.5 180 wit - -
floats-cbmc-regression/float20_true-unreach-call.i true 3.3 1.5 180 wit - -
floats-cbmc-regression/float22_true-unreach-call.i true 3.4 1.5 190 wit - -
floats-cbmc-regression/float2_true-unreach-call.i true 3.2 1.4 180 wit - -
floats-cbmc-regression/float3_true-unreach-call.i true 2.7 1.2 180 wit - -
floats-cbmc-regression/float4_true-unreach-call.i true 48   43   380 wit - -
floats-cbmc-regression/float5_true-unreach-call.i true 2.8 1.3 180 wit - -
floats-cbmc-regression/float6_true-unreach-call.i true 3.4 1.5 190 wit - -
floats-cbmc-regression/float7_true-unreach-call.i true 3.2 1.4 190 wit - -
floats-cbmc-regression/float8_true-unreach-call.i true 10   4.4 370 wit - -
float-benchs/float_int_inv_square_false-unreach-call.c false(reach) 3.9 1.8 210 wit false(reach) 4.9 3.0 240 true 9.6 5.3 320
float-benchs/inv_square_false-unreach-call.c false(reach) 3.8 1.8 210 wit false(reach) 5.1 3.0 240 true 12   6.5 330
float-benchs/nan_double_false-unreach-call.c false(reach) 3.6 1.7 210 wit false(reach) 4.4 2.6 230 false(reach) 12   7.5 350
float-benchs/nan_float_false-unreach-call.c false(reach) 3.6 1.7 210 wit false(reach) 4.6 2.7 220 true 11   6.4 320
float-benchs/sin_interpolated_index_false-unreach-call.c unknown 6.6 2.3 310 wit - -
float-benchs/inv_square_int_true-unreach-call.c true 5.1 2.3 240 wit - -
float-benchs/inv_square_true-unreach-call.c true 4.4 1.9 250 wit - -
float-benchs/nan_double_range_true-unreach-call.c true 4.3 1.9 240 wit - -
float-benchs/nan_float_range_true-unreach-call.c true 4.5 2.0 240 wit - -
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c unknown 7.4 2.5 390 wit - -
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c unknown 7.3 2.5 390 wit - -
float-benchs/sin_interpolated_index_true-unreach-call.c unknown 6.9 2.4 320 wit - -
float-benchs/sin_interpolated_smallrange_true-unreach-call.c unknown 6.9 2.4 390 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 19000 19000 31000 81 990   940   18000   81 250   150   7000  
    correct results 56 2500 2400 17000 14 990   940   18000   4 250   150   7000  
        correct true 35 2000 1900 9200 0 0   0   0   3 0   0   0  
        correct false 21 540 490 7400 14 990   940   18000   1 250   150   7000  
    incorrect results 1 300 290 930 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 1 300 290 930 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 140) 75
Run set sv-comp16.Floats