Tool BLAST 2.7.3 Cascade 0.1 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-18 12:10 [[ 14-12-19 11:22 ]] 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-11 14:25 [[ 14-12-22 07:45 ]] 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 ]] -trace [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cascade.14-12-18_1210.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-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 [[ -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-12-11_1425.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 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-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 status time(s) memory(MB) time(s) for witness
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c witness confirmed 120    140 4.1  witness invalid (error (invalid c code)) 5.7  260 2.3  witness confirmed 0.84 78 4.1  witness confirmed 5.1  260 4.1  witness confirmed 9.9  64 4.2  witness confirmed 1.4  55 3.9  witness confirmed 7.1  360 4.1  witness confirmed 38    1200 3.7  timeout 920    1800 -   
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c witness confirmed 18    84 4.0  witness invalid (error (invalid c code)) 3.0  180 2.0  witness confirmed 0.25 33 4.0  witness confirmed 5.1  310 4.0  witness confirmed 3.5  25 4.1  witness invalid (assertion) 0.70 43 1.8  witness confirmed 3.1  160 4.0  witness confirmed 27    1200 3.0  timeout 920    1800 -   
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c witness confirmed 18    76 4.9  witness invalid (error (invalid c code)) 3.9  230 2.1  witness confirmed 0.37 41 5.1  witness confirmed 6.2  320 4.7  witness confirmed 5.8  37 4.7  witness confirmed 0.95 49 4.8  witness confirmed 4.1  200 5.2  witness confirmed 32    1200 3.9  timeout 920    1800 -   
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c witness confirmed 6.1  37 4.1  witness invalid (error (invalid c code)) 2.6  160 1.9  unknown 0.18 32 -    witness confirmed 3.5  250 3.8  witness confirmed 3.2  22 4.2  witness confirmed 0.62 41 4.1  witness confirmed 2.2  120 4.2  witness confirmed 18    670 3.5  witness confirmed 100    1200 3.5 
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 530    310 -    out of memory 34    15000 -    true 4.8  79 -    true 3.6  200 -    true 0.36 62 -    true 1.3  50 -    true 13    380 -    true 39    1200 -    timeout 920    2600 -   
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 130    150 -    true 23    1700 -    true 1.5  35 -    true 71    540 -    true 0.18 26 -    true 0.78 41 -    true 6.4  230 -    true 34    1200 -    timeout 920    1600 -   
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true 160    150 -    out of memory 38    15000 -    true 1.3  35 -    true 3.4  200 -    true 0.15 22 -    true 0.67 40 -    true 4.8  160 -    true 34    1200 -    timeout 920    1800 -   
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 280    260 -    true 260    6600 -    true 2.1  43 -    true 4.1  210 -    true 0.24 34 -    true 0.93 46 -    true 6.2  210 -    true 39    1200 -    timeout 920    1800 -   
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 1.6  23 -    true 1.6  110 -    true 0.73 28 -    true 1.9  150 -    true 0.081 16 -    true 0.31 31 -    true 2.3  85 -    true 11    420 -    true 44    1200 -   
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 1.8  24 -    true 2.3  140 -    true 0.93 30 -    true 2.6  170 -    true 0.14 19 -    true 0.41 33 -    true 3.2  120 -    true 10    410 -    true 470    1600 -   
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c witness confirmed 15    37 4.4  witness invalid (error (invalid c code)) 3.3  220 1.8  witness confirmed 1.6  67 4.5  witness confirmed 4.9  280 5.4  witness confirmed 3.3  180 4.4  witness confirmed 2.5  61 4.2  witness confirmed 3.1  150 4.5  witness confirmed 8.9  280 3.0  witness confirmed 19    710 4.6 
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c witness confirmed 15    36 4.3  witness invalid (exception) 3.9  230 1.8  witness confirmed 1.6  67 4.2  witness confirmed 4.4  280 5.2  witness confirmed 3.5  180 4.7  witness confirmed 2.9  62 4.1  witness confirmed 3.0  140 4.4  witness confirmed 9.2  270 3.2  witness confirmed 17    680 4.7 
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c witness confirmed 15    38 4.4  witness invalid (error (invalid c code)) 4.0  220 1.8  witness confirmed 1.9  79 4.3  witness confirmed 4.5  290 5.3  witness confirmed 4.0  220 4.5  witness confirmed 3.2  61 4.3  witness confirmed 3.1  150 4.9  witness confirmed 9.5  270 3.6  witness confirmed 17    690 4.9 
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c witness confirmed 15    36 4.3  witness invalid (error (invalid c code)) 3.7  230 1.9  witness confirmed 1.6  67 4.4  witness confirmed 4.5  280 5.8  witness confirmed 3.4  180 4.4  witness confirmed 3.2  62 4.1  witness confirmed 3.0  150 4.3  witness confirmed 8.9  270 3.2  witness confirmed 17    690 5.8 
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c witness confirmed 0.093 16 2.0  witness invalid (error (invalid c code)) 2.6  150 1.9  unknown 0.14 26 -    witness confirmed 23    430 2.1  witness confirmed 1.7  180 2.0  witness confirmed 0.48 43 1.9  witness unconfirmed 3.2  160 1.8  witness confirmed 7.5  270 2.2  witness confirmed 8.7  280 2.3 
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c exception (gremlins) 2.0  20 -    witness invalid (error (invalid c code)) 4.3  250 1.9  witness confirmed 11    230 15    witness confirmed 190    640 3.0  witness confirmed 2.2  220 14    witness confirmed 5.6  83 14    witness confirmed 4.2  180 14    witness confirmed 15    680 4.0  witness confirmed 68    1800 26   
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c exception (gremlins) 2.2  21 -    witness invalid (error (invalid c code)) 4.9  280 1.9  witness confirmed 2.7  100 19    witness confirmed 79    900 3.0  witness confirmed 2.6  240 19    witness confirmed 6.4  89 19    true 7.2  240 -    witness confirmed 14    420 4.6  witness confirmed 62    2300 23   
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c exception (gremlins) 1.9  20 -    witness invalid (exception) 4.1  260 1.8  witness confirmed 2.4  98 3.3  witness confirmed 67    770 3.9  witness confirmed 2.4  230 3.3  witness confirmed 2.9  69 3.2  witness confirmed 3.8  190 3.3  witness confirmed 12    410 3.3  witness confirmed 31    1800 3.6 
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c exception (gremlins) 3.4  19 -    witness invalid (exception) 2.5  150 1.7  witness confirmed 0.16 27 2.6  witness confirmed 67    630 3.2  witness confirmed 2.1  190 3.2  witness confirmed 0.78 49 2.5  witness confirmed 3.3  160 2.7  witness confirmed 11    290 2.6  witness confirmed 13    440 3.1 
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c witness confirmed 3.1  27 4.2  witness invalid (exception) 3.9  240 1.8  witness confirmed 2.2  98 3.5  witness confirmed 3.3  230 4.1  witness confirmed 2.2  210 3.6  witness confirmed 1.0  48 3.3  witness confirmed 3.5  170 3.5  witness confirmed 7.6  270 3.1  witness confirmed 13    430 4.0 
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c witness confirmed 3.3  27 3.3  witness invalid (error (invalid c code)) 3.8  230 1.8  true 2.1  87 -    witness confirmed 3.2  230 3.9  witness confirmed 2.0  190 3.4  witness confirmed 1.2  48 3.3  witness confirmed 3.4  170 3.4  witness confirmed 8.4  270 3.1  witness confirmed 14    430 3.5 
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c witness confirmed 0.086 18 1.8  witness invalid (error (invalid c code)) 2.5  160 1.8  witness confirmed 0.15 27 1.9  witness confirmed 2.4  210 1.9  witness confirmed 2.2  190 1.9  witness confirmed 0.49 38 1.8  witness timeout 3.0  170 91    witness confirmed 6.2  240 2.0  witness confirmed 8.8  280 1.9 
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 89    76 -    crash 280    3400 -    true 57    810 -    true 33    270 -    true 3.3  170 -    true 11    53 -    true 5.0  190 -    true 19    1200 -    timeout 920    1500 -   
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c timeout 920    320 -    timeout 920    7300 -    true 59    830 -    true 30    640 -    true 3.4  180 -    true 6.2  49 -    true 4.8  190 -    true 19    1200 -    timeout 920    1800 -   
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 220    120 -    timeout 920    7100 -    true 64    990 -    true 35    640 -    true 3.9  220 -    true 12    52 -    true 5.1  180 -    true 21    1200 -    timeout 920    1500 -   
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c timeout 920    330 -    timeout 920    7400 -    true 58    830 -    true 30    370 -    true 3.4  180 -    true 13    52 -    true 5.0  190 -    true 19    1200 -    timeout 920    1800 -   
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 920    300 -    true 870    9100 -    true 97    410 -    true 64    640 -    true 1.6  160 -    true 17    54 -    true 6.5  230 -    true 19    680 -    timeout 920    1800 -   
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 0.82 18 -    true 870    6300 -    true 3.4  39 -    true 1.8  140 -    true 0.12 14 -    true 0.37 36 -    true 1.9  81 -    true 7.0  280 -    timeout 920    3300 -   
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 0.80 17 -    true 870    4600 -    true 1.3  31 -    true 1.5  140 -    true 0.10 12 -    true 0.25 33 -    true 1.7  63 -    true 6.2  250 -    true 8.5  270 -   
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 250    130 -    true 880    5400 -    true 140    800 -    true 63    630 -    true 2.0  190 -    true 7.0  52 -    true 5.7  220 -    true 21    1200 -    timeout 920    1800 -   
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 270    140 -    true 890    5400 -    true 150    800 -    true 64    420 -    true 2.0  190 -    true 59    71 -    true 5.9  220 -    true 17    680 -    timeout 920    1400 -   
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 270    140 -    true 880    5400 -    true 140    800 -    true 63    640 -    true 2.0  190 -    true 20    54 -    true 5.9  220 -    true 17    690 -    timeout 920    1400 -   
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 920    300 -    true 860    4300 -    true 140    810 -    true 64    720 -    true 2.2  200 -    true 86    79 -    true 6.6  220 -    true 23    1300 -    timeout 920    1800 -   
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 920    300 -    true 870    4400 -    true 140    810 -    true 63    710 -    true 2.0  200 -    true 140    100 -    true 6.4  210 -    true 22    2000 -    timeout 920    1900 -   
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 140    85 -    true 870    4300 -    true 150    800 -    true 65    640 -    true 2.1  190 -    true 28    58 -    true 6.1  210 -    true 21    1200 -    timeout 920    1800 -   
locks/test_locks_14_false-unreach-call.c witness confirmed 0.11 17 47    witness invalid (error (invalid c code)) 1.4  110 1.5  witness confirmed 0.15 25 46    witness confirmed 62    1100 47    witness confirmed 0.93 44 45    witness confirmed 0.26 36 20    witness unconfirmed 1.6  110 1.7  witness confirmed 6.6  250 2.1  witness confirmed 7.9  270 1.6 
locks/test_locks_15_false-unreach-call.c witness timeout 0.10 14 91    witness invalid (error (invalid c code)) 1.6  120 1.5  witness timeout 0.14 25 91    witness timeout 62    1100 91    witness confirmed 1.1  48 76    witness confirmed 0.33 36 56    witness unconfirmed 1.6  83 1.7  witness confirmed 6.3  250 1.9  witness confirmed 8.6  280 1.7 
locks/test_locks_10_true-unreach-call.c timeout 920    500 -    timeout 900    5300 -    true 5.7  71 -    true 13    620 -    true 0.18 24 -    true 0.32 31 -    true 2.3  83 -    true 14    700 -    true 8.2  280 -   
locks/test_locks_11_true-unreach-call_false-termination.c timeout 920    560 -    timeout 900    5500 -    true 6.8  80 -    true 42    1100 -    true 0.20 28 -    true 0.24 31 -    true 2.8  89 -    true 14    900 -    true 7.3  270 -   
locks/test_locks_12_true-unreach-call_false-termination.c timeout 920    640 -    timeout 920    6300 -    true 8.3  88 -    true 120    1100 -    true 0.23 32 -    true 0.34 32 -    true 3.5  87 -    true 19    1900 -    true 7.4  280 -   
locks/test_locks_13_true-unreach-call.c timeout 920    540 -    timeout 920    6300 -    true 9.3  100 -    true 120    1100 -    true 0.26 36 -    true 0.24 33 -    true 5.2  95 -    true 33    3200 -    true 8.1  270 -   
locks/test_locks_14_true-unreach-call.c timeout 920    690 -    true 870    2700 -    true 12    120 -    true 120    1100 -    true 0.30 40 -    true 0.26 33 -    true 8.4  98 -    true 80    5800 -    true 8.5  270 -   
locks/test_locks_15_true-unreach-call_false-termination.c timeout 920    560 -    true 870    2700 -    true 14    130 -    true 120    1100 -    true 0.33 45 -    true 0.29 33 -    true 15    110 -    true 150    6100 -    true 9.4  310 -   
locks/test_locks_5_true-unreach-call_false-termination.c true 16    69 -    true 160    4200 -    true 1.7  34 -    true 1.8  140 -    true 0.11 12 -    true 0.20 29 -    true 1.7  68 -    true 7.1  270 -    true 5.8  250 -   
locks/test_locks_6_true-unreach-call_false-termination.c true 32    130 -    true 190    4700 -    true 2.3  37 -    true 2.1  150 -    true 0.12 13 -    true 0.20 30 -    true 1.8  77 -    true 8.0  280 -    true 6.1  240 -   
locks/test_locks_7_true-unreach-call_false-termination.c true 94    160 -    true 350    4600 -    true 2.8  41 -    true 2.6  200 -    true 0.12 15 -    true 0.30 30 -    true 1.8  78 -    true 9.2  280 -    true 6.6  250 -   
locks/test_locks_8_true-unreach-call_false-termination.c true 190    180 -    true 690    5100 -    true 3.5  49 -    true 3.4  200 -    true 0.16 18 -    true 0.30 30 -    true 1.9  76 -    true 10    300 -    true 6.9  280 -   
locks/test_locks_9_true-unreach-call.c true 430    340 -    timeout 900    5300 -    true 4.2  58 -    true 5.6  240 -    true 0.17 21 -    true 0.29 31 -    true 2.1  79 -    true 11    320 -    true 7.3  270 -   
../../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 status time(s) memory(MB) time(s) for witness
total files 48 13000 8200 180 48 19000 170000 33 48 1300 11000 210 48 1800 24000 200 48 87 5200 210 48 440 2300 160 48 210 7600 160 48 990 47000 56 48 18000 54000 94
correct results 32 3300 3100 93 19 11000 82000 0 44 1300 11000 120 47 1800 23000 110 48 87 5200 210 47 440 2300 150 43 200 6800 63 48 990 47000 56 29 1000 18000 94
false negatives 0 - - - 0 - - - 1 2.1 87 0 0 - - - 0 - - - 0 - - - 1 7.2 240 0 0 - - - 0 - - -
false positives 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
false properties 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
score (48 files, max score: 78) 51 - - - 38 - - - 62 - - - 77 - - - 78 - - - 77 - - - 61 - - - 78 - - - 43 - - -
Tool BLAST 2.7.3 Cascade 0.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Seahorn SMACK Ultimate Automizer r12950 Ultimate Kojak r12950