Tool Beagle 1.1 Cascade 0.1 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-20 11:35 [[ 14-12-06 00:00 ]] 14-12-20 11:27 [[ 14-12-20 14:02 ]] 14-12-19 16:19 [[ 14-12-21 23:26 ]] 14-12-19 16:18 [[ 14-12-20 10:06 ]] 14-12-19 16:19 [[ 14-12-20 10:07 ]] 14-12-20 18:50 [[ 14-12-21 21:13 ]] 14-12-19 17:19 [[ 14-12-21 23:15 ]] 14-12-19 17:19 [[ 14-12-20 10:09 ]]
Options -t 895 -b [[ -witness-check -noout -spec ../../results-2015/blast.14-11-25_0345.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/blast-2.7.3/bin/witness.graphml -setprop spec.singlePathMatching=true -setprop parser.transformTokensToLines=false -tokenize -useTokenizer ]] -trace [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cascade.14-12-20_1127.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/Cascade-4113-patch/out/${sourcefile_name}/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] --32 [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cbmc.14-12-19_1619.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 [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cpachecker.14-12-19_1618.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-19_1619.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-12-19_1719.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-19_1719.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 status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness
bitvector/byte_add_false-unreach-call.i timeout 920    580 -    witness invalid (error (invalid c code)) 1.8  130 1.5  witness confirmed 0.22 26 2.8  witness confirmed 64    1200 2.6  witness confirmed 0.36 14 1.8  witness confirmed 0.47 46 2.5  unknown 14    410 -    witness unconfirmed 7.9  280 1.8 
bitvector/byte_add_1_true-unreach-call.i timeout 920    570 -    true 860    2200 -    true 0.74 27 -    true 35    1200 -    true 0.10 13 -    false(reach) 0.42 46 -    unknown 14    420 -    false(reach) 7.6  270 -   
bitvector/byte_add_2_true-unreach-call.i timeout 920    570 -    true 860    3400 -    true 0.77 28 -    true 78    1300 -    true 0.11 13 -    false(reach) 0.41 44 -    unknown 13    410 -    false(reach) 7.8  270 -   
bitvector/gcd_1_true-unreach-call.i true 19    37 -    true 850    8900 -    true 2.4  64 -    true 2.3  200 -    true 0.59 24 -    false(reach) 0.21 35 -    unknown 5.4  240 -    unknown 5.4  250 -   
bitvector/gcd_2_true-unreach-call.i unknown 0.088 2.0 -    true 850    4900 -    true 2.5  63 -    true 2.3  210 -    true 19    32 -    false(reach) 0.21 35 -    unknown 5.0  240 -    unknown 5.1  240 -   
bitvector/gcd_3_true-unreach-call.i unknown 0.087 2.0 -    true 850    4900 -    true 2.7  63 -    true 2.3  210 -    true 19    32 -    false(reach) 0.19 35 -    unknown 5.6  240 -    unknown 5.3  240 -   
bitvector/gcd_4_true-unreach-call.i true 6.3  18 -    true 5.1  230 -    true 0.50 23 -    true 1.4  140 -    true 0.074 12 -    timeout 920    32 -    unknown 5.5  250 -    unknown 5.5  250 -   
bitvector/interleave_bits_true-unreach-call.i true 0.30 10.0 -    true 4.9  230 -    true 0.53 23 -    true 17    430 -    true 0.065 12 -    false(reach) 0.29 39 -    unknown 20    650 -    false(reach) 15    660 -   
bitvector/jain_1_true-unreach-call.i true 0.14 10.0 -    true 680    1200 -    true 0.83 69 -    true 2.5  210 -    true 0.076 11 -    unknown 0.16 29 -    true 6.0  250 -    true 5.9  250 -   
bitvector/jain_2_true-unreach-call.i true 0.15 10.0 -    true 860    1000 -    true 1.2  140 -    true 2.6  210 -    true 0.076 11 -    false(reach) 0.17 32 -    true 6.1  250 -    true 10    260 -   
bitvector/jain_4_true-unreach-call.i true 0.15 10.0 -    true 130    12000 -    true 1.6  200 -    true 2.6  210 -    true 0.063 11 -    out of memory 790    15000 -    true 18    440 -    timeout 920    630 -   
bitvector/jain_5_true-unreach-call.i true 0.18 11 -    true 150    2400 -    true 0.50 23 -    timeout 920    1800 -    true 0.056 11 -    true 0.19 30 -    true 6.3  250 -    true 7.3  270 -   
bitvector/jain_6_true-unreach-call.i true 0.18 10.0 -    out of memory 60    15000 -    true 1.3  150 -    true 2.6  210 -    true 0.066 11 -    timeout 920    10000 -    unknown 150    530 -    timeout 920    790 -   
bitvector/jain_7_true-unreach-call.i true 0.14 10.0 -    true 860    1200 -    true 0.89 59 -    true 5.0  230 -    true 0.063 11 -    timeout 920    11000 -    unknown 93    470 -    timeout 920    610 -   
bitvector/modulus_true-unreach-call.i true 1.8  11 -    unknown 850    1100 -    true 250    1100 -    timeout 900    410 -    true 4.7  59 -    false(reach) 0.17 33 -    unknown 5.4  250 -    unknown 5.5  250 -   
bitvector/num_conversion_1_true-unreach-call.i true 0.62 10.0 -    true 12    2100 -    true 0.53 23 -    true 1.4  130 -    true 0.063 12 -    false(reach) 0.28 36 -    unknown 7.4  270 -    false(reach) 6.8  270 -   
bitvector/num_conversion_2_true-unreach-call.i true 0.61 10.0 -    true 12    1900 -    true 0.55 23 -    true 17    250 -    true 0.071 12 -    false(reach) 0.26 36 -    unknown 7.1  270 -    false(reach) 8.3  280 -   
bitvector/parity_true-unreach-call.i true 1.3  10.0 -    true 850    2500 -    true 2.8  27 -    timeout 910    1300 -    true 0.21 13 -    false(reach) 0.15 33 -    unknown 5.3  250 -    false(reach) 5.7  250 -   
bitvector/sum02_true-unreach-call.i true 27    31 -    true 420    1900 -    true 0.61 25 -    timeout 900    760 -    true 0.074 12 -    false(reach) 0.16 34 -    unknown 5.2  250 -    unknown 5.3  240 -   
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c timeout 920    1000 -    witness invalid (error (invalid c code)) 6.2  360 1.8  witness confirmed 4.7  180 9.9  witness confirmed 5.7  290 15    witness confirmed 6.9  170 5.7  witness confirmed 5.4  70 9.6  unknown 5.4  250 -    unknown 5.8  240 -   
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c out of memory 83    15000 -    witness invalid (error (invalid c code)) 6.4  320 1.8  witness confirmed 4.3  150 29    witness confirmed 87    1500 3.1  witness confirmed 6.0  140 21    witness confirmed 6.7  110 29    unknown 12    430 -    witness confirmed 49    1200 42   
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c out of memory 85    15000 -    witness invalid (error (invalid c code)) 3.6  250 1.9  witness confirmed 1.0  53 3.3  witness confirmed 4.5  260 4.1  witness confirmed 6.7  150 3.5  witness confirmed 1.6  54 3.1  unknown 7.7  270 -    witness confirmed 9.3  300 5.1 
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c timeout 920    1000 -    true 890    6800 -    true 54    760 -    true 33    700 -    true 3.1  180 -    timeout 920    52 -    unknown 5.5  240 -    unknown 5.8  240 -   
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c out of memory 84    15000 -    timeout 920    7700 -    true 50    640 -    true 30    1200 -    true 2.8  150 -    false(reach) 6.9  110 -    unknown 13    430 -    false(reach) 62    1200 -   
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c out of memory 85    15000 -    timeout 920    7900 -    true 47    590 -    true 35    1200 -    true 3.3  150 -    true 9.1  51 -    true 16    700 -    timeout 920    1400 -   
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c out of memory 130    15000 -    true 860    2200 -    true 850    620 -    aborted 130    1200 -    true 380    280 -    unknown 570    760 -    unknown 6.0  240 -    unknown 5.5  250 -   
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c out of memory 130    15000 -    timeout 890    5800 -    true 92    770 -    true 64    700 -    true 1.8  190 -    true 79    73 -    true 17    690 -    timeout 920    1900 -   
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c out of memory 120    15000 -    true 860    3800 -    true 93    670 -    true 63    1200 -    true 1.8  160 -    true 320    120 -    true 40    1000 -    unknown 850    1400 -   
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c out of memory 120    15000 -    true 860    3800 -    true 95    690 -    true 63    710 -    true 1.9  170 -    true 130    85 -    true 37    1200 -    timeout 920    1400 -   
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c out of memory 120    15000 -    true 870    7300 -    true 89    710 -    true 64    710 -    true 1.6  180 -    unknown 2.5  42 -    unknown 5.1  240 -    unknown 5.1  240 -   
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c out of memory 120    15000 -    true 870    7100 -    true 95    710 -    true 64    700 -    true 1.6  180 -    unknown 2.5  48 -    unknown 5.4  240 -    unknown 5.7  240 -   
bitvector/soft_float_1_true-unreach-call.c.cil.c timeout 920    7000 -    true 860    2200 -    true 2.9  43 -    true 11    340 -    true 0.18 17 -    false(reach) 0.40 44 -    unknown 8.1  270 -    false(reach) 9.5  300 -   
bitvector/soft_float_2_true-unreach-call.c.cil.c unknown 870    9400 -    true 25    1900 -    true 2.3  42 -    true 13    300 -    true 0.070 14 -    false(reach) 0.82 59 -    unknown 5.3  240 -    unknown 5.3  240 -   
bitvector/soft_float_3_true-unreach-call.c.cil.c timeout 920    15000 -    true 850    410 -    true 2.2  41 -    timeout 920    8900 -    true 0.084 14 -    false(reach) 1.8  77 -    unknown 5.6  240 -    unknown 5.6  240 -   
bitvector/soft_float_4_true-unreach-call.c.cil.c timeout 920    5500 -    true 860    2200 -    true 5.6  48 -    true 64    260 -    true 4.1  22 -    false(reach) 0.38 44 -    unknown 6.1  240 -    false(reach) 9.0  300 -   
bitvector/soft_float_5_true-unreach-call.c.cil.c timeout 900    15000 -    true 25    1900 -    true 2.3  43 -    true 13    300 -    true 0.062 14 -    false(reach) 0.87 61 -    unknown 5.3  240 -    unknown 5.1  240 -   
bitvector-regression/implicitfloatconversion_false-unreach-call.i unknown 0.040 1.00 -    witness confirmed 0.85 86 1.4  unknown 0.12 23 -    witness confirmed 1.6  170 1.3  witness unconfirmed 0.083 11 1.4  witness confirmed 0.15 32 1.4  unknown 5.4  240 -    unknown 5.2  240 -   
bitvector-regression/implicitunsignedconversion_false-unreach-call.i witness missing 0.11 10.0 -    witness confirmed 0.80 86 1.4  unknown 0.093 23 -    witness confirmed 1.6  160 1.4  witness confirmed 0.065 11 1.7  witness confirmed 0.12 32 1.4  witness confirmed 5.0  250 1.4  witness confirmed 5.6  250 1.3 
bitvector-regression/integerpromotion_false-unreach-call.i witness missing 0.16 13 -    witness invalid (error (invalid c code)) 1.2  99 1.5  witness confirmed 0.13 25 1.6  witness confirmed 2.3  200 1.9  witness confirmed 2.0  17 1.7  witness confirmed 0.30 32 1.6  unknown 5.5  250 -    witness confirmed 5.6  250 1.7 
bitvector-regression/signextension2_false-unreach-call.i witness missing 0.34 10.0 -    witness invalid (error (invalid c code)) 1.1  97 1.5  witness confirmed 0.13 25 1.7  witness confirmed 2.1  200 1.8  witness confirmed 0.97 16 1.7  witness confirmed 0.17 32 1.6  witness confirmed 6.5  250 1.7  witness confirmed 5.5  250 1.7 
bitvector-regression/signextension_false-unreach-call.i true 0.25 10.0 -    witness invalid (error (invalid c code)) 1.3  110 1.5  witness confirmed 0.13 25 2.0  witness confirmed 2.2  200 1.9  witness confirmed 2.0  19 1.7  witness confirmed 0.14 32 1.6  true 5.3  250 -    true 5.5  250 -   
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true 0.087 10.0 -    true 0.54 73 -    true 0.50 23 -    true 1.4  140 -    true 0.067 11 -    true 0.14 27 -    true 5.1  250 -    true 5.2  250 -   
bitvector-regression/integerpromotion_true-unreach-call.i true 0.094 10.0 -    true 0.86 79 -    true 0.57 25 -    true 1.6  140 -    true 0.079 16 -    true 0.16 27 -    unknown 5.2  240 -    false(reach) 5.5  250 -   
bitvector-regression/signextension2_true-unreach-call.i true 0.30 9.0 -    true 0.83 78 -    true 0.59 25 -    true 1.5  140 -    true 0.065 16 -    true 0.25 27 -    true 5.5  250 -    true 5.7  250 -   
bitvector-regression/signextension_true-unreach-call.i false(reach) 0.35 10.0 -    true 0.92 85 -    true 0.55 26 -    true 1.6  140 -    true 0.079 16 -    true 0.26 27 -    false(reach) 5.6  250 -    false(reach) 5.3  250 -   
bitvector-loops/diamond_false-unreach-call2.i true 2.9  12 -    witness invalid (error (invalid c code)) 0.96 98 1.7  witness confirmed 0.13 24 1.9  witness confirmed 1.8  170 2.4  witness confirmed 0.60 12 2.4  witness confirmed 0.35 43 1.9  witness confirmed 5.6  250 1.5  witness confirmed 7.3  240 2.3 
bitvector-loops/overflow_false-unreach-call1.i unknown 0.027 0 -    true 2.7  150 -    true 0.49 23 -    true 120    1100 -    true 0.065 11 -    timeout 920    220 -    timeout 920    660 -    timeout 920    1200 -   
../../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 status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness
total files 47 10000 200000 - 47 20000 130000 16 47 1800 9200 53 47 5700 34000 36 47 470 2600 42 47 6500 38000 54 47 1600 17000 4.6 47 7600 21000 56
correct results 17 58 230 - 33 16000 91000 2.8 44 1800 9100 53 40 870 18000 36 45 470 2600 41 19 550 950 54 13 170 6000 4.6 11 120 3800 54
false negatives 2 3.1 22 - 1 2.7 150 0 1 0.49 23 0 1 120 1100 0 1 0.065 11 0 0 - - - 1 5.3 250 0 1 5.5 250 0
false positives 1 0.35 10.0 - 0 - - - 0 - - - 0 - - - 0 - - - 18 14 830 0 1 5.6 250 0 11 140 4300 0
false properties 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
score (47 files, max score: 83) 4 - - - 52 - - - 68 - - - 58 - - - 69 - - - -80 - - - 5 - - - -62 - - -
Tool Beagle 1.1 Cascade 0.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Seahorn Ultimate Automizer r12950 Ultimate Kojak r12950