Tool CBMC 4.5 CPAchecker 1.2.11-svcomp14b CPAlien ESBMC 1.22.1 LLBMC Predator 2013-10-30 Symbiotic UltimateAutomizer UltimateKojak
Limits timelimit: 900 s, memlimit: 15360 MB, CPU core limit: 8
OS 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-18 23:43 13-11-18 14:59 13-11-19 00:04 13-11-18 23:26 13-11-21 13:28 13-11-19 22:09 13-11-24 23:10 13-11-19 23:49 13-11-21 12:52
Options --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
-witness ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt		 --propertyfile ${sourcefile_path}/ALL.prp
--trace ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
-m32		 ${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/ 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)
heap-manipulation/bubble_sort_linux_false.i false(label) 2.1  160   false(label) 53    610   unknown 900    470   unknown 900    11000   false(label) 0.24 2.0 false(label) 0.10 5.0 timeout 900    59   unknown 2.3  110   unknown 2.3  110  
heap-manipulation/dll_of_dll_false.i unknown 850    6600   error (recursion) 2.2  140   unknown 1.9  110   unknown 900    6000   false(label) 3.5  75   false(label) 0.12 5.0 timeout 900    780   unknown 2.2  110   unknown 2.3  110  
heap-manipulation/merge_sort_false.i false(label) 0.43 25   false(label) 2.2  130   unknown 900    470   unknown 900    520   false(label) 0.67 21   false(label) 0.10 4.0 timeout 900    63   unknown 2.2  110   unknown 2.2  110  
heap-manipulation/sll_to_dll_rev_false.i false(label) 0.35 23   timeout 900    8000   timeout 900    470   false(label) 900    480   false(label) 1.0  14   false(label) 0.11 4.0 timeout 900    270   unknown 2.1  110   unknown 2.3  110  
heap-manipulation/bubble_sort_linux_true.i true 850    4200   exception 280    870   unknown 900    470   unknown 900    10000   timeout 920    11000   true 0.15 5.0 timeout 900    58   unknown 2.2  110   unknown 2.3  110  
heap-manipulation/dll_of_dll_true.i unknown 850    6600   error (recursion) 2.2  140   unknown 1.9  110   unknown 900    6100   timeout 920    7800   true 0.15 5.0 timeout 900    770   unknown 2.2  110   unknown 2.2  110  
heap-manipulation/merge_sort_true.i true 850    4700   timeout 900    250   unknown 900    460   unknown 900    480   unknown 310    15000   true 0.34 7.0 timeout 900    2400   unknown 2.1  110   unknown 2.2  110  
heap-manipulation/sll_to_dll_rev_true.i true 850    3900   timeout 900    620   unknown 900    470   unknown 900    210   timeout 920    2000   true 0.17 5.0 timeout 900    280   unknown 2.1  110   unknown 2.3  110  
list-properties/alternating_list_false.i false(label) 0.29 20   false(label) 2.2  140   unknown 900    460   false(label) 0.71 39   false(label) 0.23 2.0 false(label) 0.12 4.0 timeout 900    60   unknown 2.1  110   unknown 2.3  110  
list-properties/list_false.i false(label) 0.29 20   false(label) 4.9  190   unknown 900    450   false(label) 5.4  110   false(label) 0.17 12   false(label) 0.16 4.0 timeout 900    170   unknown 2.1  100   unknown 2.3  110  
list-properties/list_flag_false.i false(label) 0.39 27   false(label) 2.6  170   unknown 900    470   false(label) 0.80 41   false(label) 0.12 4.0 false(label) 0.13 4.0 timeout 900    59   unknown 2.1  110   unknown 2.2  110  
list-properties/list_search_false.i false(label) 0.44 20   false(label) 3.2  190   unknown 2.0  110   false(label) 0.38 19   false(label) 0.13 2.0 false(label) 0.10 4.0 false(label) 0.36 2.0 unknown 2.2  110   unknown 2.3  110  
list-properties/simple_false.i false(label) 0.26 20   false(label) 2.5  150   unknown 900    460   false(label) 0.55 34   false(label) 0.10 2.0 false(label) 0.14 4.0 timeout 900    60   unknown 2.1  110   unknown 2.3  110  
list-properties/splice_false.i false(label) 0.34 23   false(label) 2.1  130   unknown 900    470   false(label) 1.4  47   false(label) 0.12 3.0 false(label) 0.17 4.0 timeout 900    560   unknown 2.7  110   unknown 2.2  110  
list-properties/alternating_list_true.i true 26    190   timeout 900    240   timeout 900    470   true 0.68 36   true 3.0  93   timeout 900    320   timeout 900    60   unknown 2.2  110   unknown 2.2  110  
list-properties/list_flag_true.i true 30    290   timeout 900    230   unknown 900    470   true 1.0  40   true 5.5  110   true 0.23 4.0 timeout 900    60   unknown 2.1  110   unknown 2.3  110  
list-properties/list_search_true.i true 1.3  22   true 4.6  190   unknown 2.2  140   true 0.48 25   true 0.16 2.0 true 0.19 4.0 true 0.38 2.0 unknown 2.2  110   unknown 2.2  110  
list-properties/list_true.i true 850    6400   timeout 900    240   timeout 900    450   true 20    110   true 38    400   true 0.21 4.0 timeout 900    170   unknown 2.2  110   unknown 2.2  110  
list-properties/simple_built_from_end_true.i true 14    100   timeout 900    280   unknown 900    470   true 0.95 33   true 2.9  87   true 0.18 3.0 timeout 900    1000   unknown 2.2  110   unknown 2.3  110  
list-properties/simple_true.i true 37    220   timeout 900    210   unknown 900    460   false(label) 0.55 34   true 3.0  91   true 0.16 4.0 timeout 900    1000   unknown 2.2  110   unknown 2.2  110  
list-properties/splice_true.i true 270    1700   timeout 900    250   timeout 900    470   true 3.3  50   true 43    750   timeout 900    260   timeout 900    560   unknown 2.2  110   unknown 2.5  110  
ldv-regression/1_3.c_false.i false(label) 0.27 17   false(label) 1.9  130   unknown 1.6  99   false(label) 0.27 12   false(label) 0.14 2.0 false(label) 0.11 3.0 false(label) 0.37 2.0 unknown 2.2  110   unknown 2.2  110  
ldv-regression/alt_test.c_false.i false(label) 0.27 22   false(label) 2.8  180   false(label) 2.1  120   false(label) 0.41 21   false(label) 0.12 2.0 false(label) 0.10 4.0 false(label) 0.23 2.0 unknown 2.2  110   unknown 2.3  110  
ldv-regression/callfpointer.c_false.i false(label) 0.17 16   false(label) 1.8  120   unknown 1.6  97   unknown 0.17 3.0 false(label) 0.13 2.0 false(label) 0.08 3.0 false(label) 0.19 2.0 unknown 2.1  100   unknown 2.2  110  
ldv-regression/fo_test.c_false.i false(label) 0.32 20   false(label) 2.1  130   false(label) 1.9  110   false(label) 0.37 18   false(label) 0.11 2.0 false(label) 0.09 3.0 false(label) 0.22 2.0 unknown 2.2  110   unknown 2.3  110  
ldv-regression/mutex_lock_int.c_false.i false(label) 0.17 16   false(label) 1.8  120   false(label) 1.6  98   false(label) 0.26 11   false(label) 0.10 2.0 false(label) 0.12 3.0 false(label) 0.19 2.0 false(label) 3.5  210   false(label) 3.4  210  
ldv-regression/mutex_lock_struct.c_false.i false(label) 0.20 16   false(label) 1.8  120   false(label) 1.6  97   false(label) 0.27 12   false(label) 0.10 2.0 false(label) 0.09 3.0 false(label) 0.19 2.0 false(label) 3.9  210   false(label) 3.5  210  
ldv-regression/recursive_list.c_false.i false(label) 0.25 17   false(label) 1.8  120   unknown 1.6  100   false(label) 0.32 12   false(label) 0.10 2.0 false(label) 0.13 3.0 false(label) 0.19 2.0 unknown 2.7  110   unknown 2.2  110  
ldv-regression/rule57_ebda_blast.c_false.i false(label) 0.19 16   false(label) 1.9  130   false(label) 1.7  110   false(label) 0.29 13   false(label) 0.14 2.0 false(label) 0.18 4.0 false(label) 0.20 3.0 unknown 2.4  100   unknown 2.1  110  
ldv-regression/rule60_list2.c_false_1.i false(label) 0.19 19   false(label) 2.1  130   false(label) 1.9  110   false(label) 0.35 18   false(label) 0.12 2.0 false(label) 0.10 4.0 false(label) 0.23 3.0 unknown 2.6  110   unknown 2.2  110  
ldv-regression/stateful_check_false.i false(label) 0.28 16   false(label) 2.0  130   false(label) 1.8  110   false(label) 0.62 18   false(label) 0.23 4.0 false(label) 0.09 4.0 timeout 900    380   unknown 2.7  110   unknown 2.2  110  
ldv-regression/test_while_int.c_false.i false(label) 0.25 16   false(label) 1.8  120   false(label) 1.6  98   false(label) 0.27 11   false(label) 0.09 2.0 false(label) 0.09 3.0 false(label) 0.36 2.0 unknown 2.4  110   unknown 2.8  110  
ldv-regression/test_while_int.c_false_1.i false(label) 0.25 16   false(label) 1.8  120   false(label) 1.6  97   false(label) 0.30 11   false(label) 0.10 2.0 false(label) 0.09 3.0 false(label) 0.19 2.0 unknown 2.4  110   unknown 2.2  110  
ldv-regression/alias_of_return.c_true.i true 0.58 16   true 2.0  130   true 1.6  96   true 0.21 11   true 0.10 2.0 true 0.12 3.0 true 0.20 2.0 unknown 2.6  110   unknown 2.2  110  
ldv-regression/alias_of_return.c_true_1.i true 0.52 16   true 1.9  130   true 1.6  96   true 0.22 12   true 0.09 2.0 true 0.12 3.0 true 0.20 2.0 true 3.5  200   true 3.0  200  
ldv-regression/alias_of_return_2.c_true.i true 0.53 16   true 2.0  130   true 1.6  98   true 0.24 11   true 0.12 2.0 true 0.11 3.0 true 0.19 2.0 unknown 2.7  100   unknown 2.2  110  
ldv-regression/alias_of_return_2.c_true_1.i true 0.52 16   true 1.9  130   true 1.5  96   true 0.22 11   true 0.11 2.0 true 0.11 3.0 true 0.19 2.0 true 3.7  200   true 3.1  200  
ldv-regression/ex3_forlist.c_true.i true 0.57 16   true 4.8  190   false(label) 1.8  110   true 0.32 13   true 0.14 2.0 true 0.18 4.0 true 0.21 2.0 unknown 2.8  110   unknown 2.1  110  
ldv-regression/just_assert.c_true.i true 0.59 16   true 1.6  93   true 1.5  95   true 0.21 11   true 0.09 2.0 true 0.11 3.0 true 0.19 2.0 true 3.1  120   true 2.4  130  
ldv-regression/mutex_lock_int.c_true_1.i true 0.57 16   true 2.1  130   true 1.6  96   true 0.22 11   true 0.11 2.0 true 0.12 3.0 true 0.19 2.0 true 4.6  240   true 4.5  240  
ldv-regression/mutex_lock_struct.c_true_1.i true 0.55 16   true 2.1  140   true 1.6  98   true 0.27 12   true 0.10 2.0 true 0.12 3.0 true 0.19 2.0 true 4.8  240   true 4.8  240  
ldv-regression/nested_structure.c_true.i true 0.53 16   true 1.6  94   true 1.6  97   true 0.23 12   true 0.10 2.0 true 0.12 3.0 true 0.19 2.0 unknown 2.7  100   unknown 3.2  110  
ldv-regression/nested_structure_noptr.c_true.i true 0.56 16   true 1.6  94   true 1.6  97   true 0.22 11   true 0.13 2.0 true 0.12 3.0 true 0.19 2.0 unknown 2.5  110   unknown 2.2  110  
ldv-regression/nested_structure_noptr_true.i true 0.52 16   true 1.6  95   true 1.6  97   true 0.22 12   true 0.09 2.0 true 0.12 3.0 true 0.20 2.0 unknown 3.0  110   unknown 2.2  110  
ldv-regression/nested_structure_ptr.c_true.i true 0.53 16   true 1.6  94   true 1.6  97   true 0.25 12   true 0.11 2.0 true 0.12 3.0 true 0.17 2.0 unknown 2.8  100   unknown 2.1  110  
ldv-regression/nested_structure_ptr_true.i true 0.54 16   true 1.6  94   true 1.6  97   true 0.24 12   true 0.10 2.0 true 0.14 3.0 true 0.19 2.0 unknown 2.7  100   unknown 2.2  110  
ldv-regression/nested_structure_true.i true 0.57 16   true 1.6  94   true 1.6  98   true 0.23 12   true 0.10 2.0 true 0.11 3.0 true 0.19 2.0 unknown 2.6  110   unknown 2.2  110  
ldv-regression/oomInt.c_true.i true 0.55 16   true 1.6  93   true 1.6  97   true 0.22 11   true 0.10 2.0 true 0.11 3.0 true 0.19 2.0 true 3.7  160   true 2.9  190  
ldv-regression/oomInt.c_true_1.i true 0.53 16   true 1.6  95   true 1.6  98   true 0.20 11   true 0.10 2.0 true 0.12 3.0 true 0.20 2.0 unknown 2.8  110   unknown 2.2  110  
ldv-regression/rule57_ebda_blast.c_true_1.i true 0.57 16   true 1.6  99   true 1.8  110   true 0.30 13   true 0.12 2.0 true 0.24 4.0 true 0.20 3.0 unknown 2.8  110   unknown 2.1  110  
ldv-regression/rule60_list.c_true.i true 1.1  20   true 2.7  180   true 1.9  110   true 0.34 17   true 0.10 2.0 true 0.23 4.0 true 0.21 2.0 unknown 2.4  110   unknown 2.2  110  
ldv-regression/rule60_list2.c_true.i true 0.62 19   true 1.8  98   true 2.1  120   true 0.36 17   true 0.12 2.0 true 0.16 3.0 true 0.22 2.0 unknown 2.4  110   unknown 2.2  110  
ldv-regression/sizeofparameters_test.c_true.i true 0.59 18   true 1.7  96   true 1.7  98   false(label) 0.32 16   true 0.10 2.0 true 0.12 3.0 true 0.21 2.0 unknown 2.6  110   unknown 2.3  110  
ldv-regression/structure_assignment.c_true.i true 0.55 16   true 2.0  130   true 1.6  96   true 0.22 11   true 0.13 2.0 true 0.13 3.0 true 0.20 2.0 unknown 2.5  110   unknown 2.5  110  
ldv-regression/test_address.c_true.i true 0.58 19   true 2.2  140   true 1.8  110   true 0.35 17   true 0.11 2.0 true 0.12 3.0 true 0.20 2.0 unknown 2.3  110   unknown 2.2  110  
ldv-regression/test_cut_trace.c_true.i true 0.54 16   true 1.6  94   true 1.5  96   true 0.21 11   true 0.09 2.0 true 0.11 3.0 true 0.18 2.0 unknown 2.2  110   unknown 2.2  110  
ldv-regression/test_malloc-1_true.i true 1.1  20   true 2.3  140   true 2.0  110   true 0.34 17   true 0.10 2.0 true 0.16 3.0 true 0.20 2.0 unknown 2.2  110   unknown 2.2  110  
ldv-regression/test_malloc-2_true.i true 0.58 19   true 2.2  140   true 1.8  110   true 0.32 17   true 0.10 2.0 true 0.14 3.0 true 0.21 2.0 unknown 2.2  110   unknown 2.2  110  
ldv-regression/test_overflow.c_true.i true 0.66 20   true 1.8  100   true 1.9  110   false(label) 0.38 21   true 0.09 2.0 true 0.24 4.0 true 0.23 2.0 unknown 2.2  110   unknown 2.4  110  
ldv-regression/test_union.c_true.i true 0.51 16   true 1.6  93   true 1.6  97   true 0.27 12   true 0.11 2.0 true 0.12 3.0 true 0.19 2.0 unknown 2.2  110   unknown 2.2  110  
ldv-regression/test_union.c_true_1.i true 0.55 16   false(label) 1.8  110   true 1.6  97   true 0.27 11   true 0.10 2.0 true 0.11 3.0 true 0.19 2.0 unknown 2.1  110   unknown 2.1  110  
ldv-regression/test_union_cast-1_true.i true 0.53 16   true 1.6  95   true 1.6  97   unknown 0.09 2.0 true 0.10 2.0 true 0.14 3.0 true 0.20 2.0 unknown 2.1  110   unknown 2.2  110  
ldv-regression/test_union_cast-2_true.i true 0.57 16   true 2.0  130   true 1.6  97   unknown 0.10 2.0 true 0.10 2.0 true 0.12 3.0 true 0.20 2.0 unknown 2.1  100   unknown 2.2  110  
ldv-regression/test_union_cast.c_true.i true 0.52 16   true 2.0  130   true 1.6  97   unknown 0.10 2.0 true 0.09 2.0 true 0.11 3.0 true 0.18 2.0 unknown 2.1  100   unknown 2.1  110  
ldv-regression/test_union_cast.c_true_1.i true 0.54 16   true 1.6  94   true 1.6  97   unknown 0.09 2.0 true 0.10 2.0 true 0.10 3.0 true 0.19 2.0 unknown 2.1  100   unknown 2.2  110  
ldv-regression/volatile_alias.c_true.i true 0.55 16   true 1.9  130   true 1.5  96   true 0.22 11   true 0.09 2.0 true 0.21 3.0 true 0.19 2.0 true 3.7  210   true 3.8  200  
ldv-regression/volatile_alias.c_true_1.i true 0.54 16   true 1.9  130   true 1.6  96   true 0.22 11   true 0.09 2.0 true 0.11 3.0 true 0.19 2.0 true 3.7  200   true 3.5  200  
ddv-machzwd/ddv_machzwd_all_false.i false(label) 1.1  35   false(label) 3.7  210   unknown 2.8  140   false(label) 0.90 57   false(label) 7.1  350   false(label) 0.18 10.0 false(label) 0.47 19   unknown 2.4  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_inw_false.i false(label) 1.1  34   false(label) 3.7  210   unknown 2.8  140   false(label) 0.89 56   false(label) 5.5  330   false(label) 0.17 10.0 false(label) 0.44 17   unknown 2.4  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_outb_false.i false(label) 1.0  34   false(label) 3.7  210   unknown 2.8  140   false(label) 0.90 56   false(label) 6.4  340   false(label) 0.20 10.0 false(label) 0.43 18   unknown 2.3  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_inb_p_true.i true 850    870   true 2.9  140   unknown 2.7  140   true 2.7  120   timeout 900    230   unknown 0.47 12   true 0.33 8.0 unknown 2.3  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_inb_true.i true 850    870   true 2.9  140   unknown 2.8  140   true 2.7  120   timeout 900    230   unknown 0.48 12   true 0.33 8.0 unknown 2.4  120   unknown 3.0  120  
ddv-machzwd/ddv_machzwd_inl_p_true.i true 850    870   true 2.9  140   unknown 2.7  140   true 2.7  120   timeout 900    230   unknown 0.46 12   true 0.33 8.0 unknown 2.4  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_inl_true.i true 850    870   true 2.9  140   unknown 2.7  140   true 2.7  120   timeout 900    230   unknown 0.47 12   true 0.34 8.0 unknown 2.4  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_inw_p_true.i true 850    870   true 2.9  140   unknown 2.8  140   true 2.7  120   timeout 900    230   unknown 0.47 12   true 0.33 8.0 unknown 2.4  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_outb_p_true.i true 850    870   true 2.9  140   unknown 2.8  140   true 2.7  120   timeout 900    230   unknown 0.46 12   true 0.33 8.0 unknown 2.4  120   unknown 2.6  120  
ddv-machzwd/ddv_machzwd_outl_p_true.i true 850    870   true 2.9  140   unknown 2.8  140   true 2.7  120   timeout 900    230   unknown 0.47 12   true 0.33 8.0 unknown 2.4  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_outl_true.i true 850    870   true 3.0  140   unknown 2.8  140   true 2.7  120   timeout 900    230   unknown 0.46 12   true 0.33 8.0 unknown 2.4  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_outw_p_true.i true 850    870   true 2.9  140   unknown 2.8  140   true 2.7  120   timeout 900    230   unknown 0.49 12   true 0.33 8.0 unknown 2.4  120   unknown 2.5  120  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true.i true 850    870   true 2.9  140   unknown 2.8  140   true 2.7  120   timeout 900    230   unknown 0.51 12   true 0.34 8.0 unknown 2.4  120   unknown 2.5  120  
../../sv-benchmarks/c/ 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 80 14000 45000 80 8600 21000 80 15000 15000 80 7200 37000 80 12000 41000 80 1800 950 80 18000 9100 80 200 9400 80 200 9900
correct results 78 12000 32000 67 210 9200 42 70 4200 65 970 2900 66 130 2800 68 9.5 260 60 15 230 10 38 2000 10 35 2000
false negatives 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
false positives 0 0 0 1 1.8 110 1 1.8 110 3 1.3 71 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (80 files, max score: 135) 132 107 71 97 107 111 105 18 18