Tool BLAST 2.7.3 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Seahorn SMACK 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-11-25 03:45 [[ 14-12-21 23:31 ]] 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-11-26 16:05 [[ 14-12-22 07:46 ]] 14-11-12 22:41 [[ 14-12-21 23:12 ]] 14-11-16 20:08 [[ 14-12-21 23:18 ]]
Options -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr [[ -witness-check -noout -timelimit 90 -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 ]] --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 ]] --errorwitness witness.graphml [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/smack.14-11-26_1605.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/smack-corral/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=true -tokenize -deletePragmas ]] 32bit simple [[ -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 simple [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/ultimatekojak.14-11-16_2008.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
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 920    410 -    true 100    5400 -    witness confirmed 13    490 8.8  true 0.85 170 -    timeout 920    960 -    timeout 920    3200 -    unknown 6.3  240 -    unknown 6.3  240 -   
ntdrivers/diskperf_false-unreach-call.i.cil.c witness confirmed 6.8  180 4.1  witness confirmed 1.9  110 4.7  witness confirmed 69    460 4.8  unknown 0.58 81 -    witness confirmed 0.88 34 3.9  witness confirmed 5.7  260 4.0  unknown 5.9  240 -    unknown 6.8  240 -   
ntdrivers/floppy_false-unreach-call.i.cil.c witness confirmed 5.2  120 5.0  unknown 2.0  61 -    witness confirmed 17    870 5.3  unknown 87    1100 -    witness confirmed 1.3  35 4.1  witness confirmed 95    2700 4.6  unknown 5.8  240 -    unknown 5.7  240 -   
ntdrivers/kbfiltr_false-unreach-call.i.cil.c witness confirmed 49    96 5.3  error 850    11000 -    witness confirmed 5.0  240 6.1  true 0.29 55 -    witness confirmed 1.1  51 4.6  witness confirmed 2.9  140 4.7  unknown 5.5  240 -    unknown 5.7  240 -   
ntdrivers/parport_false-unreach-call.i.cil.c witness confirmed 5.5  84 5.0  witness confirmed 23    680 5.3  witness confirmed 76    3300 5.9  out of memory 290    15000 -    witness confirmed 24    290 4.7  witness confirmed 110    3300 5.3  unknown 6.1  240 -    unknown 6.6  240 -   
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 330    200 -    true 16    150 -    true 5.1  210 -    unknown 560    9100 -    true 2.5  97 -    true 23    550 -    unknown 6.1  240 -    unknown 6.9  240 -   
ntdrivers/diskperf_true-unreach-call.i.cil.c true 130    310 -    true 27    1000 -    true 68    700 -    unknown 0.57 81 -    true 0.87 31 -    true 10    280 -    unknown 5.9  240 -    unknown 5.6  240 -   
ntdrivers/floppy2_true-unreach-call.i.cil.c true 0.43 38 -    true 160    1200 -    true 150    2200 -    out of memory 220    15000 -    true 1.1  43 -    true 120    5400 -    unknown 7.6  250 -    unknown 8.2  240 -   
ntdrivers/floppy_true-unreach-call.i.cil.c exception (gremlins) 61    160 -    unknown 2.0  59 -    true 91    2000 -    out of memory 210    15000 -    true 1.4  32 -    true 260    4700 -    unknown 5.7  240 -    unknown 6.1  240 -   
ntdrivers/parport_true-unreach-call.i.cil.c timeout 920    490 -    true 850    5500 -    true 82    3800 -    out of memory 290    15000 -    timeout 920    8400 -    true 120    2900 -    unknown 6.6  240 -    unknown 6.2  250 -   
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c witness confirmed 22    48 33    witness confirmed 62    1000 34    timeout 920    2900 -    witness confirmed 28    580 34    witness confirmed 5.6  71 34    witness confirmed 4.9  220 17    unknown 60    1300 -    unknown 150    2100 -   
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c witness confirmed 15    43 8.2  witness confirmed 16    350 7.7  timeout 920    1500 -    witness confirmed 33    650 7.7  witness confirmed 3.9  68 7.7  witness confirmed 5.0  210 6.3  unknown 31    740 -    unknown 94    2000 -   
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c witness confirmed 15    44 8.7  witness confirmed 16    350 8.6  timeout 920    1500 -    witness confirmed 30    650 7.8  witness confirmed 3.6  68 7.6  witness confirmed 5.1  210 6.3  unknown 34    760 -    unknown 92    2000 -   
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c witness confirmed 15    44 8.2  witness confirmed 15    340 7.7  timeout 920    1500 -    witness confirmed 35    650 7.9  witness confirmed 3.1  68 7.5  witness confirmed 5.2  210 6.3  unknown 33    750 -    unknown 80    2000 -   
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c witness confirmed 9.5  39 50    witness confirmed 16    320 48    witness confirmed 510    2300 30    witness confirmed 43    920 52    witness confirmed 1.8  54 48    witness confirmed 5.1  220 79    witness confirmed 12    410 34    witness timeout 49    1900 93   
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c witness confirmed 6.1  34 11    witness confirmed 16    310 11    witness confirmed 430    1100 11    witness confirmed 47    1000 11    witness confirmed 1.3  54 11    witness confirmed 5.4  210 17    witness confirmed 13    420 9.1  witness confirmed 53    1900 45   
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c witness confirmed 6.2  33 12    witness confirmed 17    310 11    witness confirmed 250    1100 18    witness confirmed 48    1000 11    witness confirmed 1.8  54 11    witness confirmed 5.2  230 17    witness confirmed 13    420 9.4  witness confirmed 44    1900 21   
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c witness confirmed 6.5  34 11    witness confirmed 16    310 11    witness confirmed 250    1100 18    witness confirmed 47    1000 11    witness confirmed 1.4  54 11    witness confirmed 5.1  230 17    witness confirmed 12    410 9.5  witness confirmed 40    1900 29   
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c witness confirmed 380    230 3.2  witness confirmed 17    310 3.2  timeout 920    1100 -    witness confirmed 48    1000 3.1  witness confirmed 3.0  75 3.1  witness confirmed 6.4  230 4.0  witness confirmed 420    1200 3.3  timeout 920    1900 -   
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c witness confirmed 210    150 23    witness confirmed 16    310 23    timeout 920    1900 -    witness confirmed 48    1100 22    witness confirmed 4.0  73 22    witness confirmed 6.0  220 55    witness confirmed 22    730 18    witness timeout 72    1900 94   
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 920    440 -    witness confirmed 86    780 3.1  timeout 920    2000 -    witness confirmed 47    1000 3.3  witness confirmed 21    150 3.1  witness confirmed 39    330 3.6  timeout 920    2400 -    timeout 920    1900 -   
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c witness confirmed 210    150 24    witness confirmed 16    310 23    witness confirmed 500    1900 21    witness confirmed 47    1100 22    witness confirmed 6.3  74 22    witness confirmed 6.0  230 55    witness confirmed 24    730 18    witness timeout 78    1900 94   
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 920    560 -    witness confirmed 84    780 3.2  timeout 920    1900 -    witness confirmed 45    1000 3.1  witness confirmed 19    150 3.1  witness confirmed 40    340 3.5  timeout 920    1700 -    timeout 920    1900 -   
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c witness confirmed 86    120 15    witness confirmed 17    310 15    timeout 920    1800 -    witness confirmed 49    1100 15    witness confirmed 2.5  69 14    witness confirmed 6.0  240 24    witness confirmed 15    450 11    unknown 90    1900 -   
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c witness confirmed 310    160 3.2  witness confirmed 16    310 3.1  timeout 920    1100 -    witness confirmed 50    1000 3.2  witness confirmed 3.2  74 3.1  witness confirmed 6.5  220 3.5  witness confirmed 410    1200 3.2  timeout 920    2200 -   
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c witness confirmed 210    150 23    witness confirmed 16    310 24    timeout 920    1900 -    witness confirmed 46    1100 23    witness confirmed 5.4  74 22    witness confirmed 6.2  220 54    witness confirmed 24    1000 18    unknown 83    1900 -   
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c witness confirmed 310    160 3.2  witness confirmed 16    310 3.2  timeout 920    970 -    witness confirmed 46    1000 3.1  witness confirmed 3.9  75 3.0  witness confirmed 6.4  230 3.5  witness confirmed 420    1200 3.3  timeout 920    1900 -   
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 920    560 -    witness confirmed 82    790 3.3  timeout 920    1700 -    witness confirmed 50    1000 3.2  witness confirmed 22    150 3.1  witness confirmed 37    350 3.7  timeout 920    1800 -    timeout 920    2200 -   
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c witness confirmed 380    230 3.2  witness confirmed 17    310 3.1  timeout 920    1100 -    witness confirmed 49    1000 3.2  witness confirmed 3.7  76 3.1  witness confirmed 6.2  240 3.6  witness confirmed 400    1200 3.3  timeout 920    1900 -   
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c timeout 920    550 -    true 850    5000 -    true 74    1900 -    true 6.2  570 -    true 9.3  52 -    false(reach) 20    320 -    timeout 920    1700 -    unknown 410    2700 -   
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 370    200 -    true 850    2500 -    true 22    860 -    true 6.7  650 -    true 7.0  51 -    true 23    280 -    timeout 920    1600 -    timeout 920    2600 -   
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c timeout 920    410 -    true 850    2500 -    true 22    750 -    true 6.9  650 -    true 11    53 -    true 24    280 -    timeout 920    1500 -    timeout 920    2600 -   
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 360    240 -    true 850    2500 -    true 22    750 -    true 6.7  650 -    true 8.3  52 -    false(reach) 20    300 -    timeout 920    1600 -    unknown 460    3100 -   
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 800    300 -    true 850    1800 -    true 73    1900 -    true 8.9  910 -    true 59    74 -    true 310    360 -    timeout 920    2600 -    timeout 920    2700 -   
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 920    430 -    true 850    1800 -    true 32    1300 -    true 9.6  1000 -    true 36    65 -    true 310    350 -    false(reach) 690    1600 -    timeout 920    2700 -   
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 920    440 -    true 850    1800 -    true 130    1900 -    true 9.9  1000 -    true 75    76 -    true 320    400 -    timeout 920    2300 -    timeout 920    3100 -   
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 920    420 -    true 850    1900 -    true 140    1900 -    true 9.8  1000 -    true 100    85 -    true 320    360 -    timeout 920    5000 -    timeout 920    2800 -   
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 920    420 -    true 850    1800 -    true 98    1900 -    true 9.7  1000 -    true 93    68 -    true 310    350 -    timeout 920    4200 -    timeout 920    2600 -   
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 920    420 -    true 850    1900 -    true 57    1900 -    true 10    1000 -    true 69    76 -    true 310    370 -    timeout 920    4800 -    timeout 920    2600 -   
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 920    550 -    true 850    1800 -    true 69    1900 -    true 9.7  1000 -    true 34    65 -    true 310    350 -    timeout 920    2800 -    timeout 920    2800 -   
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 920    560 -    true 850    1900 -    true 120    1900 -    true 10    1000 -    true 66    74 -    true 320    370 -    timeout 920    2800 -    timeout 920    3000 -   
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 920    440 -    true 850    1800 -    true 150    1900 -    true 10    1000 -    true 66    73 -    true 320    380 -    timeout 920    5300 -    timeout 920    2600 -   
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 920    540 -    true 850    1900 -    true 110    1900 -    true 9.8  1000 -    true 73    74 -    true 310    360 -    false(reach) 410    1600 -    timeout 920    2600 -   
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 920    420 -    true 850    1800 -    true 160    1900 -    true 9.9  1000 -    true 68    75 -    true 320    370 -    timeout 920    6100 -    timeout 920    2900 -   
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 920    420 -    true 850    1800 -    true 92    1900 -    true 9.8  1000 -    true 46    66 -    true 310    370 -    timeout 920    4000 -    timeout 920    2600 -   
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 920    490 -    true 850    1800 -    true 160    1900 -    true 9.8  1000 -    true 58    69 -    true 320    370 -    timeout 920    5500 -    timeout 920    2900 -   
../../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 46 22000 13000 260 46 17000 70000 260 46 17000 73000 130 46 2600 100000 250 46 2900 13000 260 46 6000 34000 400 46 20000 76000 140 46 22000 86000 380
correct results 26 4200 3400 260 42 16000 53000 260 32 4000 51000 130 36 990 34000 250 44 1000 3300 260 43 5100 30000 400 12 1800 9400 140 3 140 5600 95
false negatives 0 - - - 1 100 5400 0 0 - - - 2 1.1 220 0 0 - - - 0 - - - 0 - - - 0 - - -
false positives 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 2 40 610 0 2 1100 3200 0 0 - - -
false properties 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
score (46 files, max score: 68) 32 - - - 51 - - - 54 - - - 29 - - - 65 - - - 51 - - - 0 - - - 3 - - -
Tool BLAST 2.7.3 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Seahorn SMACK Ultimate Automizer r12950 Ultimate Kojak r12950