Tool ULTIMATE Kojak fd30d3d8
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-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 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/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.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 error 130   120   730 wit - -
heap-manipulation/dll_of_dll_false-unreach-call.i timeout 35   930   700 wit - -
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 17   5.2 490 wit false(reach) 9.0 4.9 390 false(reach) 18 10   380
heap-manipulation/sll_to_dll_rev_false-unreach-call.i timeout 900   860   3700 wit - -
heap-manipulation/bubble_sort_linux_true-unreach-call.i error 56   41   530 wit - -
heap-manipulation/dancing_true-unreach-call.i timeout 25   930   520 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i timeout 33   930   580 wit - -
heap-manipulation/merge_sort_true-unreach-call.i timeout 31   930   530 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i error 100   85   1500 wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) 10   3.2 330 wit false(reach) 8.0 4.5 380 false(reach) 12 6.8 340
list-properties/list_false-unreach-call.i false(reach) 22   10   610 wit false(reach) 8.3 4.7 360 false(reach) 14 7.9 340
list-properties/list_flag_false-unreach-call.i false(reach) 11   3.2 320 wit false(reach) 7.0 3.9 350 false(reach) 12 7.0 330
list-properties/list_search_false-unreach-call.i timeout 130   930   1900 wit - -
list-properties/simple_false-unreach-call.i false(reach) 11   3.4 340 wit false(reach) 8.3 4.6 350 false(reach) 11 6.1 330
list-properties/splice_false-unreach-call.i false(reach) 12   3.3 340 wit false(reach) 9.2 5.0 390 false(reach) 14 8.2 350
list-properties/alternating_list_true-unreach-call.i timeout 44   930   650 wit - -
list-properties/list_flag_true-unreach-call.i timeout 39   930   600 wit - -
list-properties/list_search_true-unreach-call.i timeout 46   930   840 wit - -
list-properties/list_true-unreach-call.i timeout 30   930   780 wit - -
list-properties/simple_built_from_end_true-unreach-call.i timeout 38   930   700 wit - -
list-properties/simple_true-unreach-call.i error 65   53   680 wit - -
list-properties/splice_true-unreach-call.i timeout 58   930   1200 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) 9.3 2.9 330 wit false(reach) 4.9 2.9 230 false(reach) 12 7.0 330
ldv-regression/alt_test.c_false-unreach-call.i false(reach) 9.9 3.1 340 wit false(reach) 9.1 5.1 390 false(reach) 12 6.8 330
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) 11   3.0 370 wit false(reach) 4.6 2.7 220 false(reach) 11 6.3 330
ldv-regression/fo_test.c_false-unreach-call.i unknown 7.2 2.2 300 wit - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 8.8 2.7 320 wit false(reach) 4.6 2.8 230 false(reach) 11 7.1 330
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 9.6 3.0 320 wit false(reach) 4.6 2.7 230 false(reach) 12 6.9 330
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) 10   3.0 350 wit false(reach) 5.5 3.3 250 false(reach) 13 7.7 360
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) 12   3.4 340 wit false(reach) 6.3 3.7 330 false(reach) 13 7.6 340
ldv-regression/rule60_list2.c_false-unreach-call_1.i timeout 32   930   520 wit - -
ldv-regression/stateful_check_false-unreach-call.i false(reach) 19   4.9 500 wit true 7.4 4.1 280 false(reach) 16 9.0 370
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 8.4 2.8 320 wit false(reach) 5.0 3.0 240 false(reach) 10 6.0 320
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 10   3.0 360 wit false(reach) 4.8 2.9 230 false(reach) 11 6.7 330
ldv-regression/alias_of_return.c_true-unreach-call.i timeout 140   930   1200 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i timeout 130   930   1300 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i timeout 130   930   1300 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i timeout 140   930   1400 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i timeout 35   930   730 wit - -
ldv-regression/just_assert.c_true-unreach-call.i timeout 130   930   1200 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 9.6 2.8 330 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 8.8 2.8 320 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i timeout 130   930   1200 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i timeout 130   930   1100 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i timeout 140   930   1200 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i timeout 130   930   1200 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i timeout 130   930   1300 wit - -
ldv-regression/nested_structure_true-unreach-call.i timeout 140   930   1400 wit - -
ldv-regression/oomInt.c_true-unreach-call.i timeout 130   930   1300 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i timeout 140   930   1200 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i timeout 33   930   580 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 11   3.3 330 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i timeout 31   930   590 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i timeout 130   930   1200 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i timeout 130   930   1300 wit - -
ldv-regression/test_address.c_true-unreach-call.i timeout 130   930   1300 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true 8.3 2.7 310 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i timeout 130   930   1100 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i timeout 130   930   1200 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i timeout 130   930   1300 wit - -
ldv-regression/test_union.c_true-unreach-call.i timeout 130   930   1200 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i timeout 130   930   1400 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i unknown 8.0 2.4 320 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i unknown 8.9 2.4 330 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i unknown 7.2 2.2 310 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i unknown 7.1 2.2 310 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i timeout 130   930   1400 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i timeout 140   930   1300 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i error 33   14   5900 wit - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i error 29   13   5200 wit - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i error 34   14   5900 wit - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i error 31   13   5800 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i error 29   13   6200 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i error 28   13   6200 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i error 27   13   6000 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i error 38   14   6100 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i error 30   14   6200 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i error 28   13   5000 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i error 28   13   6200 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i error 27   13   5900 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i error 31   14   5800 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 5600 37000 130000 81 110   61   4800   81 200   120   5500  
    correct results 20 230 72 7300 16 110   61   4800   16 200   120   5500  
        correct true 4 38 12 1300 1 0   0   0   0 0   0   0  
        correct false 16 190 61 6000 15 110   61   4800   16 200   120   5500  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 137) 24
Run set sv-comp16.HeapReach