Tool Predator-HP
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus05; zeus06; zeus08; zeus09; zeus10; zeus11; zeus13; zeus14; zeus16; zeus17; zeus18; zeus19; 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-07 06:55:25 CET [[ 2016-01-15 09:23:45 CET ]] [[ 2016-01-15 22:28:52 CET ]]
Run set sv-comp16.HeapReach
Options --witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/predatorhp.2016-01-07_0655.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/predatorhp.2016-01-07_0655.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) 1.2   1.0 39 wit false(reach) 16   9.0 490 true 16 8.7 360
heap-manipulation/dll_of_dll_false-unreach-call.i false(reach) 4.0   2.0 50 wit false(reach) 11   6.3 420 true 16 9.2 350
heap-manipulation/merge_sort_false-unreach-call.i false(reach) .15  1.0 24 wit false(reach) 9.7 5.3 400 true 13 7.9 320
heap-manipulation/sll_to_dll_rev_false-unreach-call.i false(reach) 2.5   1.0 59 wit false(reach) 12   6.9 440 true 15 8.4 350
heap-manipulation/bubble_sort_linux_true-unreach-call.i true 1.8   1.0 45 wit - -
heap-manipulation/dancing_true-unreach-call.i true .43  1.0 22 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i true 2.7   1.0 57 wit - -
heap-manipulation/merge_sort_true-unreach-call.i true 2.0   1.0 47 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i true 2.2   1.0 60 wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) .20  1.0 21 wit false(reach) 11   6.1 390 true 12 6.7 350
list-properties/list_false-unreach-call.i witness timeout 1.6   1.0 21 wit timeout 91   78   540 true 12 6.9 320
list-properties/list_flag_false-unreach-call.i false(reach) .21  1.0 21 wit false(reach) 11   6.2 370 true 12 8.7 340
list-properties/list_search_false-unreach-call.i false(reach) .14  1.0 22 wit false(reach) 11   6.1 380 true 12 7.9 310
list-properties/simple_false-unreach-call.i false(reach) .17  1.1 21 wit false(reach) 12   6.3 370 true 12 6.8 330
list-properties/splice_false-unreach-call.i false(reach) .23  1.0 21 wit false(reach) 12   6.8 390 true 13 8.5 330
list-properties/alternating_list_true-unreach-call.i timeout 900     320   1300 wit - -
list-properties/list_flag_true-unreach-call.i true 2.5   1.0 22 wit - -
list-properties/list_search_true-unreach-call.i true .29  1.0 22 wit - -
list-properties/list_true-unreach-call.i true 3.1   1.0 22 wit - -
list-properties/simple_built_from_end_true-unreach-call.i true 3.0   1.0 22 wit - -
list-properties/simple_true-unreach-call.i true 3.1   1.0 22 wit - -
list-properties/splice_true-unreach-call.i timeout 900     430   1100 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) .14  1.0 20 wit false(reach) 5.1 2.9 230 true 12 8.2 320
ldv-regression/alt_test.c_false-unreach-call.i false(reach) .14  1.0 21 wit false(reach) 13   7.2 400 true 13 7.7 350
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) .11  1.0 20 wit false(reach) 4.4 2.7 220 false(reach) 12 7.4 350
ldv-regression/fo_test.c_false-unreach-call.i false(reach) .13  1.0 22 wit false(reach) 9.0 5.0 380 unknown 10 6.5 320
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) .11  1.0 20 wit false(reach) 4.5 2.7 220 true 11 6.1 320
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) .13  1.0 19 wit false(reach) 4.8 2.9 230 true 11 7.2 330
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) .17  1.0 21 wit false(reach) 5.3 3.1 250 true 12 8.9 320
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) .18  1.0 21 wit false(reach) 7.2 4.1 330 true 12 6.7 330
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(reach) .17  1.0 22 wit false(reach) 10   5.5 380 true 13 7.4 340
ldv-regression/stateful_check_false-unreach-call.i false(reach) .15  1.0 21 wit false(reach) 9.5 5.3 380 true 12 7.3 330
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) .12  1.0 20 wit false(reach) 4.9 2.9 230 true 11 7.2 310
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) .13  1.1 19 wit false(reach) 4.8 2.9 230 true 11 6.9 330
ldv-regression/alias_of_return.c_true-unreach-call.i true .12  1.0 20 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true .12  1.0 19 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true .12  1.0 20 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true .12  1.0 19 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i true .17  1.0 20 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true .11  1.0 19 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true .12  1.0 19 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true .13  1.0 19 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true .11  1.0 20 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true .11  1.0 19 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true .12  1.0 19 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true .13  1.1 20 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true .11  1.0 19 wit - -
ldv-regression/nested_structure_true-unreach-call.i true .096 1.0 19 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true .11  1.0 20 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true .15  1.1 19 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true .32  1.0 21 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true .18  1.0 20 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true .16  1.0 22 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true .11  1.0 21 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true .11  1.0 19 wit - -
ldv-regression/test_address.c_true-unreach-call.i true .12  1.0 21 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true .11  1.0 20 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true .21  1.1 21 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true .11  1.0 20 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true .16  1.0 21 wit - -
ldv-regression/test_union.c_true-unreach-call.i true .11  1.0 20 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true .11  1.0 19 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i true .11  1.0 19 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i true .12  1.0 19 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i true .11  1.0 20 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true .13  1.0 19 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true .16  1.0 19 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true .17  1.1 19 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i false(reach) .76  1.0 53 wit false(reach) 59   36   880 true 18 11   400
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i false(reach) .77  1.1 50 wit false(reach) 42   26   890 true 19 12   430
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i false(reach) .73  1.0 51 wit false(reach) 56   34   880 true 18 10   410
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i unknown 1.1   1.0 52 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i unknown .90  1.0 53 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i unknown 1.1   1.1 54 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i unknown 1.1   1.0 52 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i unknown 1.0   1.0 51 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i unknown 1.1   1.0 51 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i unknown 1.1   1.0 51 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i unknown 1.1   1.0 51 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i unknown 1.1   1.0 51 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i unknown 1.0   1.0 51 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 840 4700 81 440   280   10000   81 330   200   8500  
    correct results 68 38 72 1700 24 350   200   9800   23 320   190   8200  
        correct true 44 26 46 1000 0 0   0   0   22 0   0   0  
        correct false 24 13 26 680 24 350   200   9800   1 320   190   8200  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 137) 112
Run set sv-comp16.HeapReach