Tool ULTIMATE Automizer cfb9fd9e
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-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 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/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.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 44   29   580 wit - -
heap-manipulation/dll_of_dll_false-unreach-call.i error 65   54   420 wit - -
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 18   7.4 450 wit false(reach) 9.4 5.1 380 false(reach) 18 9.9 370
heap-manipulation/sll_to_dll_rev_false-unreach-call.i error 30   20   540 wit - -
heap-manipulation/bubble_sort_linux_true-unreach-call.i error 34   20   750 wit - -
heap-manipulation/dancing_true-unreach-call.i error 20   9.2 420 wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i error 67   57   440 wit - -
heap-manipulation/merge_sort_true-unreach-call.i error 50   32   1200 wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i error 20   9.9 520 wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) 10   3.1 330 wit false(reach) 9.6 5.3 390 false(reach) 13 8.4 340
list-properties/list_false-unreach-call.i false(reach) 33   18   650 wit false(reach) 8.9 5.1 370 false(reach) 14 8.3 340
list-properties/list_flag_false-unreach-call.i false(reach) 12   3.6 340 wit false(reach) 7.8 4.3 360 false(reach) 12 6.9 330
list-properties/list_search_false-unreach-call.i error 80   67   620 wit - -
list-properties/simple_false-unreach-call.i false(reach) 13   4.2 350 wit false(reach) 8.2 4.6 350 false(reach) 13 7.3 330
list-properties/splice_false-unreach-call.i false(reach) 11   3.5 350 wit false(reach) 9.7 5.5 400 false(reach) 15 8.5 360
list-properties/alternating_list_true-unreach-call.i error 51   36   690 wit - -
list-properties/list_flag_true-unreach-call.i error 61   45   970 wit - -
list-properties/list_search_true-unreach-call.i error 150   130   720 wit - -
list-properties/list_true-unreach-call.i error 75   56   1000 wit - -
list-properties/simple_built_from_end_true-unreach-call.i error 210   190   1300 wit - -
list-properties/simple_true-unreach-call.i error 44   32   640 wit - -
list-properties/splice_true-unreach-call.i error 57   43   710 wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) 11   3.4 320 wit false(reach) 5.0 2.9 230 false(reach) 11 6.4 330
ldv-regression/alt_test.c_false-unreach-call.i false(reach) 10   3.3 330 wit false(reach) 9.6 5.3 380 false(reach) 13 7.8 320
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) 9.4 2.8 340 wit false(reach) 4.1 2.4 230 false(reach) 12 7.5 330
ldv-regression/fo_test.c_false-unreach-call.i unknown 8.9 4.2 320 wit - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 9.4 3.1 320 wit false(reach) 4.2 2.4 230 false(reach) 12 7.5 320
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 9.0 3.1 330 wit false(reach) 4.0 2.4 220 false(reach) 11 7.7 320
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) 9.4 2.9 330 wit false(reach) 5.8 3.3 330 false(reach) 12 6.8 340
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) 9.7 3.4 330 wit false(reach) 7.1 4.1 340 false(reach) 13 7.5 340
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(reach) 21   8.9 450 wit false(reach) 7.5 4.2 360 false(reach) 14 8.0 350
ldv-regression/stateful_check_false-unreach-call.i false(reach) 12   4.3 350 wit true 7.8 4.4 290 false(reach) 17 9.2 380
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 9.4 3.1 330 wit false(reach) 4.9 2.9 240 false(reach) 12 7.2 330
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 8.5 2.7 340 wit false(reach) 5.0 2.9 230 false(reach) 13 7.5 330
ldv-regression/alias_of_return.c_true-unreach-call.i true 9.4 3.3 340 wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 9.4 2.7 340 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 10   3.5 330 wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 11   3.2 380 wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i true 26   11   610 wit - -
ldv-regression/just_assert.c_true-unreach-call.i true 8.4 2.5 340 wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 9.8 3.0 330 wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 9.9 3.1 320 wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true 10   3.2 340 wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 9.7 2.9 340 wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true 8.9 2.7 330 wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 13   5.4 380 wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true 14   4.1 360 wit - -
ldv-regression/nested_structure_true-unreach-call.i true 12   3.4 350 wit - -
ldv-regression/oomInt.c_true-unreach-call.i true 9.7 3.3 320 wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true 9.3 3.0 330 wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 11   3.6 360 wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true 14   4.7 360 wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true 21   8.8 510 wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 9.1 2.8 330 wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true 8.5 2.7 320 wit - -
ldv-regression/test_address.c_true-unreach-call.i true 8.8 3.3 320 wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true 9.6 3.4 340 wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true 9.7 3.0 330 wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true 9.2 3.3 330 wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true 8.7 2.7 330 wit - -
ldv-regression/test_union.c_true-unreach-call.i true 8.1 2.6 330 wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true 8.4 2.7 320 wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i unknown 8.5 3.4 320 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i unknown 8.0 2.5 310 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i unknown 8.3 3.7 310 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i unknown 8.2 2.6 310 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true 8.7 3.0 330 wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 8.5 2.9 330 wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i timeout 900   880   1100 wit - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i timeout 900   880   1100 wit - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i timeout 900   880   880 wit - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i true 14   3.8 410 wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i true 14   4.0 400 wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i true 15   5.1 330 wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i true 15   3.8 360 wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i true 14   3.9 360 wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i true 13   3.8 340 wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i true 13   4.4 330 wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i true 13   4.2 380 wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i true 14   4.1 340 wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i true 12   4.1 330 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 4500 3700 37000 81 120   67   5300   81 230   130   5700  
    correct results 57 680 230 20000 17 120   67   5300   17 230   130   5700  
        correct true 40 460 150 14000 1 0   0   0   0 0   0   0  
        correct false 17 220 81 6200 16 120   67   5300   17 230   130   5700  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 137) 97
Run set sv-comp16.HeapReach