Tool DepthK ESBMC+DepthK version 2.1
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 CET ]]
Run set sv-comp16.HeapReach
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
heap-manipulation/bubble_sort_linux_false-unreach-call.i 6.0   3.8  190 16   8.8 490 13   8.7 330
heap-manipulation/dll_of_dll_false-unreach-call.i 79     79    15000
heap-manipulation/merge_sort_false-unreach-call.i 7.6   5.5  190 9.8 5.7 410 13   8.6 320
heap-manipulation/sll_to_dll_rev_false-unreach-call.i 5.4   3.4  180 12   6.5 430 14   8.8 350
heap-manipulation/bubble_sort_linux_true-unreach-call.i 6.0   4.0  190
heap-manipulation/dancing_true-unreach-call.i .54  .57 29
heap-manipulation/dll_of_dll_true-unreach-call.i 79     79    15000
heap-manipulation/merge_sort_true-unreach-call.i 890     900    4100
heap-manipulation/sll_to_dll_rev_true-unreach-call.i 890     900    280
list-properties/alternating_list_false-unreach-call.i 5.9   4.0  180 9.3 5.1 390 12   6.7 340
list-properties/list_false-unreach-call.i 5.9   3.9  180 91   83   660 11   6.3 330
list-properties/list_flag_false-unreach-call.i 5.2   3.4  180 9.8 5.4 380 11   7.1 330
list-properties/list_search_false-unreach-call.i 7.0   5.2  180 9.0 5.0 390 12   6.9 320
list-properties/simple_false-unreach-call.i 5.5   3.5  180 8.3 4.6 370 13   7.1 330
list-properties/splice_false-unreach-call.i 6.0   4.0  180 11   6.0 420 10   6.0 330
list-properties/alternating_list_true-unreach-call.i 1.6   1.7  130
list-properties/list_flag_true-unreach-call.i 3.7   3.7  140
list-properties/list_search_true-unreach-call.i 1.8   1.9  38
list-properties/list_true-unreach-call.i 210     210    430
list-properties/simple_built_from_end_true-unreach-call.i 3.6   3.6  130
list-properties/simple_true-unreach-call.i 5.2   3.2  180
list-properties/splice_true-unreach-call.i 32     32    160
ldv-regression/1_3.c_false-unreach-call.i 3.1   1.7  170 5.2 3.0 240 11   6.6 320
ldv-regression/alt_test.c_false-unreach-call.i 6.6   4.7  180 9.9 5.7 390 10   6.8 320
ldv-regression/callfpointer.c_false-unreach-call.i .19  .21 12
ldv-regression/fo_test.c_false-unreach-call.i 5.6   3.8  180 5.5 3.1 250 9.8 6.3 320
ldv-regression/mutex_lock_int.c_false-unreach-call.i 2.9   1.5  160 4.8 2.9 240 9.9 6.3 330
ldv-regression/mutex_lock_struct.c_false-unreach-call.i 3.1   1.6  160 4.8 2.8 230 11   6.9 320
ldv-regression/recursive_list.c_false-unreach-call.i 3.4   1.8  170 91   81   3700 12   6.8 340
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i 3.3   1.7  160 5.3 3.0 220 11   6.5 330
ldv-regression/rule60_list2.c_false-unreach-call_1.i 5.6   3.7  170 5.9 3.3 240 12   8.0 340
ldv-regression/stateful_check_false-unreach-call.i 4.0   2.5  170 19   10   610 11   6.9 320
ldv-regression/test_while_int.c_false-unreach-call.i 3.2   1.8  160 5.9 3.3 330 10   6.0 320
ldv-regression/test_while_int.c_false-unreach-call_1.i 3.4   1.8  160 4.6 2.7 230 11   6.5 320
ldv-regression/alias_of_return.c_true-unreach-call.i .34  .36 21
ldv-regression/alias_of_return.c_true-unreach-call_1.i .35  .39 21
ldv-regression/alias_of_return_2.c_true-unreach-call.i .36  .39 21
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i .41  .44 21
ldv-regression/ex3_forlist.c_true-unreach-call.i .43  .46 22
ldv-regression/just_assert.c_true-unreach-call.i .39  .43 21
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i .41  .44 21
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i .35  .37 21
ldv-regression/nested_structure.c_true-unreach-call.i .35  .38 21
ldv-regression/nested_structure_noptr.c_true-unreach-call.i .39  .43 21
ldv-regression/nested_structure_noptr_true-unreach-call.i .36  .39 21
ldv-regression/nested_structure_ptr.c_true-unreach-call.i .35  .38 21
ldv-regression/nested_structure_ptr_true-unreach-call.i .34  .37 21
ldv-regression/nested_structure_true-unreach-call.i .38  .41 22
ldv-regression/oomInt.c_true-unreach-call.i .34  .37 21
ldv-regression/oomInt.c_true-unreach-call_1.i .33  .36 21
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i .51  .53 23
ldv-regression/rule60_list.c_true-unreach-call.i .64  .68 28
ldv-regression/rule60_list2.c_true-unreach-call.i .54  .57 30
ldv-regression/sizeofparameters_test.c_true-unreach-call.i 4.4   2.7  170
ldv-regression/structure_assignment.c_true-unreach-call.i .36  .39 21
ldv-regression/test_address.c_true-unreach-call.i .71  .75 28
ldv-regression/test_cut_trace.c_true-unreach-call.i .36  .39 21
ldv-regression/test_malloc-1_true-unreach-call.i .63  .66 28
ldv-regression/test_malloc-2_true-unreach-call.i .76  .80 29
ldv-regression/test_overflow.c_true-unreach-call.i 7.2   5.6  180
ldv-regression/test_union.c_true-unreach-call.i .45  .49 21
ldv-regression/test_union.c_true-unreach-call_1.i .49  .51 21
ldv-regression/test_union_cast-1_true-unreach-call.i .13  .14 11
ldv-regression/test_union_cast-2_true-unreach-call.i .098 .11 11
ldv-regression/test_union_cast.c_true-unreach-call.i .14  .16 11
ldv-regression/test_union_cast.c_true-unreach-call_1.i .10  .12 11
ldv-regression/volatile_alias.c_true-unreach-call.i .37  .39 21
ldv-regression/volatile_alias.c_true-unreach-call_1.i .35  .41 30
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i 900     900    750
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i 890     900    830
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i 890     900    820
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i 5.6   5.6  360
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i 5.6   5.6  360
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i 5.5   5.6  360
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i 5.6   5.6  360
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i 5.1   5.1  360
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i 5.9   5.9  360
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i 5.4   5.4  360
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i 5.4   5.4  360
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i 5.6   5.6  360
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i 5.7   5.7  360
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 81 5100 5000 46000 81 340   250   11000   81 230   140   6600  
    correct results 59 400 370 7900 15 140   78   5600   15 170   110   4900  
        correct true 44 320 320 5300 0 0   0   0   15 0   0   0  
        correct false 15 75 48 2600 15 140   78   5600   0 170   110   4900  
    incorrect results 4 23 15 720 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 4 23 15 720 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 137) 39
Run set sv-comp16.HeapReach