Tool Cascade 2.0
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-16 07:57:57 CET [[ 2016-01-16 11:29:40 CET ]] [[ 2016-01-16 11:29:59 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/cascade.2016-01-16_0757.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cascade.2016-01-16_0757.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime wit1_walltime wit1_memUsage (MB) wit2_status wit2_cputime wit2_walltime wit2_memUsage (MB)
heap-manipulation/bubble_sort_linux_false-unreach-call.i unknown 860   850    1000 wit - -
heap-manipulation/dll_of_dll_false-unreach-call.i unknown 3.5 1.1  150 wit - -
heap-manipulation/merge_sort_false-unreach-call.i unknown 850   850    1100 wit - -
heap-manipulation/sll_to_dll_rev_false-unreach-call.i unknown 4.5 2.3  170 wit - -
heap-manipulation/bubble_sort_linux_true-unreach-call.i unknown 860   850    990 wit - -
heap-manipulation/dancing_true-unreach-call.i unknown 2.8 1.0  120 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i unknown 4.6 1.3  180 wit - -
heap-manipulation/merge_sort_true-unreach-call.i true 860   850    530 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i unknown 860   850    490 wit - -
list-properties/alternating_list_false-unreach-call.i unknown 3.5 2.3  130 wit - -
list-properties/list_false-unreach-call.i unknown 3.4 2.3  130 wit - -
list-properties/list_flag_false-unreach-call.i unknown 3.3 2.2  130 wit - -
list-properties/list_search_false-unreach-call.i unknown 5.3 2.6  170 wit - -
list-properties/simple_false-unreach-call.i unknown 3.1 2.2  120 wit - -
list-properties/splice_false-unreach-call.i unknown 3.7 2.3  140 wit - -
list-properties/alternating_list_true-unreach-call.i true 850   850    360 wit - -
list-properties/list_flag_true-unreach-call.i true 850   850    620 wit - -
list-properties/list_search_true-unreach-call.i true 850   850    460 wit - -
list-properties/list_true-unreach-call.i true 850   850    990 wit - -
list-properties/simple_built_from_end_true-unreach-call.i true 850   850    210 wit - -
list-properties/simple_true-unreach-call.i true 850   850    310 wit - -
list-properties/splice_true-unreach-call.i true 850   850    1000 wit - -
ldv-regression/1_3.c_false-unreach-call.i unknown 2.1 2.0  100 wit - -
ldv-regression/alt_test.c_false-unreach-call.i unknown 4.4 2.3  170 wit - -
ldv-regression/callfpointer.c_false-unreach-call.i unknown 1.7 1.9  100 wit - -
ldv-regression/fo_test.c_false-unreach-call.i unknown 4.2 2.3  140 wit - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i unknown 1.8 1.9  100 wit - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i unknown 1.9 2.0  100 wit - -
ldv-regression/recursive_list.c_false-unreach-call.i unknown 2.1 2.0  110 wit - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i unknown 2.5 2.2  110 wit - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i unknown 4.2 2.2  170 wit - -
ldv-regression/stateful_check_false-unreach-call.i unknown 3.1 2.2  130 wit - -
ldv-regression/test_while_int.c_false-unreach-call.i unknown 2.0 2.0  100 wit - -
ldv-regression/test_while_int.c_false-unreach-call_1.i unknown 1.8 1.9  100 wit - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 1.4 .75 92 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 1.3 .68 94 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 1.5 .76 92 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 1.4 .74 92 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i timeout 900   800    1300 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true 1.4 .74 90 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 1.5 .79 92 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 1.5 .80 93 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true 1.6 .80 93 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 1.6 .79 93 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true 1.6 .81 93 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 1.6 .80 94 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true 1.4 .71 93 wit - -
ldv-regression/nested_structure_true-unreach-call.i true 1.6 .81 93 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true 1.5 .77 93 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true 1.5 .78 92 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2.1 .94 100 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 3.3 1.2  140 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true 3.6 1.2  150 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2.1 .82 110 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true 1.5 .80 92 wit - -
ldv-regression/test_address.c_true-unreach-call.i true 2.6 1.0  120 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true 1.4 .73 93 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true 2.9 1.1  120 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true 2.9 1.1  120 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true 4.0 1.2  160 wit - -
ldv-regression/test_union.c_true-unreach-call.i true 1.5 .76 93 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true 1.5 .80 93 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i true 1.5 .79 93 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i true 1.6 .84 94 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i true 1.3 .66 93 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 1.5 .80 93 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true 1.2 .63 90 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 1.4 .79 90 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i unknown 17   3.1  410 wit - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i unknown 17   3.0  430 wit - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i unknown 15   2.8  390 wit - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i unknown 17   3.1  390 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i unknown 17   3.0  410 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i unknown 16   3.0  430 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i unknown 13   2.6  350 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i unknown 16   3.0  400 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i unknown 16   2.9  410 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i unknown 16   3.1  430 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i unknown 16   2.9  400 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i unknown 16   3.0  410 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i unknown 20   3.4  430 wit - -
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime wit1_walltime wit1_memUsage (MB) wit2_status wit2_cputime wit2_walltime wit2_memUsage (MB)
total tasks 81 11000 11000 21000 81 0   81 0  
    correct results 41 6900 6800 7800 0 0   0 0  
        correct true 41 6900 6800 7800 0 0   0 0  
        correct false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 137) 82
Run set sv-comp16.HeapReach