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 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.HeapReach
Options -sv-comp16 -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-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.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) 170   140   1100 wit false(reach) 11   6.2 430 unknown 21 13   400
heap-manipulation/dll_of_dll_false-unreach-call.i false(reach) 5.2 2.0 250 wit false(reach) 9.8 5.3 410 true 13 9.5 320
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 58   20   1100 wit false(reach) 9.3 5.1 370 false(reach) 20 11   390
heap-manipulation/sll_to_dll_rev_false-unreach-call.i false(reach) 160   140   1100 wit false(reach) 9.4 5.2 400 false(reach) 19 10   390
heap-manipulation/bubble_sort_linux_true-unreach-call.i timeout 900   690   4800 wit - -
heap-manipulation/dancing_true-unreach-call.i error 8.0 2.8 380 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i false(reach) 5.1 1.9 250 wit - -
heap-manipulation/merge_sort_true-unreach-call.i timeout 900   710   4700 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i timeout 900   670   6100 wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) 100   79   890 wit false(reach) 9.2 5.1 380 false(reach) 15 8.9 350
list-properties/list_false-unreach-call.i false(reach) 17   6.5 500 wit false(reach) 9.0 5.0 360 false(reach) 14 7.5 350
list-properties/list_flag_false-unreach-call.i false(reach) 110   77   1000 wit false(reach) 9.0 5.0 360 false(reach) 16 9.2 350
list-properties/list_search_false-unreach-call.i false(reach) 120   77   1000 wit false(reach) 8.9 4.9 400 false(reach) 76 66   580
list-properties/simple_false-unreach-call.i false(reach) 11   3.7 460 wit false(reach) 8.5 4.8 350 false(reach) 14 7.4 340
list-properties/splice_false-unreach-call.i false(reach) 13   4.1 500 wit false(reach) 8.3 4.5 380 false(reach) 15 8.2 360
list-properties/alternating_list_true-unreach-call.i timeout 900   680   3600 wit - -
list-properties/list_flag_true-unreach-call.i timeout 900   690   2700 wit - -
list-properties/list_search_true-unreach-call.i true 160   83   1100 wit - -
list-properties/list_true-unreach-call.i timeout 900   710   4400 wit - -
list-properties/simple_built_from_end_true-unreach-call.i timeout 900   710   3100 wit - -
list-properties/simple_true-unreach-call.i timeout 900   710   3600 wit - -
list-properties/splice_true-unreach-call.i timeout 900   720   4800 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) 6.1 2.7 340 wit false(reach) 4.9 2.9 230 false(reach) 13 11   320
ldv-regression/alt_test.c_false-unreach-call.i unknown 13   4.3 470 wit - -
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) 2.9 1.4 210 wit false(reach) 4.5 2.6 230 false(reach) 11 6.1 340
ldv-regression/fo_test.c_false-unreach-call.i false(reach) 5.7 2.2 230 wit false(reach) 8.9 4.9 390 unknown 11 8.6 310
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 4.6 1.9 320 wit false(reach) 4.6 2.8 230 false(reach) 13 7.6 350
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 5.5 2.4 330 wit false(reach) 4.6 2.7 230 false(reach) 11 10   320
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) 4.0 1.8 210 wit false(reach) 5.9 3.4 320 false(reach) 13 6.9 350
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) 4.2 1.8 220 wit false(reach) 6.6 3.7 330 false(reach) 13 7.3 330
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(reach) 5.1 1.9 240 wit false(reach) 8.9 4.9 370 false(reach) 16 12   380
ldv-regression/stateful_check_false-unreach-call.i false(reach) 5.6 2.1 230 wit false(reach) 7.7 4.3 350 false(reach) 18 9.4 370
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 3.9 1.7 210 wit false(reach) 4.8 2.9 240 false(reach) 12 8.9 330
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 3.2 1.4 200 wit false(reach) 4.9 2.8 230 false(reach) 12 7.8 320
ldv-regression/alias_of_return.c_true-unreach-call.i true 3.7 1.6 240 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 4.3 1.7 230 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 4.8 2.0 240 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 4.3 1.9 230 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i true 3.0 1.4 180 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true 3.1 1.4 190 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 4.4 1.8 240 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 4.4 1.9 240 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true 4.4 1.9 230 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 3.2 1.5 180 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true 3.3 1.5 180 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 4.5 1.9 240 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true 3.7 1.6 240 wit - -
ldv-regression/nested_structure_true-unreach-call.i true 4.4 1.9 240 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true 3.2 1.5 180 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true 3.2 1.4 180 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 3.5 1.6 190 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 7.5 2.4 300 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true 4.2 1.8 200 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 3.8 1.6 190 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true 4.3 1.9 230 wit - -
ldv-regression/test_address.c_true-unreach-call.i true 7.3 2.5 300 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true 3.4 1.5 180 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true 7.4 2.5 290 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true 6.5 2.2 300 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true 3.7 1.5 200 wit - -
ldv-regression/test_union.c_true-unreach-call.i true 3.1 1.4 180 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true 3.3 1.5 190 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i true 3.2 1.5 190 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i true 4.5 1.9 240 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i true 3.6 1.5 230 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 3.1 1.5 180 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true 3.7 1.6 240 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 4.4 1.9 240 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i false(reach) 16   6.7 510 wit false(reach) 35   23   900 timeout 91 78   850
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i false(reach) 16   6.7 520 wit false(reach) 33   21   890 timeout 91 77   880
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i false(reach) 14   6.0 520 wit false(reach) 37   23   920 timeout 91 82   870
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i true 96   83   1300 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i true 96   83   740 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i true 96   82   740 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i true 96   83   820 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i true 97   82   1300 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i true 96   83   760 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i true 97   82   750 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i true 96   83   750 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i true 96   83   1300 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i true 96   82   790 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 10000   7900   69000 81 270   160   9700   81 640   480   10000  
    correct results 69 2100   1600   30000 24 270   160   9700   19 640   480   10000  
        correct true 45 1300   970   18000 0 0   0   0   1 0   0   0  
        correct false 24 870   590   12000 24 270   160   9700   18 640   480   10000  
    incorrect results 1 5.1 1.9 250 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 1 5.1 1.9 250 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 137) 98
Run set sv-comp16.HeapReach