Tool Forest svc_16_20151108
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]
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-09 23:49:59 CET [[ 2016-01-15 09:05:13 CET ]] [[ 2016-01-15 22:20:31 CET ]]
Run set sv-comp16.HeapReach
Options -svcomp [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/forest.2016-01-09_2349.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 unknown .77 .85 39   wit - -
heap-manipulation/dll_of_dll_false-unreach-call.i true .79 .87 39   wit - -
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 1.5  1.7  39   wit false(reach) 9.1 5.0 390 true 13 7.8 330
heap-manipulation/sll_to_dll_rev_false-unreach-call.i true .71 .81 39   wit - -
heap-manipulation/bubble_sort_linux_true-unreach-call.i false(reach) 1.1  1.3  39   wit - -
heap-manipulation/dancing_true-unreach-call.i true 1.3  1.6  39   wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i true .75 .84 39   wit - -
heap-manipulation/merge_sort_true-unreach-call.i unknown .61 .69 39   wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i true .54 .62 39   wit - -
list-properties/alternating_list_false-unreach-call.i true .60 .68 38   wit - -
list-properties/list_false-unreach-call.i timeout 900    900    680   wit - -
list-properties/list_flag_false-unreach-call.i unknown .57 .65 36   wit - -
list-properties/list_search_false-unreach-call.i true .52 .59 38   wit - -
list-properties/simple_false-unreach-call.i unknown .49 .57 38   wit - -
list-properties/splice_false-unreach-call.i true .22 .31 7.5 wit - -
list-properties/alternating_list_true-unreach-call.i true .51 .60 38   wit - -
list-properties/list_flag_true-unreach-call.i true .60 .68 38   wit - -
list-properties/list_search_true-unreach-call.i true .60 .68 39   wit - -
list-properties/list_true-unreach-call.i true .19 .26 7.2 wit - -
list-properties/simple_built_from_end_true-unreach-call.i unknown .27 .34 5.1 wit - -
list-properties/simple_true-unreach-call.i true .62 .70 38   wit - -
list-properties/splice_true-unreach-call.i timeout 900    900    5400   wit - -
ldv-regression/1_3.c_false-unreach-call.i unknown .17 .24 4.5 wit - -
ldv-regression/alt_test.c_false-unreach-call.i true .41 .49 7.5 wit - -
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) .52 .60 39   wit false(reach) 4.4 2.7 220 true 11 8.0 320
ldv-regression/fo_test.c_false-unreach-call.i unknown .19 .25 4.9 wit - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i unknown .52 .62 38   wit - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i unknown .59 .68 38   wit - -
ldv-regression/recursive_list.c_false-unreach-call.i unknown .18 .25 4.6 wit - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i unknown .16 .23 7.1 wit - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i true .67 .78 38   wit - -
ldv-regression/stateful_check_false-unreach-call.i true 4.1  4.8  39   wit - -
ldv-regression/test_while_int.c_false-unreach-call.i unknown .56 .65 38   wit - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) .50 .58 38   wit false(reach) 4.8 2.7 230 true 10 6.1 320
ldv-regression/alias_of_return.c_true-unreach-call.i true .64 .75 38   wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true .61 .74 38   wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i unknown .58 .67 38   wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true .66 .77 38   wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i unknown .23 .31 7.3 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true .57 .67 38   wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true .74 .88 38   wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true .61 .73 38   wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true .66 .79 38   wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i unknown .50 .57 38   wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true .69 .81 38   wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i unknown .56 .65 38   wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true .67 .78 38   wit - -
ldv-regression/nested_structure_true-unreach-call.i unknown .55 .64 38   wit - -
ldv-regression/oomInt.c_true-unreach-call.i unknown .49 .56 38   wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i unknown .52 .61 38   wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i unknown .21 .30 9.5 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true .64 .72 37   wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true .65 .74 38   wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i false(reach) .70 .85 38   wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true .56 .64 38   wit - -
ldv-regression/test_address.c_true-unreach-call.i true .60 .71 38   wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true .51 .59 38   wit - -
ldv-regression/test_malloc-1_true-unreach-call.i unknown .47 .54 38   wit - -
ldv-regression/test_malloc-2_true-unreach-call.i unknown .52 .61 38   wit - -
ldv-regression/test_overflow.c_true-unreach-call.i unknown .39 .47 5.3 wit - -
ldv-regression/test_union.c_true-unreach-call.i true .63 .74 38   wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true .61 .72 38   wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i true .65 .77 38   wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i true .65 .77 38   wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i unknown .53 .63 38   wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true .61 .73 38   wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true .58 .67 38   wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true .62 .72 38   wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i unknown 1.2  1.3  8.5 wit - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i unknown 1.1  1.2  8.2 wit - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i unknown 1.3  1.3  8.4 wit - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i unknown 1.2  1.3  8.2 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i unknown 1.2  1.3  8.1 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i unknown 1.1  1.1  8.1 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i unknown 1.3  1.4  8.2 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i unknown 1.2  1.3  8.2 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i unknown 1.2  1.3  8.2 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i unknown 1.2  1.3  8.2 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i true 1.2  1.3  8.1 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i unknown 1.2  1.2  8.1 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i unknown 1.3  1.3  8.1 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 1900   1900   8300 81 18   10   840   81 33   22   970  
    correct results 33 22   26   1200 3 18   10   840   3 33   22   970  
        correct true 30 19   23   1100 0 0   0   0   3 0   0   0  
        correct false 3 2.5 2.9 120 3 18   10   840   0 33   22   970  
    incorrect results 10 9.9 11   320 0 0   0   0   0 0   0   0  
        incorrect true 8 8.0 9.3 250 0 0   0   0   0 0   0   0  
        incorrect false 2 1.9 2.2 77 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 137) -225
Run set sv-comp16.HeapReach