Tool BLAST 2.7.1 CPAchecker 1.1.10-svcomp13 ESBMC 1.20 LLBMC SV-COMP-13 Predator Symbiotic UFO 2012-10-22 Ultimate Automizer
Limits timelimit: 900 s, memlimit: 15360 MB
System CPU: Intel(R) Core(TM) i7-2600K CPU @ 3.40GHz with 4 cores, frequency: 3401 MHz; RAM: 16343684 kB
Date of run 2012-11-25 00:16 2012-11-14 06:53 2012-11-14 08:27 2012-11-17 03:16 2012-12-04 06:32 2012-12-03 03:44 2012-11-19 11:16 2012-12-14 13:52 2012-12-09 01:05
Options -alias bdd
-enable-recursion
-noprofile
-cref
-sv-comp
-lattice
-include-lattice symb		 -sv-comp13--explitp-pred
-heap 12000m
-disable-java-assertions		 -sv-comp13--combinations
-heap 12000m
-disable-java-assertions		 -t label
-m32		 --cex=${logfile_path_abs}/${test_name}.${sourcefile_name}.cex
../sv-benchmarks-trunk/ status time status time status time status time status time status time status time status time status time
ntdrivers-simplified/cdaudio_simpl1_unsafe.cil.c unsafe 91    unsafe 19    unsafe 2.7  safe 1.6  unsafe 0.24 unsafe 0.08 unsafe 2.2  unsafe 1.7  smtlibexception 24   
ntdrivers-simplified/floppy_simpl3_unsafe.cil.c unsafe 15    unsafe 8.4  unsafe 2.0  unsafe 0.94 unsafe 0.38 unsafe 0.25 unsafe 0.67 unsafe 0.97 smtlibexception 16   
ntdrivers-simplified/floppy_simpl4_unsafe.cil.c unsafe 14    unsafe 9.2  unsafe 2.3  unsafe 1.0  unsafe 0.47 unsafe 0.26 unsafe 1.3  unsafe 1.3  smtlibexception 48   
ntdrivers-simplified/kbfiltr_simpl2_unsafe.cil.c unsafe 4.5  unsafe 5.6  unsafe 1.9  unsafe 0.47 unsafe 0.14 unsafe 0.12 unsafe 0.53 unsafe 0.66 unsafe 23   
ntdrivers-simplified/cdaudio_simpl1_safe.cil.c safe 410    safe 19    safe 3.1  safe 1.4  safe 0.34 unsafe 0.07 safe 2.2  safe 1.2  smtlibexception 26   
ntdrivers-simplified/diskperf_simpl1_safe.cil.c safe 100    safe 13    safe 110    safe 0.69 safe 7.3  unsafe 0.05 safe 2.1  safe 0.83 smtlibexception 12   
ntdrivers-simplified/floppy_simpl3_safe.cil.c safe 120    safe 10    safe 2.3  safe 0.96 safe 0.36 unsafe 0.25 safe 0.65 safe 0.78 smtlibexception 15   
ntdrivers-simplified/floppy_simpl4_safe.cil.c safe 230    safe 12    safe 2.6  safe 1.1  safe 0.42 unsafe 0.26 safe 1.3  safe 0.86 smtlibexception 35   
ntdrivers-simplified/kbfiltr_simpl1_safe.cil.c safe 1.2  safe 3.9  safe 2.0  safe 0.39 safe 0.09 safe 0.11 safe 0.26 safe 0.43 smtlibexception 13   
ntdrivers-simplified/kbfiltr_simpl2_safe.cil.c safe 1.4  safe 4.2  safe 2.3  safe 0.54 safe 0.09 safe 0.29 safe 0.56 safe 0.44 smtlibexception 20   
ssh-simplified/s3_clnt_1_unsafe.cil.c unsafe 11    unsafe 5.5  unsafe 3.7  unsafe 25    unsafe 0.24 unsafe 0.04 unsafe 2.2  unsafe 2.5  unsafe 8.9 
ssh-simplified/s3_clnt_2_unsafe.cil.c unsafe 11    unsafe 6.7  unsafe 3.7  unsafe 23    unsafe 0.23 unsafe 0.06 unsafe 2.2  unsafe 2.6  unsafe 11   
ssh-simplified/s3_clnt_3_unsafe.cil.c unsafe 11    unsafe 5.8  unsafe 3.7  unsafe 35    unsafe 0.23 unsafe 0.04 unsafe 2.2  unsafe 2.7  unsafe 10   
ssh-simplified/s3_clnt_4_unsafe.cil.c unsafe 11    unsafe 5.7  unsafe 3.6  unsafe 24    unsafe 0.22 unsafe 0.04 unsafe 2.2  unsafe 2.7  unsafe 12   
ssh-simplified/s3_srvr_10_unsafe.cil.c unsafe 0.08 unsafe 2.3  unsafe 1.5  unsafe 0.54 unsafe 0.04 unsafe 0.29 timeout 900    unsafe 2.4  unsafe 5.3 
ssh-simplified/s3_srvr_11_unsafe.cil.c error 1.5  unsafe 6.2  unsafe 2.1  unsafe 49    unsafe 0.50 unsafe 0.73 timeout 900    unsafe 11    unsafe 21   
ssh-simplified/s3_srvr_12_unsafe.cil.c error 1.6  unsafe 5.0  unsafe 1.9  unsafe 26    unsafe 0.37 unsafe 0.75 timeout 900    unsafe 74    unsafe 18   
ssh-simplified/s3_srvr_13_unsafe.cil.c error 1.3  unsafe 3.8  unsafe 2.0  unsafe 10    unsafe 0.15 unsafe 3.7  timeout 900    unsafe 3.6  unsafe 14   
ssh-simplified/s3_srvr_14_unsafe.cil.c error 2.4  unsafe 5.2  unsafe 2.3  unsafe 2.2  unsafe 0.05 unsafe 1.8  timeout 900    unsafe 2.1  unsafe 7.4 
ssh-simplified/s3_srvr_1_unsafe.cil.c unsafe 2.1  unsafe 2.9  unsafe 1.7  unsafe 15    unsafe 0.13 unsafe 0.08 timeout 900    unsafe 1.4  unsafe 8.4 
ssh-simplified/s3_srvr_2_unsafe.cil.c unsafe 2.2  unsafe 2.9  unsafe 1.7  unsafe 9.4  unsafe 0.13 unsafe 0.06 timeout 900    unsafe 2.0  unsafe 9.5 
ssh-simplified/s3_srvr_6_unsafe.cil.c unsafe 0.08 unsafe 1.8  unsafe 110    unsafe 0.46 unsafe 0.04 unsafe 20    timeout 900    unsafe 1.0  unsafe 4.1 
ssh-simplified/s3_clnt_1_safe.cil.c safe 65    safe 6.6  safe 7.3  safe 250    safe 1.1  unsafe 1.5  safe 3.3  safe 2.2  safe 26   
ssh-simplified/s3_clnt_2_safe.cil.c timeout 910    safe 6.5  safe 7.2  safe 260    safe 1.1  unsafe 7.3  safe 3.3  safe 2.8  safe 25   
ssh-simplified/s3_clnt_3_safe.cil.c safe 160    safe 6.6  safe 7.2  safe 410    safe 1.1  unsafe 17    safe 3.3  safe 2.9  safe 27   
ssh-simplified/s3_clnt_4_safe.cil.c timeout 910    safe 6.7  safe 7.1  safe 270    safe 1.1  unsafe 4.7  safe 3.3  safe 2.2  safe 26   
ssh-simplified/s3_srvr_1_safe.cil.c unknown 0.05 safe 7.0  safe 2.2  safe 450    safe 1.7  unsafe 0.15 timeout 900    safe 0.39 safe 29   
ssh-simplified/s3_srvr_1a_safe.cil.c safe 0.57 safe 2.0  safe 1.2  safe 450    safe 0.41 unsafe 0.05 timeout 900    safe 1.9  safe 5.2 
ssh-simplified/s3_srvr_1b_safe.cil.c safe 0.56 safe 1.5  safe 1.1  safe 350    safe 0.35 safe 0.04 timeout 900    safe 0.86 safe 4.2 
ssh-simplified/s3_srvr_2_safe.cil.c safe 190    safe 5.9  safe 2.2  safe 450    safe 1.6  unsafe 0.13 timeout 900    safe 4.7  safe 29   
ssh-simplified/s3_srvr_3_safe.cil.c safe 200    safe 6.6  safe 89    safe 450    safe 1.5  unsafe 0.16 timeout 900    safe 5.4  safe 28   
ssh-simplified/s3_srvr_4_safe.cil.c safe 200    safe 6.1  safe 10    safe 450    safe 1.6  unsafe 0.17 timeout 900    safe 3.7  safe 29   
ssh-simplified/s3_srvr_6_safe.cil.c timeout 910    safe 12    safe 320    safe 450    safe 1.6  unsafe 20    timeout 900    safe 6.8  safe 33   
ssh-simplified/s3_srvr_7_safe.cil.c timeout 910    safe 7.6  safe 120    safe 450    safe 1.7  unsafe 5.5  timeout 900    safe 4.4  safe 31   
ssh-simplified/s3_srvr_8_safe.cil.c safe 100    safe 8.5  safe 2.2  safe 450    safe 1.4  unsafe 0.26 timeout 900    safe 5.4  safe 28   
locks/test_locks_14_unsafe.c unsafe 0.09 unsafe 1.6  unsafe 1.8  unsafe 0.34 unsafe 0.08 unsafe 0.05 timeout 900    unsafe 0.58 unsafe 3.9 
locks/test_locks_15_unsafe.c unsafe 0.11 unsafe 1.6  unsafe 1.8  unsafe 0.31 unsafe 0.09 unsafe 0.03 timeout 900    unsafe 0.60 unsafe 4.2 
locks/test_locks_10_safe.c timeout 910    safe 1.3  safe 6.4  safe 450    safe 3.5  safe 430    timeout 900    safe 0.40 safe 4.6 
locks/test_locks_11_safe.c timeout 910    safe 1.4  safe 24    safe 450    safe 4.1  timeout 900    timeout 900    safe 0.39 safe 4.9 
locks/test_locks_12_safe.c timeout 910    safe 1.4  safe 110    safe 450    safe 4.7  timeout 900    timeout 900    safe 0.40 safe 5.3 
locks/test_locks_13_safe.c timeout 910    safe 1.4  safe 100    safe 450    safe 5.3  timeout 900    timeout 900    safe 0.43 safe 8.3 
locks/test_locks_14_safe.c timeout 910    safe 1.4  safe 100    safe 450    safe 6.0  timeout 900    timeout 900    safe 0.40 safe 8.1 
locks/test_locks_15_safe.c timeout 910    safe 1.4  safe 100    safe 450    safe 6.6  timeout 900    timeout 900    safe 0.40 safe 8.4 
locks/test_locks_5_safe.c safe 11    safe 1.2  safe 1.3  safe 450    safe 1.4  safe 0.18 timeout 900    safe 0.40 safe 3.1 
locks/test_locks_6_safe.c safe 21    safe 1.3  safe 1.6  safe 450    safe 1.8  safe 1.2  timeout 900    safe 0.43 safe 3.4 
locks/test_locks_7_safe.c safe 67    safe 1.3  safe 1.9  safe 450    safe 2.2  safe 11    timeout 900    safe 0.40 safe 3.7 
locks/test_locks_8_safe.c safe 140    safe 1.3  safe 2.3  safe 450    safe 2.6  safe 42    timeout 900    safe 0.40 safe 4.2 
locks/test_locks_9_safe.c safe 330    safe 1.3  safe 3.5  safe 450    safe 3.0  safe 140    timeout 900    safe 0.39 safe 4.7 
total files 48 12000 48 260 48 1300 48 10000 48 70 48 5200 48 27000 48 170 48 750
correct results 33 2500 48 260 48 1300 47 10000 48 70 27 650 18 34 48 170 39 540
false negatives 0 0 0 0 0 0 1 1.6 0 0 0 0 0 0 0 0 0 0
false positives 0 0 0 0 0 0 0 0 0 0 16 58 0 0 0 0 0 0
false properties 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (48 files, max score: 78) 52 78 78 69 78 -28 28 78 63