Tool CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Seahorn Ultimate Automizer r12950 Ultimate Kojak r12950
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host cayman[1-8]
OS Linux 3.13.0
System CPU: Intel Core i7-4770 @ 3.40 GHz with 8 cores, frequency: 3.4 GHz; RAM: 33 GB
Date of execution 14-12-04 12:41 [[ 14-12-21 23:21 ]] 14-11-15 15:53 [[ 14-12-21 23:23 ]] 14-12-13 18:39 [[ 14-12-19 11:24 ]] 14-12-20 18:50 [[ 14-12-21 21:13 ]] 14-12-02 13:00 [[ 14-12-21 23:12 ]] 14-12-02 13:02 [[ 14-12-21 23:18 ]]
Options --32 [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cbmc.14-12-04_1241.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/cbmc-sv-comp-2015/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] -sv-comp15 -disable-java-assertions -heap 10000m -setprop cpa.predicate.handlePointerAliasing=false [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cpachecker.14-11-15_1553.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/CPAchecker-1.3.10-svcomp15-unix/output/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=true ]] [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/esbmc.14-12-13_1839.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/esbmc-v1.24.1/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] --cex=witness.graphml [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/seahorn.14-12-20_1850.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/seahorn-svcomp15/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] 32bit precise [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/ultimateautomizer.14-11-12_2241.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/UltimateAutomizer/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] 32bit precise [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/ultimatekojak.14-12-02_1302.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/UltimateKojak/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]]
../../sv-benchmarks/c/ status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness
floats-cdfpl/newton_1_4_false-unreach-call.i witness confirmed 5.8  53 1.4  witness confirmed 650    8700 1.5  witness unconfirmed 0.61 31 1.4  witness confirmed 0.17 32 1.4  unknown 5.0  240 -    unknown 5.0  240 -   
floats-cdfpl/newton_1_5_false-unreach-call.i witness confirmed 8.2  52 1.4  witness confirmed 9.0  280 1.5  witness unconfirmed 0.33 25 1.7  witness confirmed 0.19 32 1.4  unknown 5.0  240 -    unknown 5.3  240 -   
floats-cdfpl/newton_1_6_false-unreach-call.i witness confirmed 5.4  50 1.5  witness confirmed 3.9  280 1.4  witness unconfirmed 0.42 31 1.4  witness confirmed 0.15 32 1.7  unknown 5.3  240 -    unknown 5.3  240 -   
floats-cdfpl/newton_1_7_false-unreach-call.i witness confirmed 10    59 1.4  witness confirmed 3.9  280 1.4  witness unconfirmed 0.33 31 1.4  witness confirmed 0.16 32 1.7  unknown 5.1  240 -    unknown 5.4  240 -   
floats-cdfpl/newton_1_8_false-unreach-call.i witness confirmed 13    65 1.4  witness confirmed 4.1  280 1.4  witness unconfirmed 0.27 25 1.4  witness confirmed 0.29 32 1.4  unknown 5.2  240 -    unknown 5.1  240 -   
floats-cdfpl/newton_2_6_false-unreach-call.i witness confirmed 130    220 1.5  out of memory 860    15000 -    witness unconfirmed 0.65 41 1.4  witness confirmed 0.16 32 1.4  unknown 5.2  240 -    unknown 5.2  240 -   
floats-cdfpl/newton_2_7_false-unreach-call.i witness confirmed 49    150 1.4  witness confirmed 33    400 1.4  witness unconfirmed 0.74 41 1.5  witness confirmed 0.14 32 1.4  unknown 5.2  240 -    unknown 5.0  240 -   
floats-cdfpl/newton_2_8_false-unreach-call.i witness confirmed 52    140 1.5  witness confirmed 15    390 1.4  witness unconfirmed 0.44 41 1.5  witness confirmed 0.15 32 1.7  unknown 5.2  240 -    unknown 5.2  240 -   
floats-cdfpl/newton_3_6_false-unreach-call.i unknown 510    580 -    timeout 920    880 -    witness unconfirmed 2.2  69 1.5  witness confirmed 0.16 32 1.4  unknown 5.2  240 -    unknown 5.1  240 -   
floats-cdfpl/newton_3_7_false-unreach-call.i unknown 250    370 -    out of memory 710    15000 -    witness unconfirmed 0.62 69 1.5  witness confirmed 0.14 32 1.4  unknown 5.4  240 -    unknown 5.0  240 -   
floats-cdfpl/newton_3_8_false-unreach-call.i unknown 48    170 -    witness confirmed 22    510 1.5  witness unconfirmed 0.43 68 1.5  witness confirmed 0.28 32 1.4  unknown 5.1  240 -    unknown 5.2  240 -   
floats-cdfpl/sine_1_false-unreach-call.i witness confirmed 5.2  45 1.4  witness confirmed 4.4  210 1.7  witness unconfirmed 0.27 24 1.4  witness confirmed 0.16 32 1.4  unknown 5.2  240 -    unknown 5.3  250 -   
floats-cdfpl/sine_2_false-unreach-call.i witness confirmed 1.7  36 1.4  witness confirmed 8.1  220 1.4  witness unconfirmed 0.34 23 1.4  witness confirmed 0.15 32 1.4  unknown 5.1  240 -    unknown 5.2  240 -   
floats-cdfpl/sine_3_false-unreach-call.i witness confirmed 3.9  41 1.4  witness confirmed 700    5200 1.5  witness unconfirmed 0.45 23 1.4  witness confirmed 0.30 32 1.4  unknown 5.3  240 -    unknown 5.5  240 -   
floats-cdfpl/square_1_false-unreach-call.i witness confirmed 1.0  35 1.4  witness confirmed 67    380 1.5  witness unconfirmed 0.15 14 1.4  witness confirmed 0.16 32 1.4  unknown 5.2  240 -    unknown 5.4  240 -   
floats-cdfpl/square_2_false-unreach-call.i witness confirmed 1.0  35 1.4  witness confirmed 300    700 1.5  witness unconfirmed 0.11 14 1.4  witness confirmed 0.17 32 1.4  unknown 5.0  240 -    unknown 5.3  240 -   
floats-cdfpl/square_3_false-unreach-call.i witness confirmed 1.6  36 1.7  witness confirmed 62    380 1.4  witness unconfirmed 0.16 14 1.4  witness confirmed 0.15 29 1.4  unknown 5.5  240 -    unknown 5.3  240 -   
floats-cdfpl/newton_1_1_true-unreach-call.i true 850    93 -    true 640    640 -    true 150    55 -    false(reach) 0.29 32 -    unknown 5.1  240 -    unknown 5.2  240 -   
floats-cdfpl/newton_1_2_true-unreach-call.i true 300    100 -    timeout 920    570 -    true 300    64 -    false(reach) 0.29 32 -    unknown 5.3  240 -    unknown 4.9  240 -   
floats-cdfpl/newton_1_3_true-unreach-call.i true 200    83 -    timeout 920    600 -    true 490    63 -    false(reach) 0.28 32 -    unknown 5.3  240 -    unknown 5.2  240 -   
floats-cdfpl/newton_2_1_true-unreach-call.i true 680    210 -    timeout 920    620 -    true 460    100 -    false(reach) 0.14 32 -    unknown 5.2  240 -    unknown 5.1  240 -   
floats-cdfpl/newton_2_2_true-unreach-call.i true 770    210 -    timeout 920    720 -    true 840    120 -    false(reach) 0.16 32 -    unknown 5.4  240 -    unknown 5.3  240 -   
floats-cdfpl/newton_2_3_true-unreach-call.i true 720    220 -    timeout 920    740 -    timeout 920    120 -    false(reach) 0.18 32 -    unknown 5.8  240 -    unknown 5.0  240 -   
floats-cdfpl/newton_2_4_true-unreach-call.i true 850    270 -    timeout 920    710 -    timeout 920    120 -    false(reach) 0.16 32 -    unknown 5.2  240 -    unknown 5.0  240 -   
floats-cdfpl/newton_2_5_true-unreach-call.i true 850    320 -    timeout 920    760 -    timeout 920    120 -    false(reach) 0.25 32 -    unknown 5.3  240 -    unknown 5.4  240 -   
floats-cdfpl/newton_3_1_true-unreach-call.i true 850    810 -    timeout 920    840 -    true 550    150 -    false(reach) 0.16 31 -    unknown 5.2  240 -    unknown 5.4  240 -   
floats-cdfpl/newton_3_2_true-unreach-call.i true 850    510 -    timeout 920    790 -    timeout 920    150 -    false(reach) 0.16 32 -    unknown 5.4  240 -    unknown 5.4  240 -   
floats-cdfpl/newton_3_3_true-unreach-call.i true 850    510 -    timeout 920    880 -    timeout 920    150 -    false(reach) 0.17 32 -    unknown 5.4  240 -    unknown 5.2  240 -   
floats-cdfpl/newton_3_4_true-unreach-call.i true 850    530 -    timeout 920    790 -    timeout 920    150 -    false(reach) 0.17 32 -    unknown 5.1  240 -    unknown 5.0  240 -   
floats-cdfpl/newton_3_5_true-unreach-call.i true 850    540 -    timeout 920    770 -    timeout 920    150 -    false(reach) 0.19 32 -    unknown 5.3  240 -    unknown 5.3  240 -   
floats-cdfpl/sine_4_true-unreach-call.i error 850    140 -    timeout 920    490 -    timeout 920    64 -    false(reach) 0.16 32 -    unknown 5.4  250 -    unknown 5.1  240 -   
floats-cdfpl/sine_5_true-unreach-call.i true 30    50 -    timeout 920    440 -    true 840    56 -    false(reach) 0.13 32 -    unknown 5.3  240 -    unknown 5.1  240 -   
floats-cdfpl/sine_6_true-unreach-call.i true 850    91 -    timeout 890    590 -    true 810    60 -    false(reach) 0.17 31 -    unknown 5.4  240 -    unknown 5.2  240 -   
floats-cdfpl/sine_7_true-unreach-call.i true 32    55 -    true 470    480 -    true 890    55 -    false(reach) 0.14 32 -    unknown 5.1  240 -    unknown 5.3  240 -   
floats-cdfpl/sine_8_true-unreach-call.i true 470    96 -    true 270    380 -    timeout 910    65 -    false(reach) 0.27 32 -    unknown 5.2  240 -    unknown 5.4  240 -   
floats-cdfpl/square_4_true-unreach-call.i true 850    130 -    true 600    520 -    false(reach) 0.16 14 -    false(reach) 0.29 32 -    unknown 5.2  240 -    unknown 5.4  240 -   
floats-cdfpl/square_5_true-unreach-call.i true 850    130 -    true 520    530 -    true 1.8  16 -    false(reach) 0.28 32 -    unknown 5.3  240 -    unknown 5.3  240 -   
floats-cdfpl/square_6_true-unreach-call.i true 850    130 -    true 360    460 -    true 3.5  17 -    false(reach) 0.15 32 -    unknown 5.2  240 -    unknown 6.0  240 -   
floats-cdfpl/square_7_true-unreach-call.i true 390    140 -    true 240    440 -    true 3.0  17 -    false(reach) 0.15 32 -    unknown 5.3  240 -    unknown 6.1  240 -   
floats-cdfpl/square_8_true-unreach-call.i true 7.2  36 -    true 57    300 -    true 0.082 13 -    false(reach) 0.15 31 -    unknown 5.3  240 -    unknown 5.2  240 -   
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 1.5  37 -    exception 24    370 -    false(reach) 1.0  28 -    unknown 0.032 9.0 -    unknown 5.1  240 -    unknown 5.5  240 -   
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true 0.49 24 -    true 1.4  130 -    true 0.058 11 -    true 0.14 23 -    unknown 5.2  240 -    unknown 5.4  240 -   
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 8.4  32 -    true 14    250 -    true 0.16 19 -    unknown 0.055 9.0 -    unknown 5.1  240 -    unknown 5.0  240 -   
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true 0.48 23 -    true 1.4  140 -    false(reach) 0.10 11 -    true 0.14 27 -    false(reach) 5.2  250 -    false(reach) 5.6  250 -   
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 1.3  28 -    true 3.9  250 -    false(reach) 1.1  19 -    unknown 0.059 9.0 -    unknown 5.4  240 -    unknown 5.5  240 -   
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true 0.52 23 -    true 1.4  140 -    unknown 0.040 2.0 -    true 0.16 27 -    unknown 5.4  240 -    unknown 5.5  250 -   
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true 0.50 23 -    true 1.4  140 -    unknown 0.040 2.0 -    true 0.21 27 -    unknown 5.6  240 -    unknown 6.2  240 -   
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 0.59 26 -    true 1.6  140 -    unknown 0.022 6.0 -    unknown 0.049 9.0 -    unknown 5.4  240 -    unknown 5.3  240 -   
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 1.2  29 -    unknown 3.3  230 -    unknown 0.045 6.0 -    unknown 0.048 9.0 -    false(reach) 5.3  240 -    false(reach) 5.6  240 -   
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 0.68 26 -    false(reach) 2.2  200 -    true 0.099 17 -    unknown 0.043 9.0 -    true 5.7  250 -    true 6.2  250 -   
floats-cbmc-regression/float-to-double2_true-unreach-call.i true 0.48 23 -    true 1.4  130 -    unknown 0.028 2.0 -    true 0.12 21 -    unknown 5.5  250 -    true 5.5  240 -   
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true 0.51 23 -    true 1.4  140 -    unknown 0.031 2.0 -    true 0.17 21 -    false(reach) 5.5  250 -    false(reach) 5.4  250 -   
floats-cbmc-regression/float11_true-unreach-call.i true 0.53 24 -    true 1.4  140 -    true 0.056 12 -    true 0.14 22 -    unknown 5.1  240 -    unknown 5.1  240 -   
floats-cbmc-regression/float12_true-unreach-call.i true 0.53 24 -    true 2.4  210 -    true 0.054 12 -    false(reach) 0.15 32 -    unknown 5.0  240 -    unknown 5.0  240 -   
floats-cbmc-regression/float13_true-unreach-call.i true 0.51 24 -    true 2.1  200 -    false(reach) 0.12 12 -    true 0.14 27 -    unknown 5.5  240 -    unknown 5.0  240 -   
floats-cbmc-regression/float14_true-unreach-call.i true 1.1  27 -    true 3.3  210 -    false(reach) 0.96 17 -    unknown 0.057 9.0 -    unknown 5.1  240 -    unknown 4.9  240 -   
floats-cbmc-regression/float18_true-unreach-call.i true 1.1  27 -    true 1.5  140 -    false(reach) 1.0  17 -    unknown 0.048 9.0 -    unknown 5.6  240 -    unknown 5.5  250 -   
floats-cbmc-regression/float19_true-unreach-call.i true 1.1  27 -    true 3.1  210 -    unknown 0.075 8.0 -    unknown 0.054 9.0 -    unknown 5.3  240 -    unknown 5.3  240 -   
floats-cbmc-regression/float1_true-unreach-call.i true 0.50 23 -    true 1.4  140 -    true 0.067 12 -    true 0.15 27 -    unknown 5.0  240 -    unknown 5.3  240 -   
floats-cbmc-regression/float20_true-unreach-call.i true 0.60 27 -    true 1.4  130 -    unknown 0.041 2.0 -    false(reach) 0.32 32 -    unknown 5.1  240 -    unknown 5.0  240 -   
floats-cbmc-regression/float22_true-unreach-call.i true 0.55 24 -    true 1.5  140 -    unknown 0.054 4.0 -    true 0.19 22 -    unknown 5.1  240 -    unknown 5.3  240 -   
floats-cbmc-regression/float2_true-unreach-call.i true 0.51 23 -    true 1.4  130 -    unknown 0.015 2.0 -    true 0.15 27 -    unknown 5.0  240 -    unknown 4.9  240 -   
floats-cbmc-regression/float3_true-unreach-call.i true 0.59 25 -    true 1.4  130 -    true 0.086 12 -    false(reach) 0.18 31 -    unknown 5.4  240 -    unknown 5.1  240 -   
floats-cbmc-regression/float4_true-unreach-call.i true 35    46 -    true 37    320 -    true 0.16 18 -    unknown 0.052 9.0 -    unknown 5.3  240 -    unknown 5.5  240 -   
floats-cbmc-regression/float5_true-unreach-call.i true 0.54 24 -    true 1.4  130 -    true 0.072 12 -    false(reach) 0.13 33 -    unknown 5.2  240 -    unknown 5.2  240 -   
floats-cbmc-regression/float6_true-unreach-call.i true 0.56 24 -    true 1.4  130 -    true 0.081 13 -    false(reach) 0.19 33 -    unknown 5.1  240 -    unknown 5.0  240 -   
floats-cbmc-regression/float7_true-unreach-call.i true 0.47 23 -    false(reach) 1.6  160 -    true 0.054 11 -    true 0.16 27 -    false(reach) 5.5  250 -    false(reach) 5.7  250 -   
floats-cbmc-regression/float8_true-unreach-call.i true 2.6  29 -    true 7.0  220 -    true 0.089 17 -    unknown 0.042 9.0 -    unknown 5.2  240 -    unknown 5.1  240 -   
float-benchs/float_int_inv_square_false-unreach-call.c witness confirmed 0.13 25 1.5  witness confirmed 1.7  170 1.4  unknown 0.055 11 -    witness confirmed 0.17 32 1.5  unknown 5.1  240 -    unknown 5.2  240 -   
float-benchs/inv_square_false-unreach-call.c witness confirmed 0.14 25 1.4  witness confirmed 1.7  170 1.4  unknown 0.057 12 -    witness confirmed 0.17 32 1.5  unknown 5.2  240 -    unknown 5.3  240 -   
float-benchs/nan_double_false-unreach-call.c witness confirmed 0.12 23 1.4  witness confirmed 1.6  160 1.4  true 0.067 12 -    witness confirmed 0.14 32 1.4  true 5.7  250 -    true 5.2  250 -   
float-benchs/nan_float_false-unreach-call.c witness confirmed 0.12 23 1.4  witness confirmed 1.6  160 1.4  true 0.073 12 -    witness confirmed 0.14 32 1.4  true 5.6  250 -    true 5.4  240 -   
float-benchs/sin_interpolated_index_false-unreach-call.c witness confirmed 3.9  210 1.7  unknown 2.8  200 -    unknown 0.081 14 -    witness confirmed 0.34 32 1.6  unknown 5.4  240 -    unknown 5.1  240 -   
float-benchs/inv_square_int_true-unreach-call.c true 0.68 27 -    true 2.8  220 -    unknown 0.075 12 -    false(reach) 0.16 32 -    unknown 5.5  240 -    unknown 5.2  240 -   
float-benchs/inv_square_true-unreach-call.c true 0.64 27 -    true 2.4  220 -    unknown 0.077 12 -    false(reach) 0.16 32 -    unknown 5.3  240 -    unknown 5.2  240 -   
float-benchs/nan_double_range_true-unreach-call.c true 0.53 23 -    true 2.1  210 -    true 0.060 12 -    false(reach) 0.16 32 -    unknown 5.2  240 -    unknown 5.1  240 -   
float-benchs/nan_float_range_true-unreach-call.c true 0.53 23 -    true 2.2  210 -    true 0.074 12 -    false(reach) 0.13 32 -    unknown 5.3  240 -    unknown 5.5  240 -   
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c error 850    710 -    unknown 2.9  210 -    unknown 0.090 14 -    false(reach) 0.23 34 -    unknown 5.3  240 -    unknown 5.5  240 -   
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c error 850    660 -    unknown 2.8  210 -    unknown 0.072 14 -    false(reach) 0.23 34 -    unknown 5.1  240 -    unknown 5.1  240 -   
float-benchs/sin_interpolated_index_true-unreach-call.c error 850    660 -    unknown 2.7  210 -    unknown 0.089 14 -    false(reach) 0.22 32 -    unknown 5.1  240 -    unknown 5.3  240 -   
float-benchs/sin_interpolated_smallrange_true-unreach-call.c true 850    3800 -    unknown 2.9  200 -    unknown 0.12 14 -    unknown 0.25 30 -    unknown 5.2  240 -    unknown 5.0  240 -   
../../sv-benchmarks/c/ status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness
total files 81 19000 14000 28 81 21000 70000 26 81 14000 2900 25 81 14 2300 32 81 430 19000 - 81 430 19000 -
correct results 74 15000 11000 28 54 5100 27000 26 27 5300 970 0 34 5.9 1000 32 1 5.7 250 - 2 12 490 -
false negatives 0 - - - 0 - - - 2 0.14 24 0 0 - - - 2 11 490 - 2 11 490 -
false positives 0 - - - 2 3.8 360 0 7 4.5 120 0 35 6.7 1100 0 4 22 980 - 4 22 980 -
false properties 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
score (81 files, max score: 140) 129 - - - 78 - - - -12 - - - -164 - - - -46 - - - -44 - - -
Tool CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Seahorn Ultimate Automizer r12950 Ultimate Kojak r12950