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 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]]
Run set sv-comp16.HeapReach
Options -sv-comp16-bam -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-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.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) 13   6.1 530 wit false(reach) 16   8.5 470 true 13 7.8 330
heap-manipulation/dll_of_dll_false-unreach-call.i error 4.0 1.6 250 wit - -
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 6.4 2.3 360 wit false(reach) 8.4 4.7 410 true 14 8.8 330
heap-manipulation/sll_to_dll_rev_false-unreach-call.i false(reach) 10   4.0 420 wit false(reach) 12   6.4 430 true 13 7.6 330
heap-manipulation/bubble_sort_linux_true-unreach-call.i false(reach) 12   5.3 540 wit - -
heap-manipulation/dancing_true-unreach-call.i error 4.9 2.0 260 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i error 5.0 2.0 250 wit - -
heap-manipulation/merge_sort_true-unreach-call.i false(reach) 9.4 3.4 490 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i false(reach) 14   7.8 500 wit - -
list-properties/alternating_list_false-unreach-call.i witness unconfirmed 5.6 2.1 340 wit true 6.7 3.8 270 error 43 34   500
list-properties/list_false-unreach-call.i false(reach) 7.9 2.8 380 wit true 7.5 4.2 280 false(reach) 45 29   710
list-properties/list_flag_false-unreach-call.i false(reach) 6.9 2.5 350 wit false(reach) 8.8 4.9 370 false(reach) 15 7.9 350
list-properties/list_search_false-unreach-call.i witness unconfirmed 8.5 3.2 400 wit true 5.9 3.3 270 true 17 11   360
list-properties/simple_false-unreach-call.i false(reach) 7.0 2.6 360 wit false(reach) 8.2 4.5 360 false(reach) 14 7.5 340
list-properties/splice_false-unreach-call.i false(reach) 7.7 2.8 390 wit false(reach) 7.9 4.4 370 false(reach) 17 11   350
list-properties/alternating_list_true-unreach-call.i false(reach) 6.9 2.5 390 wit - -
list-properties/list_flag_true-unreach-call.i false(reach) 8.6 3.0 410 wit - -
list-properties/list_search_true-unreach-call.i false(reach) 10   3.7 500 wit - -
list-properties/list_true-unreach-call.i false(reach) 7.2 2.6 380 wit - -
list-properties/simple_built_from_end_true-unreach-call.i false(reach) 8.3 3.0 460 wit - -
list-properties/simple_true-unreach-call.i false(reach) 8.0 2.9 390 wit - -
list-properties/splice_true-unreach-call.i false(reach) 7.5 2.7 420 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) 4.5 2.1 230 wit false(reach) 5.0 2.9 240 true 11 6.9 320
ldv-regression/alt_test.c_false-unreach-call.i false(reach) 7.3 2.6 360 wit false(reach) 9.4 5.2 390 true 12 6.6 330
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) 3.9 1.8 230 wit false(reach) 4.5 2.7 230 false(reach) 12 6.6 320
ldv-regression/fo_test.c_false-unreach-call.i witness unconfirmed 6.5 2.4 350 wit true 6.7 3.8 260 unknown 11 6.3 320
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 4.0 1.8 230 wit false(reach) 4.1 2.4 230 true 12 7.2 320
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 3.4 1.6 230 wit false(reach) 4.7 2.8 220 true 14 7.9 350
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) 3.9 1.7 230 wit true 6.0 3.4 240 false(reach) 12 6.9 330
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) 5.6 2.3 340 wit false(reach) 6.7 3.9 330 true 12 9.1 340
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(reach) 8.3 2.8 390 wit false(reach) 7.6 4.2 360 true 14 8.0 360
ldv-regression/stateful_check_false-unreach-call.i false(reach) 5.7 2.1 360 wit false(reach) 8.2 4.6 370 true 11 8.6 330
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 4.3 1.9 230 wit false(reach) 4.4 2.6 230 false(reach) 12 9.9 340
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 3.5 1.6 230 wit false(reach) 4.7 2.8 230 true 13 7.3 350
ldv-regression/alias_of_return.c_true-unreach-call.i true 3.3 1.6 220 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 3.6 1.8 220 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 3.9 1.9 230 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 3.9 1.8 220 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i true 5.6 2.2 350 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true 3.5 1.6 210 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 3.7 1.7 230 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 3.5 1.7 220 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true 3.3 1.6 220 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 3.6 1.8 220 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true 3.5 1.7 210 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 3.8 1.8 220 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true 3.1 1.5 210 wit - -
ldv-regression/nested_structure_true-unreach-call.i true 3.6 1.8 210 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true 3.9 1.8 210 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true 3.3 1.5 220 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 4.7 2.1 230 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 5.7 2.3 370 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true 5.7 2.2 350 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 3.8 1.7 230 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true 3.7 1.8 220 wit - -
ldv-regression/test_address.c_true-unreach-call.i true 4.6 2.0 230 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true 3.3 1.5 220 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true 4.3 1.9 220 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true 4.3 1.9 230 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true 5.3 2.2 240 wit - -
ldv-regression/test_union.c_true-unreach-call.i true 3.7 1.8 220 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true 3.2 1.5 220 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i true 3.6 1.7 210 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i true 3.5 1.7 220 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i true 3.7 1.8 230 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 3.7 1.8 220 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true 3.0 1.4 210 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 3.5 1.7 220 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i witness unconfirmed 13   3.9 540 wit true 19   10   580 true 19 11   400
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i witness unconfirmed 12   3.8 540 wit true 15   7.8 580 true 19 13   430
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i witness unconfirmed 14   4.2 560 wit true 17   9.2 600 timeout 91 78   870
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i true 8.9 2.8 360 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i true 10   3.3 360 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i true 10   3.2 350 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i true 10   3.3 350 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i true 10   3.3 350 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i true 9.0 2.9 350 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i true 8.8 2.8 340 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i true 10   3.3 350 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i true 10   3.3 340 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i true 10   3.3 360 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 510 200 25000 81 200   110   8300   81 470   320   9300  
    correct results 62 340 140 17000 18 130   75   5800   18 270   160   6400  
        correct true 44 230 92 11000 2 0   0   0   11 0   0   0  
        correct false 18 110 46 5900 16 130   75   5800   7 270   160   6400  
    incorrect results 10 92 37 4500 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 10 92 37 4500 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 137) -54
Run set sv-comp16.HeapReach