Tool CBMC
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-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.HeapReach
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.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 witness invalid (assertion) 2.4  2.5  180 wit assertion 7.8 4.2 290 unknown 22 14   430
heap-manipulation/dll_of_dll_false-unreach-call.i witness invalid (assertion) .58 .59 38 wit assertion 8.2 4.7 300 true 16 9.8 360
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 1.3  1.3  76 wit assertion 7.2 4.1 260 false(reach) 19 10   390
heap-manipulation/sll_to_dll_rev_false-unreach-call.i witness invalid (assertion) .48 .50 36 wit assertion 6.1 3.4 270 error 30 21   680
heap-manipulation/bubble_sort_linux_true-unreach-call.i true 850    850    4600 wit - -
heap-manipulation/dancing_true-unreach-call.i true 850    850    580 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i true 850    850    2400 wit - -
heap-manipulation/merge_sort_true-unreach-call.i true 480    480    14000 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i true 850    850    4200 wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) .25 .26 28 wit assertion 5.6 3.2 250 false(reach) 13 7.7 330
list-properties/list_false-unreach-call.i false(reach) .32 .33 29 wit assertion 6.5 3.6 250 false(reach) 16 8.8 350
list-properties/list_flag_false-unreach-call.i false(reach) .31 .32 27 wit assertion 6.2 3.7 250 false(reach) 14 8.4 330
list-properties/list_search_false-unreach-call.i witness invalid (assertion) .51 .53 28 wit assertion 6.5 3.6 250 error 49 38   640
list-properties/simple_false-unreach-call.i false(reach) .25 .26 28 wit assertion 5.2 3.0 240 false(reach) 13 7.6 340
list-properties/splice_false-unreach-call.i false(reach) .21 .22 28 wit assertion 6.9 3.9 260 false(reach) 15 8.4 340
list-properties/alternating_list_true-unreach-call.i true 850    850    4300 wit - -
list-properties/list_flag_true-unreach-call.i true 850    850    6800 wit - -
list-properties/list_search_true-unreach-call.i true 3.9  4.0  60 wit - -
list-properties/list_true-unreach-call.i true 850    850    6900 wit - -
list-properties/simple_built_from_end_true-unreach-call.i true 850    850    2400 wit - -
list-properties/simple_true-unreach-call.i true 850    850    5100 wit - -
list-properties/splice_true-unreach-call.i true 850    850    1900 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) .25 .26 25 wit assertion 4.6 2.6 220 false(reach) 12 6.6 330
ldv-regression/alt_test.c_false-unreach-call.i false(reach) .25 .26 29 wit true 7.0 3.8 260 false(reach) 14 8.0 340
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) .14 .15 24 wit false(reach) 4.1 2.4 220 false(reach) 13 9.1 330
ldv-regression/fo_test.c_false-unreach-call.i false(reach) .28 .29 28 wit false(reach) 7.8 4.3 360 unknown 11 7.1 310
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) .15 .16 24 wit true 4.5 2.7 210 false(reach) 12 6.5 330
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) .14 .15 24 wit true 4.1 2.4 210 false(reach) 12 6.6 330
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) .22 .23 25 wit exception 4.8 2.8 220 false(reach) 12 7.4 330
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) .17 .18 25 wit assertion 4.6 2.6 220 false(reach) 13 7.2 330
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(reach) .18 .19 26 wit false(reach) 8.8 4.8 350 false(reach) 33 21   670
ldv-regression/stateful_check_false-unreach-call.i false(reach) .36 .37 26 wit false(reach) 7.7 4.3 370 false(reach) 19 10   370
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) .25 .26 24 wit false(reach) 5.1 2.9 230 false(reach) 12 6.9 340
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) .25 .27 24 wit false(reach) 4.7 2.7 230 false(reach) 12 6.9 360
ldv-regression/alias_of_return.c_true-unreach-call.i true 1.1  1.1  24 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true .88 .91 24 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true .88 .91 24 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 1.1  1.1  24 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i true 1.1  1.1  24 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true 1.0  1.1  24 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 1.0  1.1  24 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 1.1  1.1  24 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true 1.0  1.1  24 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true .83 .87 24 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true 1.1  1.1  24 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 1.1  1.2  24 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true 1.1  1.2  24 wit - -
ldv-regression/nested_structure_true-unreach-call.i true 1.0  1.1  24 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true .99 1.0  24 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true .83 .85 24 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 1.1  1.1  25 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 1.7  1.8  28 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true 1.2  1.3  26 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 1.1  1.2  26 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true .88 .91 24 wit - -
ldv-regression/test_address.c_true-unreach-call.i true 1.2  1.2  26 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true 1.1  1.1  24 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true 2.0  2.1  28 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true 1.2  1.2  26 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true 1.3  1.3  28 wit - -
ldv-regression/test_union.c_true-unreach-call.i true .94 .97 24 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true 1.1  1.2  24 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i true 1.1  1.1  24 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i true 1.1  1.2  24 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i true 1.1  1.1  24 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 1.0  1.1  24 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true .84 .87 24 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 1.1  1.2  24 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i witness unconfirmed 39    39    600 wit true 19   9.8 590 timeout 90 74   1000
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i witness unconfirmed 34    34    580 wit true 18   9.6 580 timeout 90 74   1000
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i witness unconfirmed 37    37    590 wit true 18   9.8 580 timeout 90 73   1000
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i true 850    850    380 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i true 850    850    390 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i true 850    850    390 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i true 850    850    390 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i true 850    850    360 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i true 850    850    390 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i true 850    850    390 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i true 850    850    390 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i true 850    850    390 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i true 850    850    380 wit - -
../../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 18000   18000   60000 81 190   100   7500   81 650   460   12000  
    correct results 74 18000   18000   58000 9 110   60   4600   17 260   150   6400  
        correct true 56 18000   18000   58000 3 0   0   0   0 0   0   0  
        correct false 18 5.3 5.5 520 6 110   60   4600   17 260   150   6400  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 137) 130
Run set sv-comp16.HeapReach