Tool ULTIMATE Automizer cfb9fd9e
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-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 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/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.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 unknown 9.7 3.0 350 wit - -
floats-cdfpl/newton_1_5_false-unreach-call.i unknown 9.0 3.5 360 wit - -
floats-cdfpl/newton_1_6_false-unreach-call.i unknown 7.9 2.8 320 wit - -
floats-cdfpl/newton_1_7_false-unreach-call.i unknown 8.8 3.0 340 wit - -
floats-cdfpl/newton_1_8_false-unreach-call.i unknown 8.8 2.9 330 wit - -
floats-cdfpl/newton_2_6_false-unreach-call.i unknown 9.7 4.4 330 wit - -
floats-cdfpl/newton_2_7_false-unreach-call.i unknown 9.2 3.0 320 wit - -
floats-cdfpl/newton_2_8_false-unreach-call.i unknown 8.7 3.4 320 wit - -
floats-cdfpl/newton_3_6_false-unreach-call.i unknown 9.5 2.8 350 wit - -
floats-cdfpl/newton_3_7_false-unreach-call.i unknown 9.8 2.8 350 wit - -
floats-cdfpl/newton_3_8_false-unreach-call.i unknown 8.5 3.1 330 wit - -
floats-cdfpl/sine_1_false-unreach-call.i unknown 8.0 2.8 320 wit - -
floats-cdfpl/sine_2_false-unreach-call.i unknown 8.2 2.8 320 wit - -
floats-cdfpl/sine_3_false-unreach-call.i unknown 8.4 2.6 330 wit - -
floats-cdfpl/square_1_false-unreach-call.i unknown 9.2 2.7 330 wit - -
floats-cdfpl/square_2_false-unreach-call.i unknown 9.7 4.8 320 wit - -
floats-cdfpl/square_3_false-unreach-call.i unknown 8.3 2.6 330 wit - -
floats-cdfpl/newton_1_1_true-unreach-call.i unknown 9.6 2.8 340 wit - -
floats-cdfpl/newton_1_2_true-unreach-call.i unknown 9.3 2.7 330 wit - -
floats-cdfpl/newton_1_3_true-unreach-call.i unknown 8.0 2.5 310 wit - -
floats-cdfpl/newton_2_1_true-unreach-call.i unknown 8.1 2.5 310 wit - -
floats-cdfpl/newton_2_2_true-unreach-call.i unknown 7.7 2.5 320 wit - -
floats-cdfpl/newton_2_3_true-unreach-call.i unknown 8.6 2.6 320 wit - -
floats-cdfpl/newton_2_4_true-unreach-call.i unknown 8.2 2.8 320 wit - -
floats-cdfpl/newton_2_5_true-unreach-call.i unknown 9.7 3.4 330 wit - -
floats-cdfpl/newton_3_1_true-unreach-call.i unknown 9.8 3.0 350 wit - -
floats-cdfpl/newton_3_2_true-unreach-call.i unknown 8.9 3.0 330 wit - -
floats-cdfpl/newton_3_3_true-unreach-call.i unknown 9.5 3.3 310 wit - -
floats-cdfpl/newton_3_4_true-unreach-call.i unknown 8.8 3.0 340 wit - -
floats-cdfpl/newton_3_5_true-unreach-call.i unknown 8.8 2.8 330 wit - -
floats-cdfpl/sine_4_true-unreach-call.i unknown 9.2 2.8 330 wit - -
floats-cdfpl/sine_5_true-unreach-call.i unknown 9.3 4.0 320 wit - -
floats-cdfpl/sine_6_true-unreach-call.i unknown 7.8 2.7 320 wit - -
floats-cdfpl/sine_7_true-unreach-call.i unknown 8.6 2.7 310 wit - -
floats-cdfpl/sine_8_true-unreach-call.i unknown 8.5 2.6 320 wit - -
floats-cdfpl/square_4_true-unreach-call.i unknown 8.0 2.5 310 wit - -
floats-cdfpl/square_5_true-unreach-call.i unknown 8.2 2.6 320 wit - -
floats-cdfpl/square_6_true-unreach-call.i unknown 9.1 2.6 320 wit - -
floats-cdfpl/square_7_true-unreach-call.i unknown 9.0 4.0 330 wit - -
floats-cdfpl/square_8_true-unreach-call.i unknown 8.5 3.0 330 wit - -
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i unknown 8.2 2.7 310 wit - -
floats-cbmc-regression/float-no-simp1_true-unreach-call.i unknown 9.2 3.0 330 wit - -
floats-cbmc-regression/float-no-simp2_true-unreach-call.i unknown 8.6 3.1 320 wit - -
floats-cbmc-regression/float-no-simp3_true-unreach-call.i unknown 7.8 3.6 320 wit - -
floats-cbmc-regression/float-no-simp4_true-unreach-call.i unknown 7.2 2.3 310 wit - -
floats-cbmc-regression/float-no-simp6_true-unreach-call.i unknown 8.7 2.6 340 wit - -
floats-cbmc-regression/float-no-simp7_true-unreach-call.i unknown 8.5 3.2 320 wit - -
floats-cbmc-regression/float-no-simp8_true-unreach-call.i error 9.0 4.6 330 wit - -
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 8.8 2.7 320 wit - -
floats-cbmc-regression/float-to-double1_true-unreach-call.i unknown 7.7 2.4 310 wit - -
floats-cbmc-regression/float-to-double2_true-unreach-call.i unknown 8.6 3.5 320 wit - -
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i unknown 7.4 2.5 300 wit - -
floats-cbmc-regression/float11_true-unreach-call.i unknown 8.7 3.1 330 wit - -
floats-cbmc-regression/float12_true-unreach-call.i unknown 8.7 2.6 320 wit - -
floats-cbmc-regression/float13_true-unreach-call.i unknown 8.1 2.6 320 wit - -
floats-cbmc-regression/float14_true-unreach-call.i unknown 9.1 2.8 330 wit - -
floats-cbmc-regression/float18_true-unreach-call.i unknown 8.0 2.4 300 wit - -
floats-cbmc-regression/float19_true-unreach-call.i unknown 8.6 2.8 320 wit - -
floats-cbmc-regression/float1_true-unreach-call.i unknown 9.7 2.8 340 wit - -
floats-cbmc-regression/float20_true-unreach-call.i unknown 8.6 2.7 320 wit - -
floats-cbmc-regression/float22_true-unreach-call.i error 14   4.9 360 wit - -
floats-cbmc-regression/float2_true-unreach-call.i error 8.2 3.1 320 wit - -
floats-cbmc-regression/float3_true-unreach-call.i unknown 8.5 3.2 330 wit - -
floats-cbmc-regression/float4_true-unreach-call.i unknown 7.9 3.6 310 wit - -
floats-cbmc-regression/float5_true-unreach-call.i unknown 8.1 2.5 330 wit - -
floats-cbmc-regression/float6_true-unreach-call.i unknown 8.9 2.8 330 wit - -
floats-cbmc-regression/float7_true-unreach-call.i unknown 7.4 2.3 320 wit - -
floats-cbmc-regression/float8_true-unreach-call.i unknown 8.2 2.5 300 wit - -
float-benchs/float_int_inv_square_false-unreach-call.c unknown 8.5 2.9 330 wit - -
float-benchs/inv_square_false-unreach-call.c unknown 8.4 2.7 320 wit - -
float-benchs/nan_double_false-unreach-call.c false(reach) 7.9 2.4 330 wit false(reach) 4.5 2.7 230 false(reach) 10 5.7 320
float-benchs/nan_float_false-unreach-call.c false(reach) 8.7 3.2 330 wit false(reach) 4.3 2.6 220 false(reach) 12 7.2 340
float-benchs/sin_interpolated_index_false-unreach-call.c error 7.5 3.1 310 wit - -
float-benchs/inv_square_int_true-unreach-call.c unknown 8.1 2.6 320 wit - -
float-benchs/inv_square_true-unreach-call.c unknown 8.7 2.7 330 wit - -
float-benchs/nan_double_range_true-unreach-call.c unknown 8.7 2.7 320 wit - -
float-benchs/nan_float_range_true-unreach-call.c unknown 8.3 3.0 310 wit - -
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c error 8.4 2.8 320 wit - -
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c error 8.5 2.7 310 wit - -
float-benchs/sin_interpolated_index_true-unreach-call.c error 9.4 3.0 340 wit - -
float-benchs/sin_interpolated_smallrange_true-unreach-call.c error 8.4 3.1 310 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 700 240   26000 81 8.8 5.3 450 81 22 13 660
    correct results 2 17 5.6 660 2 8.8 5.3 450 2 22 13 660
        correct true 0
        correct false 2 17 5.6 660 2 8.8 5.3 450 2 22 13 660
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 140) 2
Run set sv-comp16.Floats