Tool SMACK+Corral 1.5.2
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-23-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-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]]
Run set sv-comp16.HeapReach
Options -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.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 unconfirmed 3.9 3.9 91 wit true 15   8.2 490 unknown 21   11   430
heap-manipulation/dll_of_dll_false-unreach-call.i false(reach) 3.9 3.9 91 wit false(reach) 9.8 5.5 390 true 14   7.7 330
heap-manipulation/merge_sort_false-unreach-call.i witness unconfirmed 3.0 3.0 90 wit true 13   7.1 460 true 18   10   360
heap-manipulation/sll_to_dll_rev_false-unreach-call.i false(reach) 3.8 3.7 86 wit true 9.0 5.0 290 false(reach) 19   10   380
heap-manipulation/bubble_sort_linux_true-unreach-call.i timeout 880   930   440 wit - -
heap-manipulation/dancing_true-unreach-call.i true 880   880   470 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i false(reach) 3.6 3.5 91 wit - -
heap-manipulation/merge_sort_true-unreach-call.i timeout 880   930   480 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i timeout 880   930   280 wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) 3.5 3.5 82 wit true 7.0 3.9 260 false(reach) 12   8.1 340
list-properties/list_false-unreach-call.i false(reach) 3.5 3.5 82 wit true 9.7 5.7 400 false(reach) 16   10   340
list-properties/list_flag_false-unreach-call.i false(reach) 3.5 3.5 77 wit true 7.3 4.1 260 false(reach) 13   8.0 330
list-properties/list_search_false-unreach-call.i witness unconfirmed 3.5 3.5 79 wit true 6.9 3.9 260 error 50   42   470
list-properties/simple_false-unreach-call.i false(reach) 3.2 3.1 79 wit true 8.3 4.9 300 false(reach) 13   7.7 330
list-properties/splice_false-unreach-call.i false(reach) 3.6 3.6 86 wit true 7.9 4.4 270 false(reach) 15   8.9 360
list-properties/alternating_list_true-unreach-call.i true 880   880   280 wit - -
list-properties/list_flag_true-unreach-call.i true 880   880   300 wit - -
list-properties/list_search_true-unreach-call.i true 3.3 3.3 78 wit - -
list-properties/list_true-unreach-call.i true 880   880   250 wit - -
list-properties/simple_built_from_end_true-unreach-call.i true 880   880   250 wit - -
list-properties/simple_true-unreach-call.i true 880   880   280 wit - -
list-properties/splice_true-unreach-call.i true 880   880   330 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) 2.9 2.9 71 wit true 5.8 3.3 240 false(reach) 12   6.9 340
ldv-regression/alt_test.c_false-unreach-call.i false(reach) 3.3 3.3 75 wit true 14   7.4 490 false(reach) 15   9.3 340
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) 3.1 3.1 75 wit false(reach) 4.5 2.6 220 false(reach) 11   6.2 330
ldv-regression/fo_test.c_false-unreach-call.i false(reach) 3.1 3.1 76 wit false(reach) 8.1 4.6 360 unknown 9.5 6.7 310
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 3.1 3.1 73 wit true 4.2 2.5 220 false(reach) 12   8.0 320
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 3.0 3.0 69 wit true 4.4 2.6 220 false(reach) 11   6.9 320
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) 3.2 3.2 77 wit false(reach) 5.5 3.2 320 false(reach) 11   7.3 340
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i witness unconfirmed 3.2 3.2 78 wit true 5.4 3.1 240 true 11   5.9 320
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(reach) 3.4 3.4 74 wit true 22   12   590 false(reach) 15   8.5 340
ldv-regression/stateful_check_false-unreach-call.i witness unconfirmed 3.1 3.1 77 wit true 9.8 5.3 330 true 13   9.3 360
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 3.3 3.3 78 wit true 4.8 2.8 220 false(reach) 12   7.7 320
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 3.4 3.4 76 wit false(reach) 4.7 2.8 230 false(reach) 13   7.5 360
ldv-regression/alias_of_return.c_true-unreach-call.i true 2.5 2.5 64 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2.6 2.6 62 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2.8 2.8 67 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2.4 2.4 62 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i true 3.1 3.1 77 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true 2.5 2.6 62 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2.7 2.7 67 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2.8 2.8 67 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true 2.6 2.6 66 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2.7 2.7 66 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2.7 2.8 67 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2.8 2.8 66 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2.7 2.7 66 wit - -
ldv-regression/nested_structure_true-unreach-call.i true 2.5 2.6 70 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true 2.7 2.7 64 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true 2.7 2.7 65 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2.9 2.9 66 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 2.8 2.8 68 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true 2.9 2.9 67 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2.5 2.5 64 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true 2.8 2.8 67 wit - -
ldv-regression/test_address.c_true-unreach-call.i true 2.8 2.8 64 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2.5 2.5 66 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true 2.6 2.6 66 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true 2.8 2.8 70 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true 2.8 2.8 67 wit - -
ldv-regression/test_union.c_true-unreach-call.i true 2.6 2.6 64 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true 2.3 2.4 64 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i true 2.7 2.7 64 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i true 2.7 2.7 66 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i true 2.6 2.6 64 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2.7 2.7 64 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true 2.6 2.7 66 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2.7 2.7 65 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i witness unconfirmed 10   10   210 wit true 17   9.0 560 true 34   20   520
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i witness unconfirmed 10   9.9 210 wit true 16   8.6 570 true 34   19   530
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i witness unconfirmed 11   10   200 wit true 17   8.7 560 true 35   20   540
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i true 5.7 5.8 120 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i true 5.7 5.6 120 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i true 5.7 5.7 120 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i true 5.3 5.3 110 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i true 5.4 5.5 120 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i true 5.9 5.9 110 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i true 5.8 5.8 120 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i true 5.6 5.6 120 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i true 5.1 5.1 110 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i true 5.6 5.6 110 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 9100   9200   9300 81 240   130   8700   81 440   270   9300  
    correct results 69 6400   6400   7000 17 140   77   5300   16 220   140   5700  
        correct true 52 6300   6300   5600 12 0   0   0   1 0   0   0  
        correct false 17 57   57   1300 5 140   77   5300   15 220   140   5700  
    incorrect results 1 3.6 3.5 91 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 1 3.6 3.5 91 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 137) 105
Run set sv-comp16.HeapReach