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 130   120   730
heap-manipulation/dll_of_dll_false-unreach-call.i 35   930   700
heap-manipulation/merge_sort_false-unreach-call.i 17   5.2 490 9.0 4.9 390 18 10   380
heap-manipulation/sll_to_dll_rev_false-unreach-call.i 900   860   3700
heap-manipulation/bubble_sort_linux_true-unreach-call.i 56   41   530
heap-manipulation/dancing_true-unreach-call.i 25   930   520
heap-manipulation/dll_of_dll_true-unreach-call.i 33   930   580
heap-manipulation/merge_sort_true-unreach-call.i 31   930   530
heap-manipulation/sll_to_dll_rev_true-unreach-call.i 100   85   1500
list-properties/alternating_list_false-unreach-call.i 10   3.2 330 8.0 4.5 380 12 6.8 340
list-properties/list_false-unreach-call.i 22   10   610 8.3 4.7 360 14 7.9 340
list-properties/list_flag_false-unreach-call.i 11   3.2 320 7.0 3.9 350 12 7.0 330
list-properties/list_search_false-unreach-call.i 130   930   1900
list-properties/simple_false-unreach-call.i 11   3.4 340 8.3 4.6 350 11 6.1 330
list-properties/splice_false-unreach-call.i 12   3.3 340 9.2 5.0 390 14 8.2 350
list-properties/alternating_list_true-unreach-call.i 44   930   650
list-properties/list_flag_true-unreach-call.i 39   930   600
list-properties/list_search_true-unreach-call.i 46   930   840
list-properties/list_true-unreach-call.i 30   930   780
list-properties/simple_built_from_end_true-unreach-call.i 38   930   700
list-properties/simple_true-unreach-call.i 65   53   680
list-properties/splice_true-unreach-call.i 58   930   1200
ldv-regression/1_3.c_false-unreach-call.i 9.3 2.9 330 4.9 2.9 230 12 7.0 330
ldv-regression/alt_test.c_false-unreach-call.i 9.9 3.1 340 9.1 5.1 390 12 6.8 330
ldv-regression/callfpointer.c_false-unreach-call.i 11   3.0 370 4.6 2.7 220 11 6.3 330
ldv-regression/fo_test.c_false-unreach-call.i 7.2 2.2 300
ldv-regression/mutex_lock_int.c_false-unreach-call.i 8.8 2.7 320 4.6 2.8 230 11 7.1 330
ldv-regression/mutex_lock_struct.c_false-unreach-call.i 9.6 3.0 320 4.6 2.7 230 12 6.9 330
ldv-regression/recursive_list.c_false-unreach-call.i 10   3.0 350 5.5 3.3 250 13 7.7 360
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i 12   3.4 340 6.3 3.7 330 13 7.6 340
ldv-regression/rule60_list2.c_false-unreach-call_1.i 32   930   520
ldv-regression/stateful_check_false-unreach-call.i 19   4.9 500 7.4 4.1 280 16 9.0 370
ldv-regression/test_while_int.c_false-unreach-call.i 8.4 2.8 320 5.0 3.0 240 10 6.0 320
ldv-regression/test_while_int.c_false-unreach-call_1.i 10   3.0 360 4.8 2.9 230 11 6.7 330
ldv-regression/alias_of_return.c_true-unreach-call.i 140   930   1200
ldv-regression/alias_of_return.c_true-unreach-call_1.i 130   930   1300
ldv-regression/alias_of_return_2.c_true-unreach-call.i 130   930   1300
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i 140   930   1400
ldv-regression/ex3_forlist.c_true-unreach-call.i 35   930   730
ldv-regression/just_assert.c_true-unreach-call.i 130   930   1200
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i 9.6 2.8 330
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i 8.8 2.8 320
ldv-regression/nested_structure.c_true-unreach-call.i 130   930   1200
ldv-regression/nested_structure_noptr.c_true-unreach-call.i 130   930   1100
ldv-regression/nested_structure_noptr_true-unreach-call.i 140   930   1200
ldv-regression/nested_structure_ptr.c_true-unreach-call.i 130   930   1200
ldv-regression/nested_structure_ptr_true-unreach-call.i 130   930   1300
ldv-regression/nested_structure_true-unreach-call.i 140   930   1400
ldv-regression/oomInt.c_true-unreach-call.i 130   930   1300
ldv-regression/oomInt.c_true-unreach-call_1.i 140   930   1200
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i 33   930   580
ldv-regression/rule60_list.c_true-unreach-call.i 11   3.3 330
ldv-regression/rule60_list2.c_true-unreach-call.i 31   930   590
ldv-regression/sizeofparameters_test.c_true-unreach-call.i 130   930   1200
ldv-regression/structure_assignment.c_true-unreach-call.i 130   930   1300
ldv-regression/test_address.c_true-unreach-call.i 130   930   1300
ldv-regression/test_cut_trace.c_true-unreach-call.i 8.3 2.7 310
ldv-regression/test_malloc-1_true-unreach-call.i 130   930   1100
ldv-regression/test_malloc-2_true-unreach-call.i 130   930   1200
ldv-regression/test_overflow.c_true-unreach-call.i 130   930   1300
ldv-regression/test_union.c_true-unreach-call.i 130   930   1200
ldv-regression/test_union.c_true-unreach-call_1.i 130   930   1400
ldv-regression/test_union_cast-1_true-unreach-call.i 8.0 2.4 320
ldv-regression/test_union_cast-2_true-unreach-call.i 8.9 2.4 330
ldv-regression/test_union_cast.c_true-unreach-call.i 7.2 2.2 310
ldv-regression/test_union_cast.c_true-unreach-call_1.i 7.1 2.2 310
ldv-regression/volatile_alias.c_true-unreach-call.i 130   930   1400
ldv-regression/volatile_alias.c_true-unreach-call_1.i 140   930   1300
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i 33   14   5900
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i 29   13   5200
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i 34   14   5900
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i 31   13   5800
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i 29   13   6200
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i 28   13   6200
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i 27   13   6000
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i 38   14   6100
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i 30   14   6200
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i 28   13   5000
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i 28   13   6200
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i 27   13   5900
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i 31   14   5800
../../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