Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
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-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]]
Run set sv-comp16.Floats
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.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 51      51     340   91   89   330 11   6.7 320
floats-cdfpl/newton_1_5_false-unreach-call.i 33      30     340   58   57   1000 11   6.4 330
floats-cdfpl/newton_1_6_false-unreach-call.i 18      21     330   14   12   390 10   6.2 330
floats-cdfpl/newton_1_7_false-unreach-call.i 7.9    10     340   41   39   520 11   6.0 340
floats-cdfpl/newton_1_8_false-unreach-call.i 8.3    10     330   16   14   400 10   6.0 330
floats-cdfpl/newton_2_6_false-unreach-call.i 630      610     7500   91   88   430 12   7.4 340
floats-cdfpl/newton_2_7_false-unreach-call.i 310      290     2500   91   89   1800 10   6.2 320
floats-cdfpl/newton_2_8_false-unreach-call.i 24      21     600   91   89   1000 10   6.1 340
floats-cdfpl/newton_3_6_false-unreach-call.i 770      740     15000  
floats-cdfpl/newton_3_7_false-unreach-call.i 92      71     1100   91   89   1300 9.7 5.5 320
floats-cdfpl/newton_3_8_false-unreach-call.i 48      41     1100   91   89   1300 11   6.6 330
floats-cdfpl/sine_1_false-unreach-call.i 16      20     290   38   37   430 11   6.4 310
floats-cdfpl/sine_2_false-unreach-call.i 24      30     300   91   89   2200 9.9 6.1 330
floats-cdfpl/sine_3_false-unreach-call.i 6.5    11     280   11   8.9 330 11   6.5 330
floats-cdfpl/square_1_false-unreach-call.i 28      30     420   58   56   690 10   6.4 310
floats-cdfpl/square_2_false-unreach-call.i 70      70     480   91   89   320 10   6.2 320
floats-cdfpl/square_3_false-unreach-call.i 27      30     430   91   89   340 10   6.1 320
floats-cdfpl/newton_1_1_true-unreach-call.i 200      200     52  
floats-cdfpl/newton_1_2_true-unreach-call.i 320      320     57  
floats-cdfpl/newton_1_3_true-unreach-call.i 590      590     57  
floats-cdfpl/newton_2_1_true-unreach-call.i 410      410     100  
floats-cdfpl/newton_2_2_true-unreach-call.i 840      840     120  
floats-cdfpl/newton_2_3_true-unreach-call.i 890      900     120  
floats-cdfpl/newton_2_4_true-unreach-call.i 900      900     120  
floats-cdfpl/newton_2_5_true-unreach-call.i 890      900     120  
floats-cdfpl/newton_3_1_true-unreach-call.i 680      680     150  
floats-cdfpl/newton_3_2_true-unreach-call.i 890      900     150  
floats-cdfpl/newton_3_3_true-unreach-call.i 890      900     150  
floats-cdfpl/newton_3_4_true-unreach-call.i 890      900     150  
floats-cdfpl/newton_3_5_true-unreach-call.i 890      900     150  
floats-cdfpl/sine_4_true-unreach-call.i 890      900     60  
floats-cdfpl/sine_5_true-unreach-call.i 890      900     65  
floats-cdfpl/sine_6_true-unreach-call.i 890      900     60  
floats-cdfpl/sine_7_true-unreach-call.i 890      900     58  
floats-cdfpl/sine_8_true-unreach-call.i 890      900     57  
floats-cdfpl/square_4_true-unreach-call.i 800      800     680  
floats-cdfpl/square_5_true-unreach-call.i 2.2    2.2   16  
floats-cdfpl/square_6_true-unreach-call.i 4.4    4.4   18  
floats-cdfpl/square_7_true-unreach-call.i 3.8    3.8   18  
floats-cdfpl/square_8_true-unreach-call.i .064  .072 15  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i .18   .20  28  
floats-cbmc-regression/float-no-simp1_true-unreach-call.i .090  .10  13  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i .25   .27  24  
floats-cbmc-regression/float-no-simp3_true-unreach-call.i 3.4    10     200  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i .11   .13  24  
floats-cbmc-regression/float-no-simp6_true-unreach-call.i .0085 .019 2.9
floats-cbmc-regression/float-no-simp7_true-unreach-call.i .0098 .021 2.8
floats-cbmc-regression/float-no-simp8_true-unreach-call.i .032  .046 10  
floats-cbmc-regression/float-rounding1_true-unreach-call.i .030  .041 11  
floats-cbmc-regression/float-to-double1_true-unreach-call.i .10   .12  23  
floats-cbmc-regression/float-to-double2_true-unreach-call.i .010  .021 2.7
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i .0091 .020 3.2
floats-cbmc-regression/float11_true-unreach-call.i .10   .12  13  
floats-cbmc-regression/float12_true-unreach-call.i .099  .11  13  
floats-cbmc-regression/float13_true-unreach-call.i 3.8    10     200  
floats-cbmc-regression/float14_true-unreach-call.i 12      12     370  
floats-cbmc-regression/float18_true-unreach-call.i 12      12     340  
floats-cbmc-regression/float19_true-unreach-call.i .062  .073 14  
floats-cbmc-regression/float1_true-unreach-call.i .096  .11  13  
floats-cbmc-regression/float20_true-unreach-call.i .015  .027 3.0
floats-cbmc-regression/float22_true-unreach-call.i .065  .076 14  
floats-cbmc-regression/float2_true-unreach-call.i .010  .021 2.9
floats-cbmc-regression/float3_true-unreach-call.i .062  .072 13  
floats-cbmc-regression/float4_true-unreach-call.i .17   .18  24  
floats-cbmc-regression/float5_true-unreach-call.i .069  .078 13  
floats-cbmc-regression/float6_true-unreach-call.i 4.0    10     200  
floats-cbmc-regression/float7_true-unreach-call.i .066  .076 13  
floats-cbmc-regression/float8_true-unreach-call.i .11   .12  23  
float-benchs/float_int_inv_square_false-unreach-call.c 5.2    10     250   5.2 3.2 240 12   7.1 340
float-benchs/inv_square_false-unreach-call.c 5.1    10     250   5.3 3.2 240 10   6.0 310
float-benchs/nan_double_false-unreach-call.c 4.0    10     220   4.7 2.8 230 9.6 5.8 310
float-benchs/nan_float_false-unreach-call.c 4.0    10     220   4.6 2.8 220 11   6.6 320
float-benchs/sin_interpolated_index_false-unreach-call.c 72      51     2700   5.7 3.3 250 10   5.9 320
float-benchs/inv_square_int_true-unreach-call.c .066  .075 13  
float-benchs/inv_square_true-unreach-call.c 13      10     470  
float-benchs/nan_double_range_true-unreach-call.c 5.8    10     270  
float-benchs/nan_float_range_true-unreach-call.c 5.9    10     270  
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c 260      220     3900  
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c 270      250     3100  
float-benchs/sin_interpolated_index_true-unreach-call.c 71      51     3000  
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 900      900     11000  
../../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 18000 18000 62000 81 1100   1000   14000   81 220   130   6800  
    correct results 43 4500 4500 21000 11 1100   1000   14000   20 220   130   6800  
        correct true 22 3100 3100 810 0 0   0   0   20 0   0   0  
        correct false 21 1500 1400 20000 11 1100   1000   14000   0 220   130   6800  
    incorrect results 5 1400 1300 11000 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 5 1400 1300 11000 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 140) -15
Run set sv-comp16.Floats