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 false(reach) 51      51     340   wit timeout 91   89   330 true 11   6.7 320
floats-cdfpl/newton_1_5_false-unreach-call.i false(reach) 33      30     340   wit false(reach) 58   57   1000 true 11   6.4 330
floats-cdfpl/newton_1_6_false-unreach-call.i false(reach) 18      21     330   wit false(reach) 14   12   390 true 10   6.2 330
floats-cdfpl/newton_1_7_false-unreach-call.i false(reach) 7.9    10     340   wit false(reach) 41   39   520 true 11   6.0 340
floats-cdfpl/newton_1_8_false-unreach-call.i false(reach) 8.3    10     330   wit false(reach) 16   14   400 true 10   6.0 330
floats-cdfpl/newton_2_6_false-unreach-call.i false(reach) 630      610     7500   wit timeout 91   88   430 true 12   7.4 340
floats-cdfpl/newton_2_7_false-unreach-call.i false(reach) 310      290     2500   wit timeout 91   89   1800 true 10   6.2 320
floats-cdfpl/newton_2_8_false-unreach-call.i false(reach) 24      21     600   wit timeout 91   89   1000 true 10   6.1 340
floats-cdfpl/newton_3_6_false-unreach-call.i out of memory 770      740     15000   wit - -
floats-cdfpl/newton_3_7_false-unreach-call.i false(reach) 92      71     1100   wit timeout 91   89   1300 true 9.7 5.5 320
floats-cdfpl/newton_3_8_false-unreach-call.i false(reach) 48      41     1100   wit timeout 91   89   1300 true 11   6.6 330
floats-cdfpl/sine_1_false-unreach-call.i false(reach) 16      20     290   wit false(reach) 38   37   430 true 11   6.4 310
floats-cdfpl/sine_2_false-unreach-call.i false(reach) 24      30     300   wit timeout 91   89   2200 true 9.9 6.1 330
floats-cdfpl/sine_3_false-unreach-call.i false(reach) 6.5    11     280   wit false(reach) 11   8.9 330 true 11   6.5 330
floats-cdfpl/square_1_false-unreach-call.i false(reach) 28      30     420   wit false(reach) 58   56   690 true 10   6.4 310
floats-cdfpl/square_2_false-unreach-call.i false(reach) 70      70     480   wit timeout 91   89   320 true 10   6.2 320
floats-cdfpl/square_3_false-unreach-call.i false(reach) 27      30     430   wit timeout 91   89   340 true 10   6.1 320
floats-cdfpl/newton_1_1_true-unreach-call.i true 200      200     52   wit - -
floats-cdfpl/newton_1_2_true-unreach-call.i true 320      320     57   wit - -
floats-cdfpl/newton_1_3_true-unreach-call.i true 590      590     57   wit - -
floats-cdfpl/newton_2_1_true-unreach-call.i true 410      410     100   wit - -
floats-cdfpl/newton_2_2_true-unreach-call.i true 840      840     120   wit - -
floats-cdfpl/newton_2_3_true-unreach-call.i unknown 890      900     120   wit - -
floats-cdfpl/newton_2_4_true-unreach-call.i unknown 900      900     120   wit - -
floats-cdfpl/newton_2_5_true-unreach-call.i unknown 890      900     120   wit - -
floats-cdfpl/newton_3_1_true-unreach-call.i true 680      680     150   wit - -
floats-cdfpl/newton_3_2_true-unreach-call.i unknown 890      900     150   wit - -
floats-cdfpl/newton_3_3_true-unreach-call.i unknown 890      900     150   wit - -
floats-cdfpl/newton_3_4_true-unreach-call.i unknown 890      900     150   wit - -
floats-cdfpl/newton_3_5_true-unreach-call.i unknown 890      900     150   wit - -
floats-cdfpl/sine_4_true-unreach-call.i unknown 890      900     60   wit - -
floats-cdfpl/sine_5_true-unreach-call.i unknown 890      900     65   wit - -
floats-cdfpl/sine_6_true-unreach-call.i unknown 890      900     60   wit - -
floats-cdfpl/sine_7_true-unreach-call.i unknown 890      900     58   wit - -
floats-cdfpl/sine_8_true-unreach-call.i unknown 890      900     57   wit - -
floats-cdfpl/square_4_true-unreach-call.i false(reach) 800      800     680   wit - -
floats-cdfpl/square_5_true-unreach-call.i true 2.2    2.2   16   wit - -
floats-cdfpl/square_6_true-unreach-call.i true 4.4    4.4   18   wit - -
floats-cdfpl/square_7_true-unreach-call.i true 3.8    3.8   18   wit - -
floats-cdfpl/square_8_true-unreach-call.i true .064  .072 15   wit - -
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i unknown .18   .20  28   wit - -
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true .090  .10  13   wit - -
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true .25   .27  24   wit - -
floats-cbmc-regression/float-no-simp3_true-unreach-call.i error (1) 3.4    10     200   wit - -
floats-cbmc-regression/float-no-simp4_true-unreach-call.i unknown .11   .13  24   wit - -
floats-cbmc-regression/float-no-simp6_true-unreach-call.i unknown .0085 .019 2.9 wit - -
floats-cbmc-regression/float-no-simp7_true-unreach-call.i unknown .0098 .021 2.8 wit - -
floats-cbmc-regression/float-no-simp8_true-unreach-call.i unknown .032  .046 10   wit - -
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown .030  .041 11   wit - -
floats-cbmc-regression/float-to-double1_true-unreach-call.i true .10   .12  23   wit - -
floats-cbmc-regression/float-to-double2_true-unreach-call.i unknown .010  .021 2.7 wit - -
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i unknown .0091 .020 3.2 wit - -
floats-cbmc-regression/float11_true-unreach-call.i true .10   .12  13   wit - -
floats-cbmc-regression/float12_true-unreach-call.i true .099  .11  13   wit - -
floats-cbmc-regression/float13_true-unreach-call.i error (1) 3.8    10     200   wit - -
floats-cbmc-regression/float14_true-unreach-call.i false(reach) 12      12     370   wit - -
floats-cbmc-regression/float18_true-unreach-call.i error (1) 12      12     340   wit - -
floats-cbmc-regression/float19_true-unreach-call.i unknown .062  .073 14   wit - -
floats-cbmc-regression/float1_true-unreach-call.i true .096  .11  13   wit - -
floats-cbmc-regression/float20_true-unreach-call.i unknown .015  .027 3.0 wit - -
floats-cbmc-regression/float22_true-unreach-call.i unknown .065  .076 14   wit - -
floats-cbmc-regression/float2_true-unreach-call.i unknown .010  .021 2.9 wit - -
floats-cbmc-regression/float3_true-unreach-call.i true .062  .072 13   wit - -
floats-cbmc-regression/float4_true-unreach-call.i true .17   .18  24   wit - -
floats-cbmc-regression/float5_true-unreach-call.i true .069  .078 13   wit - -
floats-cbmc-regression/float6_true-unreach-call.i error (1) 4.0    10     200   wit - -
floats-cbmc-regression/float7_true-unreach-call.i true .066  .076 13   wit - -
floats-cbmc-regression/float8_true-unreach-call.i true .11   .12  23   wit - -
float-benchs/float_int_inv_square_false-unreach-call.c false(reach) 5.2    10     250   wit false(reach) 5.2 3.2 240 true 12   7.1 340
float-benchs/inv_square_false-unreach-call.c false(reach) 5.1    10     250   wit false(reach) 5.3 3.2 240 true 10   6.0 310
float-benchs/nan_double_false-unreach-call.c false(reach) 4.0    10     220   wit false(reach) 4.7 2.8 230 true 9.6 5.8 310
float-benchs/nan_float_false-unreach-call.c false(reach) 4.0    10     220   wit false(reach) 4.6 2.8 220 true 11   6.6 320
float-benchs/sin_interpolated_index_false-unreach-call.c false(reach) 72      51     2700   wit unknown 5.7 3.3 250 error 10   5.9 320
float-benchs/inv_square_int_true-unreach-call.c true .066  .075 13   wit - -
float-benchs/inv_square_true-unreach-call.c error (1) 13      10     470   wit - -
float-benchs/nan_double_range_true-unreach-call.c error (1) 5.8    10     270   wit - -
float-benchs/nan_float_range_true-unreach-call.c error (1) 5.9    10     270   wit - -
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c false(reach) 260      220     3900   wit - -
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c false(reach) 270      250     3100   wit - -
float-benchs/sin_interpolated_index_true-unreach-call.c false(reach) 71      51     3000   wit - -
float-benchs/sin_interpolated_smallrange_true-unreach-call.c unknown 900      900     11000   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 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