Tool symbiotic 3.0.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-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:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 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/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.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 false(reach) 18     18     6.7 wit false(reach) 15   8.7 460 unknown 10   6.9 320
heap-manipulation/dll_of_dll_false-unreach-call.i false(reach) 18     18     6.8 wit false(reach) 11   6.0 440 unknown 8.9 7.0 310
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 18     18     6.7 wit false(reach) 8.6 4.7 400 unknown 10   5.9 320
heap-manipulation/sll_to_dll_rev_false-unreach-call.i false(reach) 18     18     6.8 wit false(reach) 9.9 5.8 410 unknown 8.8 6.4 310
heap-manipulation/bubble_sort_linux_true-unreach-call.i true 18     18     5.9 wit - -
heap-manipulation/dancing_true-unreach-call.i timeout 900     900     14   wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i false(reach) 18     18     7.0 wit - -
heap-manipulation/merge_sort_true-unreach-call.i timeout 900     900     13   wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i timeout 900     900     48   wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) 18     18     6.7 wit false(reach) 8.3 4.7 370 unknown 10   8.3 320
list-properties/list_false-unreach-call.i witness unconfirmed 36     36     6.9 wit true 5.9 3.3 250 unknown 9.3 5.4 310
list-properties/list_flag_false-unreach-call.i false(reach) 35     35     6.6 wit false(reach) 8.3 4.6 350 unknown 9.9 6.0 340
list-properties/list_search_false-unreach-call.i false(reach) 18     18     6.8 wit false(reach) 9.6 5.3 380 unknown 9.0 5.1 310
list-properties/simple_false-unreach-call.i false(reach) 36     36     6.6 wit false(reach) 7.8 4.5 350 unknown 8.7 5.4 310
list-properties/splice_false-unreach-call.i false(reach) 18     18     6.7 wit false(reach) 9.5 5.3 370 unknown 8.9 5.7 310
list-properties/alternating_list_true-unreach-call.i timeout 900     900     8.5 wit - -
list-properties/list_flag_true-unreach-call.i timeout 900     900     16   wit - -
list-properties/list_search_true-unreach-call.i true 18     18     5.7 wit - -
list-properties/list_true-unreach-call.i timeout 900     900     62   wit - -
list-properties/simple_built_from_end_true-unreach-call.i timeout 900     900     8.5 wit - -
list-properties/simple_true-unreach-call.i timeout 900     900     8.2 wit - -
list-properties/splice_true-unreach-call.i timeout 900     900     9.6 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) 18     18     6.7 wit false(reach) 5.1 3.0 240 unknown 11   7.6 320
ldv-regression/alt_test.c_false-unreach-call.i false(reach) 18     18     6.8 wit false(reach) 10   5.6 400 unknown 10   6.1 330
ldv-regression/callfpointer.c_false-unreach-call.i witness unconfirmed .096 .12  6.6 wit true 4.4 2.7 220 unknown 8.7 5.1 320
ldv-regression/fo_test.c_false-unreach-call.i unknown .19  .20  5.8 wit - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 18     18     8.3 wit false(reach) 4.8 2.7 230 unknown 9.4 5.4 310
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 18     18     6.6 wit false(reach) 4.6 2.8 220 unknown 8.9 5.1 310
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) .19  .21  6.8 wit false(reach) 5.2 3.0 240 unknown 9.1 5.3 300
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) 19     19     6.8 wit false(reach) 6.4 3.6 330 unknown 8.8 5.4 300
ldv-regression/rule60_list2.c_false-unreach-call_1.i witness unconfirmed .22  .25  6.8 wit true 6.4 3.6 250 unknown 8.8 5.2 340
ldv-regression/stateful_check_false-unreach-call.i timeout 900     900     7.0 wit - -
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 18     18     6.8 wit false(reach) 5.2 3.0 230 unknown 11   6.2 320
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 18     18     6.7 wit false(reach) 4.6 2.7 230 unknown 9.1 5.5 300
ldv-regression/alias_of_return.c_true-unreach-call.i true .090 .11  5.6 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true .16  .18  5.8 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true .16  .19  5.7 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true .084 .11  5.7 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i unknown 18     18     5.9 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true .092 .12  5.5 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 18     18     5.8 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 18     18     5.6 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true .18  .20  5.8 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true .16  .19  5.6 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true .095 .12  5.5 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true .090 .11  5.6 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true .10  .12  6.0 wit - -
ldv-regression/nested_structure_true-unreach-call.i true .065 .085 5.7 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true .12  .14  5.8 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true .099 .12  5.7 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 71     71     6.1 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 18     18     5.7 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true 70     70     6.1 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true .17  .18  5.9 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true .060 .083 5.6 wit - -
ldv-regression/test_address.c_true-unreach-call.i true .082 .11  5.6 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true .17  .19  5.7 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true .15  .17  5.6 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true .095 .11  5.8 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true .076 .093 5.7 wit - -
ldv-regression/test_union.c_true-unreach-call.i true .12  .14  5.7 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true .083 .11  5.8 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i true .16  .19  5.7 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i true .17  .20  5.8 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i true .089 .11  5.7 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true .15  .18  5.7 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true .16  .18  5.8 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true .081 .10  5.7 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i error .42  .44  10   wit - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i error .43  .44  10   wit - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i error .44  .46  11   wit - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i error .26  .27  10   wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i error .37  .39  10   wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i error .40  .42  10   wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i error .37  .40  10   wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i error .25  .27  10   wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i error .17  .19  10   wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i error .42  .44  10   wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i error .28  .29  10   wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i error .23  .24  10   wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i error .30  .32  10   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 9600 9600 680   81 150   86   6400   81 190   120   6300  
    correct results 52 560 560 320   17 130   76   5600   0 160   100   5300  
        correct true 35 230 240 200   0 0   0   0   0 0   0   0  
        correct false 17 320 320 120   17 130   76   5600   0 160   100   5300  
    incorrect results 1 18 18 7.0 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 1 18 18 7.0 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 137) 71
Run set sv-comp16.HeapReach