Tool Forester
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus13; zeus15; 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-06 15:22:35 CET [[ 2016-01-15 09:07:03 CET ]] [[ 2016-01-15 22:21:21 CET ]]
Run set sv-comp16.HeapReach
Options --trace error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/forester.2016-01-06_1522.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/forester.2016-01-06_1522.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) .046 .049 10   wit false(reach) 13   7.3 470 true 13   7.3 340
heap-manipulation/dll_of_dll_false-unreach-call.i unknown .17  .18  9.7 wit - -
heap-manipulation/merge_sort_false-unreach-call.i unknown .17  .18  10   wit - -
heap-manipulation/sll_to_dll_rev_false-unreach-call.i unknown .22  .23  11   wit - -
heap-manipulation/bubble_sort_linux_true-unreach-call.i true 1.4   1.4   24   wit - -
heap-manipulation/dancing_true-unreach-call.i unknown .16  .18  10   wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i unknown .12  .13  10   wit - -
heap-manipulation/merge_sort_true-unreach-call.i unknown .33  .34  13   wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i unknown .27  .28  12   wit - -
list-properties/alternating_list_false-unreach-call.i unknown .16  .17  9.4 wit - -
list-properties/list_false-unreach-call.i witness timeout .18  .19  9.1 wit timeout 91   82   710 true 11   6.6 330
list-properties/list_flag_false-unreach-call.i unknown .047 .051 8.4 wit - -
list-properties/list_search_false-unreach-call.i unknown .17  .18  10   wit - -
list-properties/simple_false-unreach-call.i false(reach) .075 .080 8.6 wit false(reach) 8.3 4.6 370 true 11   7.3 330
list-properties/splice_false-unreach-call.i unknown .13  .14  11   wit - -
list-properties/alternating_list_true-unreach-call.i unknown .19  .20  9.7 wit - -
list-properties/list_flag_true-unreach-call.i unknown .047 .050 8.4 wit - -
list-properties/list_search_true-unreach-call.i true .19  .19  11   wit - -
list-properties/list_true-unreach-call.i unknown .39  .40  10   wit - -
list-properties/simple_built_from_end_true-unreach-call.i unknown .031 .034 8.3 wit - -
list-properties/simple_true-unreach-call.i true .043 .047 8.5 wit - -
list-properties/splice_true-unreach-call.i unknown .15  .16  11   wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) .043 .047 8.4 wit false(reach) 5.0 3.0 240 true 10   5.7 330
ldv-regression/alt_test.c_false-unreach-call.i false(reach) .042 .045 8.7 wit false(reach) 9.0 5.0 400 true 11   6.2 330
ldv-regression/callfpointer.c_false-unreach-call.i unknown .064 .076 8.7 wit - -
ldv-regression/fo_test.c_false-unreach-call.i false(reach) .047 .051 8.7 wit false(reach) 8.5 4.7 390 unknown 10   6.8 320
ldv-regression/mutex_lock_int.c_false-unreach-call.i unknown .048 .050 8.2 wit - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i unknown .042 .044 8.2 wit - -
ldv-regression/recursive_list.c_false-unreach-call.i unknown .047 .050 8.2 wit - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i unknown .071 .077 8.3 wit - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i unknown .062 .067 8.6 wit - -
ldv-regression/stateful_check_false-unreach-call.i unknown .050 .054 8.5 wit - -
ldv-regression/test_while_int.c_false-unreach-call.i unknown .046 .051 8.1 wit - -
ldv-regression/test_while_int.c_false-unreach-call_1.i unknown .038 .042 8.0 wit - -
ldv-regression/alias_of_return.c_true-unreach-call.i unknown .034 .035 8.1 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i unknown .052 .056 8.0 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i unknown .038 .039 8.0 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i unknown .045 .049 8.1 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i unknown .059 .062 8.2 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true .050 .053 11   wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i unknown .068 .071 8.1 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i unknown .052 .058 8.5 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true .048 .056 11   wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true .051 .058 11   wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true .093 .10  11   wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true .069 .080 11   wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true .066 .070 11   wit - -
ldv-regression/nested_structure_true-unreach-call.i true .057 .062 11   wit - -
ldv-regression/oomInt.c_true-unreach-call.i unknown .039 .043 8.2 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i unknown .035 .038 8.0 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i unknown .041 .043 8.3 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true .039 .043 8.4 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i unknown .041 .047 8.9 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i unknown .045 .050 8.3 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true .059 .065 11   wit - -
ldv-regression/test_address.c_true-unreach-call.i unknown .043 .046 8.4 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true .056 .062 11   wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true .037 .040 8.6 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true .095 .10  11   wit - -
ldv-regression/test_overflow.c_true-unreach-call.i unknown .075 .080 8.6 wit - -
ldv-regression/test_union.c_true-unreach-call.i unknown .037 .041 8.1 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i unknown .048 .053 8.4 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i unknown .035 .037 8.1 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i unknown .037 .041 8.0 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i unknown .033 .037 8.0 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i unknown .033 .036 7.9 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true .049 .053 11   wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true .058 .067 11   wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i unknown .17  .17  17   wit - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i unknown .17  .18  16   wit - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i unknown .17  .18  16   wit - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i unknown .18  .18  16   wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i unknown .23  .24  16   wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i unknown .16  .17  16   wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i unknown .18  .18  16   wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i unknown .17  .17  16   wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i unknown .20  .21  16   wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i unknown .22  .23  16   wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i unknown .13  .14  16   wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i unknown .17  .17  16   wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i unknown .14  .15  19   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 9.3  9.8  860 81 130   110   2600   81 66   40   2000  
    correct results 22 2.7  2.8  240 5 44   25   1900   4 55   33   1700  
        correct true 17 2.4  2.6  190 0 0   0   0   4 0   0   0  
        correct false 5 .25 .27 44 5 44   25   1900   0 55   33   1700  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 137) 39
Run set sv-comp16.HeapReach