Tool CPAchecker 1.4-svcomp16c
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-22-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-04 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]]
Run set sv-comp16.HeapReach
Options -sv-comp16--k-induction -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.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) 20   9.9 550 wit false(reach) 11   6.4 450 unknown 23   13   430
heap-manipulation/dll_of_dll_false-unreach-call.i unknown 93   72   1100 wit - -
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 61   19   1000 wit false(reach) 8.5 4.7 390 false(reach) 18   10   370
heap-manipulation/sll_to_dll_rev_false-unreach-call.i false(reach) 11   4.1 470 wit false(reach) 8.7 4.9 420 false(reach) 19   11   370
heap-manipulation/bubble_sort_linux_true-unreach-call.i timeout 900   410   5600 wit - -
heap-manipulation/dancing_true-unreach-call.i error (recursion) 6.3 2.2 270 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i unknown 91   71   1100 wit - -
heap-manipulation/merge_sort_true-unreach-call.i timeout 900   390   5700 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i timeout 900   390   6600 wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) 9.5 3.3 410 wit false(reach) 7.9 4.4 380 false(reach) 14   8.3 340
list-properties/list_false-unreach-call.i false(reach) 14   6.0 420 wit false(reach) 7.5 4.2 370 false(reach) 15   8.6 360
list-properties/list_flag_false-unreach-call.i false(reach) 11   4.1 400 wit false(reach) 7.0 3.9 360 false(reach) 15   8.4 350
list-properties/list_search_false-unreach-call.i false(reach) 13   3.6 480 wit false(reach) 8.6 4.8 380 false(reach) 77   66   600
list-properties/simple_false-unreach-call.i false(reach) 9.7 3.3 420 wit false(reach) 7.5 4.2 360 false(reach) 15   8.2 370
list-properties/splice_false-unreach-call.i false(reach) 12   3.9 460 wit false(reach) 7.6 4.2 380 false(reach) 18   9.8 370
list-properties/alternating_list_true-unreach-call.i timeout 900   420   3400 wit - -
list-properties/list_flag_true-unreach-call.i timeout 900   420   3600 wit - -
list-properties/list_search_true-unreach-call.i true 53   9.2 1400 wit - -
list-properties/list_true-unreach-call.i timeout 900   420   4500 wit - -
list-properties/simple_built_from_end_true-unreach-call.i timeout 900   420   3800 wit - -
list-properties/simple_true-unreach-call.i timeout 900   420   3900 wit - -
list-properties/splice_true-unreach-call.i timeout 900   410   5600 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) 4.0 1.9 240 wit false(reach) 5.3 3.0 320 false(reach) 13   7.6 340
ldv-regression/alt_test.c_false-unreach-call.i error 7.5 3.0 330 wit - -
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) 3.9 1.9 230 wit false(reach) 4.3 2.5 220 false(reach) 11   6.5 330
ldv-regression/fo_test.c_false-unreach-call.i false(reach) 6.5 2.6 310 wit false(reach) 8.4 4.7 380 unknown 9.7 5.6 310
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 4.3 2.0 240 wit false(reach) 4.7 2.7 220 false(reach) 12   7.2 330
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 4.2 2.0 240 wit false(reach) 4.8 2.9 240 false(reach) 11   6.4 330
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) 4.5 2.2 240 wit false(reach) 5.4 3.2 340 false(reach) 12   7.3 340
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) 4.0 1.8 250 wit false(reach) 5.6 3.2 330 false(reach) 14   8.0 330
ldv-regression/rule60_list2.c_false-unreach-call_1.i error 6.6 2.3 320 wit - -
ldv-regression/stateful_check_false-unreach-call.i false(reach) 16   3.9 560 wit false(reach) 7.8 4.4 360 false(reach) 18   9.9 370
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 5.2 2.0 340 wit false(reach) 4.9 2.9 230 false(reach) 13   8.0 360
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 6.1 2.3 340 wit false(reach) 4.1 2.4 230 false(reach) 12   7.3 330
ldv-regression/alias_of_return.c_true-unreach-call.i true 3.5 1.6 190 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 3.5 1.6 200 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 3.7 1.6 200 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 3.5 1.6 200 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i true 41   7.7 920 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true 2.7 1.3 190 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 3.6 1.6 200 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 3.5 1.6 200 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true 3.4 1.6 190 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2.9 1.3 200 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true 3.6 1.7 200 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2.9 1.3 200 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true 3.1 1.4 200 wit - -
ldv-regression/nested_structure_true-unreach-call.i true 3.6 1.7 200 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true 3.7 1.6 190 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true 3.6 1.6 200 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 3.5 1.5 200 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 4.6 1.9 210 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true 4.9 2.0 220 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 4.3 1.8 210 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true 3.6 1.6 200 wit - -
ldv-regression/test_address.c_true-unreach-call.i true 4.4 1.9 210 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true 3.4 1.6 190 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true 4.4 1.9 210 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true 3.7 1.6 210 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true 4.9 2.0 220 wit - -
ldv-regression/test_union.c_true-unreach-call.i true 3.0 1.4 200 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true 2.9 1.4 190 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i true 3.7 1.7 200 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i true 3.0 1.4 200 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i true 2.9 1.3 200 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 3.5 1.6 190 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true 3.5 1.6 200 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 3.5 1.6 200 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i timeout 900   380   7400 wit - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i timeout 900   370   7100 wit - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i timeout 900   370   7200 wit - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i true 8.9 2.8 350 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i true 7.8 2.4 340 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i true 8.8 2.7 350 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i true 8.9 2.8 340 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i true 7.6 2.3 340 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i true 8.8 2.7 350 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i true 7.4 2.2 350 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i true 8.7 2.7 350 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i true 7.7 2.4 340 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i true 7.5 2.3 340 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 12000 5200 87000 81 130   74   6400   81 340   220   6900  
    correct results 64 510 170 20000 19 130   74   6400   17 340   220   6900  
        correct true 45 290 95 12000 0 0   0   0   0 0   0   0  
        correct false 19 220 80 7600 19 130   74   6400   17 340   220   6900  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 137) 109
Run set sv-comp16.HeapReach