Tool SeaHorn-F16 0.1.0
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-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]]
Run set sv-comp16.HeapReach
Options --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.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 .54 .32 55
heap-manipulation/dll_of_dll_false-unreach-call.i .25 .15 28 92   60   2600 11   6.3 320
heap-manipulation/merge_sort_false-unreach-call.i .85 .45 84 10   5.5 400 13   7.8 330
heap-manipulation/sll_to_dll_rev_false-unreach-call.i .65 .36 80 12   6.4 430 14   8.5 340
heap-manipulation/bubble_sort_linux_true-unreach-call.i .59 .37 55
heap-manipulation/dancing_true-unreach-call.i .74 .40 52
heap-manipulation/dll_of_dll_true-unreach-call.i .25 .15 28
heap-manipulation/merge_sort_true-unreach-call.i .87 .46 85
heap-manipulation/sll_to_dll_rev_true-unreach-call.i .68 .37 81
list-properties/alternating_list_false-unreach-call.i .36 .21 43 10   5.5 400 13   7.8 350
list-properties/list_false-unreach-call.i .52 .29 52 91   82   760 11   8.4 320
list-properties/list_flag_false-unreach-call.i .39 .24 46 9.0 5.0 360 13   8.8 340
list-properties/list_search_false-unreach-call.i .43 .25 40 8.8 4.8 370 12   7.2 340
list-properties/simple_false-unreach-call.i .37 .23 42 9.0 5.1 370 11   6.5 330
list-properties/splice_false-unreach-call.i .56 .30 55 9.3 5.2 370 11   7.5 320
list-properties/alternating_list_true-unreach-call.i .44 .24 43
list-properties/list_flag_true-unreach-call.i .49 .26 48
list-properties/list_search_true-unreach-call.i .37 .23 38
list-properties/list_true-unreach-call.i .49 .28 53
list-properties/simple_built_from_end_true-unreach-call.i .32 .19 44
list-properties/simple_true-unreach-call.i .33 .20 42
list-properties/splice_true-unreach-call.i .85 .46 61
ldv-regression/1_3.c_false-unreach-call.i .23 .15 35 8.9 5.0 290 11   6.4 320
ldv-regression/alt_test.c_false-unreach-call.i .23 .14 35 23   12   660 11   6.3 330
ldv-regression/callfpointer.c_false-unreach-call.i .19 .12 34 5.2 3.0 230 11   6.4 330
ldv-regression/fo_test.c_false-unreach-call.i .25 .14 35 19   9.9 630 9.9 6.1 310
ldv-regression/mutex_lock_int.c_false-unreach-call.i .23 .15 35 5.8 3.3 240 11   6.0 340
ldv-regression/mutex_lock_struct.c_false-unreach-call.i .23 .15 35 5.2 3.0 230 11   6.4 330
ldv-regression/recursive_list.c_false-unreach-call.i .22 .13 35 8.9 4.9 310 11   6.5 330
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i .34 .21 40 6.6 3.8 330 11   6.6 340
ldv-regression/rule60_list2.c_false-unreach-call_1.i .26 .17 40 9.2 5.1 380 10   6.3 320
ldv-regression/stateful_check_false-unreach-call.i .47 .26 44 16   8.5 500 13   8.3 340
ldv-regression/test_while_int.c_false-unreach-call.i .24 .15 34 15   8.3 520 11   6.6 310
ldv-regression/test_while_int.c_false-unreach-call_1.i .22 .13 35 7.8 4.3 280 9.2 5.6 310
ldv-regression/alias_of_return.c_true-unreach-call.i .19 .12 29
ldv-regression/alias_of_return.c_true-unreach-call_1.i .19 .13 29
ldv-regression/alias_of_return_2.c_true-unreach-call.i .19 .13 24
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i .25 .16 29
ldv-regression/ex3_forlist.c_true-unreach-call.i .34 .20 43
ldv-regression/just_assert.c_true-unreach-call.i .21 .14 29
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i .18 .12 29
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i .16 .11 29
ldv-regression/nested_structure.c_true-unreach-call.i .18 .12 29
ldv-regression/nested_structure_noptr.c_true-unreach-call.i .17 .11 29
ldv-regression/nested_structure_noptr_true-unreach-call.i .25 .16 29
ldv-regression/nested_structure_ptr.c_true-unreach-call.i .20 .12 29
ldv-regression/nested_structure_ptr_true-unreach-call.i .18 .12 29
ldv-regression/nested_structure_true-unreach-call.i .18 .12 29
ldv-regression/oomInt.c_true-unreach-call.i .24 .16 27
ldv-regression/oomInt.c_true-unreach-call_1.i .20 .13 29
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i .31 .19 38
ldv-regression/rule60_list.c_true-unreach-call.i .21 .13 29
ldv-regression/rule60_list2.c_true-unreach-call.i .30 .19 37
ldv-regression/sizeofparameters_test.c_true-unreach-call.i .18 .12 30
ldv-regression/structure_assignment.c_true-unreach-call.i .25 .16 29
ldv-regression/test_address.c_true-unreach-call.i .23 .15 29
ldv-regression/test_cut_trace.c_true-unreach-call.i .17 .12 24
ldv-regression/test_malloc-1_true-unreach-call.i .15 .10 29
ldv-regression/test_malloc-2_true-unreach-call.i .21 .14 29
ldv-regression/test_overflow.c_true-unreach-call.i .22 .14 29
ldv-regression/test_union.c_true-unreach-call.i .24 .15 29
ldv-regression/test_union.c_true-unreach-call_1.i .20 .13 29
ldv-regression/test_union_cast-1_true-unreach-call.i .21 .14 29
ldv-regression/test_union_cast-2_true-unreach-call.i .21 .13 29
ldv-regression/test_union_cast.c_true-unreach-call.i .19 .12 27
ldv-regression/test_union_cast.c_true-unreach-call_1.i .18 .12 29
ldv-regression/volatile_alias.c_true-unreach-call.i .28 .18 31
ldv-regression/volatile_alias.c_true-unreach-call_1.i .21 .14 29
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i .60 .32 37
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i .59 .34 36
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i .59 .34 36
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i .58 .32 33
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i .52 .30 33
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i .51 .29 33
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i .49 .27 33
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i .48 .27 33
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i .64 .35 33
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i .42 .25 33
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i .50 .29 33
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i .54 .31 33
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i .51 .29 33
../../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 29   17    3000 81 380   250   11000   81 240   150   6900  
    correct results 54 17   10    1800 10 100   55   3900   10 120   75   3300  
        correct true 44 12   7.7  1300 0 0   0   0   10 0   0   0  
        correct false 10 4.7 2.7  510 10 100   55   3900   0 120   75   3300  
    incorrect results 14 7.6 4.2  690 0 0   0   0   0 0   0   0  
        incorrect true 3 1.8 1.0  110 0 0   0   0   0 0   0   0  
        incorrect false 11 5.8 3.2  580 0 0   0   0   0 0   0   0  
score (81 tasks, max score: 137) -174
Run set sv-comp16.HeapReach