Tool CPAchecker 1.4-svn 18373
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 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]]
Run set sv-comp16.HeapReach
Options -sv-comp16--refsel -disable-java-assertions -heap 12500m -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-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.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) 74   66   800 wit false(reach) 11   6.1 420 unknown 22 12   420
heap-manipulation/dll_of_dll_false-unreach-call.i false(reach) 7.9 2.9 380 wit false(reach) 10   5.7 410 true 13 8.1 330
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 7.9 2.9 380 wit false(reach) 9.5 5.2 390 false(reach) 20 11   390
heap-manipulation/sll_to_dll_rev_false-unreach-call.i timeout 900   850   3100 wit - -
heap-manipulation/bubble_sort_linux_true-unreach-call.i timeout 900   860   5000 wit - -
heap-manipulation/dancing_true-unreach-call.i error (recursion) 4.6 2.0 230 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i false(reach) 7.8 2.8 390 wit - -
heap-manipulation/merge_sort_true-unreach-call.i timeout 900   890   990 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i timeout 900   890   790 wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) 7.8 2.9 380 wit false(reach) 7.1 4.0 360 false(reach) 15 8.0 360
list-properties/list_false-unreach-call.i timeout 900   820   15000 wit - -
list-properties/list_flag_false-unreach-call.i false(reach) 7.5 2.7 370 wit false(reach) 8.6 4.8 360 false(reach) 15 8.3 380
list-properties/list_search_false-unreach-call.i false(reach) 23   15   500 wit false(reach) 7.7 4.3 360 false(reach) 80 69   470
list-properties/simple_false-unreach-call.i false(reach) 7.9 2.8 370 wit false(reach) 7.5 4.2 350 false(reach) 16 8.6 360
list-properties/splice_false-unreach-call.i false(reach) 6.8 2.5 370 wit false(reach) 7.6 4.2 350 false(reach) 15 8.1 340
list-properties/alternating_list_true-unreach-call.i timeout 900   850   7000 wit - -
list-properties/list_flag_true-unreach-call.i timeout 900   890   870 wit - -
list-properties/list_search_true-unreach-call.i true 600   600   830 wit - -
list-properties/list_true-unreach-call.i timeout 900   890   1100 wit - -
list-properties/simple_built_from_end_true-unreach-call.i timeout 900   890   910 wit - -
list-properties/simple_true-unreach-call.i timeout 900   860   4300 wit - -
list-properties/splice_true-unreach-call.i timeout 900   870   2200 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) 4.4 1.9 240 wit false(reach) 5.2 3.0 240 false(reach) 13 7.5 340
ldv-regression/alt_test.c_false-unreach-call.i false(reach) 6.8 2.4 370 wit false(reach) 9.5 5.2 390 false(reach) 17 9.3 360
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) 3.9 1.8 220 wit false(reach) 4.4 2.6 230 false(reach) 12 7.7 340
ldv-regression/fo_test.c_false-unreach-call.i false(reach) 6.3 2.3 270 wit false(reach) 8.3 4.6 360 unknown 11 7.9 310
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 3.6 1.7 230 wit false(reach) 5.2 3.0 240 false(reach) 13 7.4 350
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 4.1 1.9 230 wit false(reach) 4.7 2.9 230 false(reach) 12 7.4 330
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) 4.4 2.0 250 wit false(reach) 5.3 3.1 240 false(reach) 12 7.4 330
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) 4.8 2.1 240 wit false(reach) 6.2 3.7 330 false(reach) 14 8.1 330
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(reach) 6.2 2.2 370 wit false(reach) 7.7 4.2 350 false(reach) 16 8.6 350
ldv-regression/stateful_check_false-unreach-call.i false(reach) 5.0 2.0 260 wit false(reach) 7.6 4.3 340 false(reach) 18 9.9 380
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 4.3 1.9 240 wit false(reach) 4.9 2.9 230 false(reach) 13 8.7 350
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 4.1 1.9 230 wit false(reach) 4.4 2.6 230 false(reach) 13 7.7 340
ldv-regression/alias_of_return.c_true-unreach-call.i true 3.7 1.7 210 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 3.3 1.5 210 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 3.7 1.8 220 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2.9 1.4 210 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i true 4.1 1.8 210 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true 3.5 1.6 200 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 3.8 1.8 220 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 3.2 1.5 220 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true 3.5 1.7 210 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 3.4 1.6 210 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true 3.5 1.6 210 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 3.1 1.4 210 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true 3.4 1.7 210 wit - -
ldv-regression/nested_structure_true-unreach-call.i true 3.6 1.7 210 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true 3.6 1.7 210 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true 3.1 1.4 210 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 3.9 1.8 220 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 5.1 2.2 240 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true 4.7 2.0 230 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 3.5 1.5 220 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.0 1.8 220 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true 3.4 1.6 200 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true 4.3 1.9 210 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true 4.2 1.8 220 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true 4.7 2.0 220 wit - -
ldv-regression/test_union.c_true-unreach-call.i true 3.5 1.6 210 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true 3.4 1.6 200 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.5 1.7 210 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i true 3.6 1.7 210 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 3.6 1.7 210 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true 3.5 1.6 210 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 3.4 1.7 210 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i false(reach) 18   7.0 600 wit false(reach) 29   18   880 timeout 91 79   860
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i false(reach) 18   7.1 610 wit false(reach) 34   22   890 timeout 91 79   890
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i false(reach) 19   7.2 600 wit false(reach) 30   19   890 timeout 90 76   890
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i true 11   3.8 380 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i true 9.8 3.3 390 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i true 11   3.8 380 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i true 11   3.8 390 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i true 11   3.6 390 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i true 9.3 3.2 390 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i true 11   3.8 390 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i true 11   3.8 390 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i true 11   3.6 390 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i true 11   3.9 390 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 11000   10000   62000 81 240   140   9100   81 630   470   9800  
    correct results 68 1100   830   20000 23 240   140   9100   18 630   470   9800  
        correct true 45 840   690   12000 0 0   0   0   1 0   0   0  
        correct false 23 260   140   8500 23 240   140   9100   17 630   470   9800  
    incorrect results 1 7.8 2.8 390 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 1 7.8 2.8 390 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 137) 97
Run set sv-comp16.HeapReach