Tool BLAST 2.7.1 CBMC 4.5 CPAchecker 1.2.11-svcomp14b CPAlien ESBMC 1.22.1 FrankenBit LLBMC Predator 2013-10-30 Symbiotic UFO UltimateAutomizer UltimateKojak
Limits timelimit: 900 s, memlimit: 15360 MB, CPU core limit: 8
OS Linux 3.2.0-56-generic x86_64 Linux 3.2.0-57-generic x86_64 Linux 3.2.0-56-generic x86_64
System CPU: Intel Core i7-2600 CPU @ 3.40GHz with 8 cores, frequency: 3401 MHz; RAM: 32827640 kB
Date of execution 13-11-22 09:28 13-11-18 23:43 13-11-18 14:59 13-11-22 09:12 13-11-18 23:26 13-12-04 17:02 13-11-21 13:28 13-11-19 22:09 13-11-24 23:10 13-11-21 15:51 13-11-19 23:49 13-11-21 12:52
Options -alias empty
-enable-recursion
-noprofile
-cref
-sv-comp
-lattice
-include-lattice symb
-nosserr
-errorpathfile ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
-propertyfile ${sourcefile_path}/ALL.prp		 --propertyfile ${sourcefile_path}/ALL.prp
--32		 -sv-comp14
-heap 10000M
-spec ${sourcefile_path}/ALL.prp
-disable-java-assertions		 -c ${sourcefile_path}/ALL.prp --spec=${sourcefile_path}/ALL.prp
--cex=${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt		 -spec ${sourcefile_path}/ALL.prp
-witness ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt		 --propertyfile ${sourcefile_path}/ALL.prp
--trace ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
-m32		 --spec=${sourcefile_path}/ALL.prp
--cex=${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt		 ${sourcefile_path}/ALL.prp ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt ${sourcefile_path}/ALL.prp ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
../../sv-benchmarks/c/loops/ status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB)
array_false.i false(label) 0.92 13   false(label) 0.18 16   false(label) 2.2  140   false(label) 1.6  99   false(label) 0.28 12   false(label) 0.52 23   false(label) 0.21 2.0 false(label) 0.09 3.0 unknown 0.18 2.0 false(label) 0.52 64   unknown 2.2  110   unknown 2.2  110  
bubble_sort_false.i exception (gremlins) 0.11 12   false(label) 2.0  160   false(label) 8.4  490   unknown 1.9  110   false(label) 900    1500   false(label) 0.38 27   false(label) 0.16 3.0 unknown 0.11 5.0 timeout 900    60   false(label) 1.0  120   unknown 2.2  110   unknown 2.2  110  
count_up_down_false.i false(label) 0.10 10.0 false(label) 0.17 16   false(label) 1.8  120   false(label) 1.6  97   false(label) 0.30 12   false(label) 0.25 18   false(label) 0.09 2.0 false(label) 0.08 3.0 false(label) 0.57 2.0 false(label) 0.43 35   false(label) 2.5  140   false(label) 2.7  150  
eureka_01_false.i false(label) 5.6  29   false(label) 0.36 20   false(label) 51    1800   unknown 2.1  150   false(label) 900    560   false(label) 0.38 26   false(label) 0.29 19   unknown 490    89   unknown 0.30 4.0 false(label) 1.0  110   timeout 920    2300   unknown 200    1700  
for_bounded_loop1_false.i false(label) 1.6  14   false(label) 0.19 16   false(label) 1.8  120   false(label) 1.6  99   false(label) 0.36 13   false(label) 0.28 24   false(label) 0.09 2.0 false(label) 0.11 3.0 timeout 900    240   false(label) 0.67 99   false(label) 7.8  210   false(label) 3.5  210  
insertion_sort_false.i false(label) 7.5  15   false(label) 3.0  260   timeout 900    2200   unknown 1.6  99   false(label) 18    66   false(label) 0.43 25   false(label) 0.24 7.0 unknown 0.11 3.0 unknown 0.38 2.0 false(label) 1.1  110   unknown 2.2  110   unknown 2.2  110  
invert_string_false.i false(label) 1.8  17   false(label) 0.47 28   timeout 900    2200   unknown 1.7  110   false(label) 0.60 17   false(label) 0.38 25   false(label) 0.17 4.0 unknown 0.12 3.0 unknown 0.19 2.0 false(label) 0.86 120   unknown 2.2  110   unknown 2.2  110  
linear_search_false.i false(label) 0.13 11   false(label) 0.62 19   exception 2.6  150   false(label) 1.6  99   true 0.30 12   false(label) 1.1  24   false(label) 0.20 5.0 unknown 0.12 3.0 unknown 0.19 2.0 false(label) 0.59 80   unknown 2.2  110   unknown 2.3  120  
ludcmp_false.i false(label) 2.8  18   false(label) 0.65 36   false(label) 4.7  490   false(label) 1.8  120   false(label) 0.32 13   false(label) 0.25 17   false(label) 0.18 54   false(label) 0.11 4.0 false(label) 0.19 2.0 false(label) 0.42 33   unknown 2.2  110   unknown 2.2  110  
matrix_false.i exception (gremlins) 0.10 5.0 false(label) 0.20 18   false(label) 24    1700   unknown 900    690   false(label) 900    350   unknown 0.12 8.0 false(label) 0.11 2.0 unknown 0.11 3.0 unknown 0.23 2.0 unknown 0.12 8.0 unknown 2.1  110   unknown 2.2  110  
nec11_false.i false(label) 0.11 10.0 false(label) 0.17 16   false(label) 2.0  130   false(label) 1.7  100   false(label) 0.29 12   false(label) 0.25 23   false(label) 0.10 1.00 false(label) 0.10 3.0 unknown 0.20 2.0 false(label) 0.59 97   false(label) 2.9  200   false(label) 2.7  170  
nec20_false.i false(label) 0.38 14   false(label) 0.34 31   false(label) 1.8  120   false(label) 1.6  98   false(label) 0.31 12   false(label) 0.26 24   false(label) 0.09 2.0 unknown 0.10 3.0 unknown 0.20 2.0 false(label) 0.74 110   false(label) 4.2  230   false(label) 3.3  200  
s3_false.i false(label) 33    43   false(label) 40    1000   false(label) 3.1  160   unknown 2.0  110   false(label) 900    1700   false(label) 0.92 29   false(label) 130    2900   unknown 0.12 6.0 true 0.31 5.0 false(label) 4.1  180   unknown 2.3  120   unknown 2.4  130  
string_false.i false(label) 2.5  16   false(label) 0.29 17   false(label) 54    1700   false(label) 1.8  110   false(label) 0.72 18   false(label) 0.30 25   false(label) 0.15 3.0 unknown 0.10 4.0 unknown 0.39 5.0 unknown 0.10 4.0 false(label) 3.5  210   false(label) 9.6  250  
sum01_bug02_false.i false(label) 29    23   false(label) 0.34 16   false(label) 2.2  140   false(label) 1.7  99   false(label) 0.31 12   false(label) 0.42 25   false(label) 0.16 3.0 false(label) 0.10 3.0 timeout 900    160   false(label) 1.5  120   false(label) 15    240   false(label) 9.0  250  
sum01_bug02_sum01_bug02_base.case_false.i false(label) 16    19   false(label) 0.24 16   false(label) 2.0  130   false(label) 1.6  99   false(label) 0.32 12   false(label) 0.34 24   false(label) 0.14 2.0 false(label) 0.09 3.0 timeout 900    160   false(label) 1.0  110   false(label) 6.4  240   false(label) 5.3  240  
sum01_false.i false(label) 44    26   false(label) 0.34 16   false(label) 2.5  160   false(label) 1.6  100   false(label) 0.28 12   false(label) 0.61 27   false(label) 0.18 3.0 false(label) 0.10 3.0 timeout 900    160   false(label) 1.9  140   false(label) 24    250   false(label) 14    250  
sum03_false.i false(label) 8.7  20   false(label) 0.30 16   false(label) 1.9  120   false(label) 1.9  130   false(label) 0.29 12   false(label) 0.36 24   false(label) 0.16 2.0 false(label) 0.10 3.0 false(label) 0.34 2.0 false(label) 1.7  140   false(label) 28    250   false(label) 16    250  
sum04_false.i false(label) 2.1  15   false(label) 0.33 16   false(label) 1.8  120   false(label) 1.7  110   false(label) 0.30 12   false(label) 0.24 18   false(label) 0.10 2.0 false(label) 0.10 3.0 false(label) 0.20 2.0 false(label) 0.45 36   false(label) 6.2  240   false(label) 7.0  240  
sum_array_false.i false(label) 1.1  17   false(label) 0.18 17   false(label) 23    1700   unknown 1.6  99   false(label) 4.8  33   false(label) 0.32 25   false(label) 0.11 3.0 unknown 0.12 3.0 unknown 0.19 2.0 false(label) 1.00 120   unknown 2.2  110   unknown 2.3  110  
terminator_01_false.i false(label) 0.10 10.0 false(label) 0.18 16   false(label) 1.9  120   false(label) 1.6  97   false(label) 0.31 12   false(label) 0.27 23   false(label) 0.12 2.0 false(label) 0.10 3.0 false(label) 0.19 2.0 false(label) 0.62 78   false(label) 3.4  200   false(label) 2.8  190  
terminator_02_false.i false(label) 0.14 10.0 false(label) 0.17 16   false(label) 1.8  120   false(label) 1.6  99   false(label) 0.40 15   false(label) 0.27 24   false(label) 0.10 2.0 false(label) 0.09 3.0 unknown 0.19 2.0 false(label) 0.80 110   false(label) 2.4  140   false(label) 2.6  160  
terminator_03_false.i false(label) 0.26 13   false(label) 0.17 16   false(label) 2.1  140   false(label) 1.6  98   false(label) 0.33 14   false(label) 0.27 24   false(label) 0.10 2.0 false(label) 0.09 3.0 timeout 900    61   false(label) 0.77 100   false(label) 3.1  150   false(label) 2.7  170  
trex01_false.i false(label) 0.11 11   false(label) 0.17 16   false(label) 1.8  120   false(label) 1.6  98   false(label) 0.42 15   false(label) 0.30 24   false(label) 0.10 2.0 false(label) 0.12 3.0 unknown 0.61 2.0 false(label) 0.78 100   false(label) 2.5  150   false(label) 2.8  190  
trex02_false.i false(label) 0.14 10.0 false(label) 0.17 16   false(label) 1.8  120   false(label) 1.6  98   false(label) 0.35 13   false(label) 0.24 23   false(label) 0.11 2.0 false(label) 0.09 3.0 false(label) 0.20 2.0 false(label) 0.57 87   false(label) 2.4  140   false(label) 2.6  160  
trex03_false.i false(label) 0.12 11   false(label) 0.17 16   false(label) 2.1  140   false(label) 1.6  99   false(label) 0.39 16   false(label) 0.32 24   false(label) 0.11 2.0 false(label) 0.09 3.0 unknown 0.20 2.0 false(label) 0.77 110   false(label) 2.5  150   false(label) 3.0  200  
verisec_NetBSD-libc__loop_false.i false(label) 0.91 14   false(label) 0.26 16   false(label) 2.2  140   unknown 1.6  96   false(label) 0.30 12   false(label) 0.29 24   false(label) 0.12 2.0 false(label) 0.10 4.0 false(label) 0.19 2.0 false(label) 0.63 87   unknown 2.1  100   unknown 2.2  110  
verisec_OpenSER__cases1_stripFullBoth_arr_false.i false(label) 69    34   false(label) 0.34 19   false(label) 23    1100   unknown 1.6  99   false(label) 1.1  29   false(label) 0.38 26   false(label) 0.30 9.0 unknown 0.10 5.0 unknown 0.20 2.0 false(label) 0.64 87   unknown 2.2  110   unknown 2.3  110  
verisec_sendmail__tTflag_arr_one_loop_false.i true 0.74 13   false(label) 0.36 18   false(label) 3.2  180   unknown 1.8  130   false(label) 0.79 17   false(label) 31    64   false(label) 0.25 5.0 unknown 0.10 4.0 unknown 0.26 5.0 true 1.0  110   false(label) 3.0  200   true 11    250  
vogal_false.i timeout 920    210   false(label) 0.48 22   false(label) 55    1200   unknown 1.6  98   false(label) 1.4  33   false(label) 0.72 29   false(label) 0.13 3.0 false(label) 0.15 4.0 unknown 0.64 11   false(label) 4.2  190   unknown 2.2  100   unknown 2.5  110  
while_infinite_loop_4_false.i false(label) 0.12 10.0 false(label) 0.17 16   false(label) 1.8  120   false(label) 1.6  97   false(label) 0.28 12   false(label) 0.25 18   false(label) 0.10 2.0 false(label) 0.09 3.0 false(label) 0.20 2.0 false(label) 0.44 35   false(label) 2.4  140   false(label) 2.5  160  
array_true.i true 1.4  14   true 0.54 16   true 2.2  130   false(label) 1.6  98   true 0.27 12   true 0.32 26   true 0.11 2.0 false(label) 0.11 3.0 unknown 0.19 2.0 true 0.67 110   unknown 2.2  110   unknown 2.2  110  
bubble_sort_true.i true 0.10 10.0 true 34    180   true 22    1700   unknown 900    690   true 0.63 14   true 0.23 17   true 0.10 2.0 unknown 0.16 4.0 true 0.20 2.0 true 0.43 36   unknown 2.1  100   unknown 2.2  110  
count_up_down_true.i false(label) 0.10 10.0 true 0.62 18   timeout 900    4200   false(label) 1.6  98   true 0.28 12   true 0.22 17   true 0.26 3.0 false(label) 0.09 3.0 true 0.19 2.0 true 0.43 36   false(label) 2.6  140   false(label) 2.5  150  
eureka_01_true.i timeout 920    620   true 0.70 18   timeout 900    1000   true 22    460   true 0.24 12   timeout 920    1500   true 0.45 5.0 true 8.2  11   true 0.19 2.0 false(label) 95    280   timeout 920    1500   timeout 920    990  
eureka_05_true.i false(label) 13    20   true 0.54 16   true 14    230   true 5.7  450   true 0.31 12   timeout 920    1200   true 0.14 2.0 true 0.19 3.0 true 0.20 2.0 false(label) 2.8  170   timeout 910    550   timeout 920    440  
for_infinite_loop_1_true.i true 0.10 9.0 true 0.56 16   true 22    1700   timeout 900    660   true 0.24 11   true 0.40 17   true 0.19 2.0 true 0.18 3.0 timeout 900    2.0 true 0.43 36   true 2.7  140   true 3.7  170  
for_infinite_loop_2_true.i true 0.12 9.0 true 0.53 16   true 22    1700   unknown 900    630   true 0.23 12   true 0.25 17   true 0.19 2.0 true 0.17 3.0 timeout 900    2.0 true 0.43 37   true 2.4  140   true 2.7  170  
insertion_sort_true.i false(label) 6.6  15   true 850    3700   timeout 900    1700   unknown 1.6  98   unknown 900    110   timeout 920    170   timeout 920    180   unknown 0.11 3.0 unknown 0.36 2.0 false(label) 0.80 110   unknown 2.1  110   unknown 2.3  110  
invert_string_true.i false(label) 2.7  24   true 0.61 16   true 8.0  200   unknown 1.6  100   true 0.29 12   timeout 920    72   true 0.21 2.0 unknown 0.09 3.0 unknown 0.19 2.0 false(label) 0.64 82   unknown 2.1  110   unknown 2.2  110  
linear_sea.ch_true.i false(label) 0.10 11   true 0.78 21   exception 23    1100   false(label) 1.6  99   true 0.32 12   timeout 920    220   true 0.43 8.0 unknown 0.14 3.0 unknown 0.20 2.0 false(label) 0.63 83   unknown 2.2  110   unknown 2.3  120  
lu.cmp_true.i true 72    66   true 0.77 16   true 1.9  100   true 23    470   true 0.32 13   true 0.99 30   true 0.30 10.0 true 1.3  10.0 true 0.19 2.0 true 0.83 110   unknown 2.3  110   unknown 2.2  110  
matrix_true.i exception (gremlins) 0.09 5.0 true 0.55 16   true 4.9  170   false(label) 1.6  99   true 0.27 12   unknown 0.14 8.0 true 0.10 2.0 false(label) 0.10 4.0 unknown 0.19 2.0 unknown 0.11 8.0 unknown 2.1  110   unknown 2.3  110  
n.c11_true.i true 1.3  15   true 0.57 16   true 1.6  95   true 1.7  110   true 0.31 12   true 0.35 26   true 0.17 2.0 true 0.12 3.0 unknown 0.19 2.0 true 0.80 95   true 8.9  240   true 5.1  240  
n.c24_true.i timeout 920    220   true 1.1  18   timeout 900    3300   unknown 560    560   true 0.25 14   timeout 920    11000   timeout 920    13000   false(label) 0.10 4.0 timeout 900    1700   timeout 920    740   unknown 2.1  110   unknown 2.2  110  
n.c40_true.i false(label) 0.47 13   true 0.54 16   false(label) 8.4  210   false(label) 1.6  95   true 0.27 12   true 0.42 17   true 0.20 2.0 true 0.11 3.0 true 0.35 2.0 true 0.45 36   unknown 2.2  110   unknown 2.3  110  
nec40_true.i false(label) 0.51 13   true 0.54 16   false(label) 1.9  130   false(label) 1.6  99   true 0.22 11   true 0.23 18   true 0.10 2.0 true 0.12 3.0 true 0.19 2.0 true 0.41 38   unknown 2.2  110   unknown 2.2  110  
string_true.i true 1.3  14   true 0.81 23   true 53    1700   false(label) 1.8  110   true 0.35 13   true 0.25 18   true 0.27 8.0 unknown 1.2  6.0 unknown 0.38 5.0 unknown 0.10 4.0 false(label) 3.6  210   true 12    250  
sum01_true.i true 2.0  15   true 0.58 16   timeout 900    4100   false(label) 1.6  99   true 0.32 12   timeout 920    500   true 0.19 3.0 false(label) 0.09 3.0 true 0.19 2.0 true 1.1  120   timeout 920    340   timeout 920    300  
sum03_true.i true 0.31 13   true 0.55 16   true 53    1700   unknown 900    820   true 0.22 11   true 0.41 18   true 0.19 2.0 false(label) 0.09 3.0 timeout 900    2.0 true 0.44 38   timeout 920    370   timeout 920    370  
sum04_true.i true 1.6  16   true 0.53 16   true 1.6  95   true 1.7  100   true 0.21 11   true 0.22 18   true 0.09 2.0 true 0.12 3.0 true 0.37 2.0 true 0.42 36   true 11    240   true 9.1  240  
sum_array_true.i false(label) 1.1  16   true 39    590   timeout 900    2600   unknown 1.6  99   true 2.9  29   timeout 920    640   true 13    77   unknown 0.11 3.0 unknown 0.19 2.0 false(label) 1.00 120   unknown 2.6  110   unknown 2.2  110  
terminator_02_true.i true 1.3  16   true 0.90 24   true 2.0  130   false(label) 1.6  98   true 0.31 14   true 0.56 27   true 0.11 2.0 true 0.12 3.0 unknown 0.19 2.0 true 0.81 110   true 2.6  160   true 2.9  190  
terminator_03_true.i true 0.57 14   true 0.66 19   true 2.0  130   false(label) 1.6  98   true 0.37 14   true 0.34 26   true 0.32 5.0 true 0.12 3.0 timeout 900    72   true 0.61 81   true 3.2  160   true 3.0  190  
trex01_true.i true 1.4  14   true 1.1  25   true 53    1100   unknown 900    800   true 0.38 15   timeout 920    1300   true 0.36 6.0 false(label) 0.10 4.0 unknown 0.34 2.0 true 1.0  120   true 3.3  170   true 3.4  200  
trex02_true.i true 0.21 13   true 0.68 20   true 2.0  130   false(label) 1.6  98   true 0.34 13   true 0.42 17   true 0.24 4.0 true 0.14 3.0 true 0.19 2.0 true 0.41 34   true 3.0  150   true 2.8  170  
trex03_true.i false(label) 0.14 11   true 1.4  31   true 2.1  140   false(label) 1.6  99   true 0.34 15   true 0.42 27   true 0.40 8.0 true 0.12 3.0 unknown 0.19 2.0 true 0.89 110   false(label) 2.8  150   false(label) 3.0  200  
trex04_true.i true 0.65 16   true 0.66 19   true 2.2  140   false(label) 1.6  99   true 2.4  17   true 0.37 27   true 0.29 4.0 true 0.11 3.0 unknown 0.19 2.0 true 0.66 100   true 3.3  170   true 3.1  200  
veris.c_NetBSD-libc__loop_true.i true 0.37 13   true 0.62 17   true 2.1  130   unknown 1.6  95   true 0.33 12   true 0.21 17   true 0.10 2.0 true 0.13 3.0 true 0.20 2.0 true 0.42 35   unknown 2.9  110   unknown 2.2  110  
veris.c_OpenSER__cases1_stripFullBoth_arr_true.i true 0.14 10.0 true 73    100   true 22    1100   unknown 1.6  100   true 0.38 13   true 0.23 17   true 1.5  32   unknown 120    520   true 0.19 2.0 true 0.44 35   unknown 2.6  110   unknown 2.3  110  
veris.c_sendmail__tTflag_arr_one_loop_true.i true 0.43 13   true 0.63 16   true 23    1100   unknown 1.6  96   true 0.31 12   true 0.22 17   true 0.17 3.0 unknown 0.11 4.0 true 0.20 2.0 true 0.43 36   false(label) 2.7  170   true 4.2  230  
vogal_true.i timeout 920    150   true 0.92 23   timeout 900    1800   unknown 1.6  97   true 0.34 14   timeout 920    96   true 0.18 3.0 unknown 8.8  15   unknown 0.20 2.0 unknown 0.10 4.0 unknown 2.5  100   unknown 2.2  110  
while_infinite_loop_1_true.i true 0.10 9.0 true 0.52 16   true 1.6  94   true 1.5  98   true 0.20 11   true 0.42 17   true 0.18 2.0 true 0.16 3.0 timeout 900    2.0 true 0.42 35   true 3.0  140   true 2.7  170  
while_infinite_loop_2_true.i true 0.12 9.0 true 0.53 16   true 1.6  94   true 1.6  96   true 0.22 11   true 0.22 17   true 0.18 2.0 true 0.19 3.0 timeout 900    2.0 true 0.42 36   true 2.4  140   true 2.7  160  
while_infinite_loop_3_true.i true 0.11 9.0 true 0.56 16   true 1.6  94   true 1.5  97   true 0.22 11   true 0.21 17   true 0.20 2.0 true 0.16 3.0 timeout 900    2.0 true 0.43 35   true 2.5  140   true 3.3  160  
../../sv-benchmarks/c/loops/ status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB)
total files 65 4000 2100 65 1100 7100 65 8700 51000 65 6100 12000 65 4500 5100 65 9300 18000 65 2000 17000 65 630 840 65 13000 2800 65 1100 6000 65 4800 14000 65 4100 13000
correct results 48 320 770 65 1100 7100 52 600 27000 28 91 3900 63 3600 5000 53 50 1200 63 160 3300 37 14 130 21 4.9 42 52 44 4300 30 170 5500 31 150 6200
false negatives 1 0.74 13 0 0 0 0 0 0 0 0 0 1 0.30 12 0 0 0 0 0 0 0 0 0 1 0.31 5.0 1 1.0 110 0 0 0 1 11 250
false positives 9 24 130 0 0 0 2 10 340 13 21 1300 0 0 0 0 0 0 0 0 0 7 0.68 24 0 0 0 6 100 840 4 12 670 2 5.5 350
score (65 files, max score: 99) 25 99 68 -16 88 76 95 27 26 44 26 29