Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
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-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 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/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.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 out of memory 100      100     15000   wit - -
heap-manipulation/dll_of_dll_false-unreach-call.i out of memory 620      620     15000   wit - -
heap-manipulation/merge_sort_false-unreach-call.i unknown 900      900     12000   wit - -
heap-manipulation/sll_to_dll_rev_false-unreach-call.i out of memory 570      570     15000   wit - -
heap-manipulation/bubble_sort_linux_true-unreach-call.i out of memory 100      100     15000   wit - -
heap-manipulation/dancing_true-unreach-call.i true 26      26     3500   wit - -
heap-manipulation/dll_of_dll_true-unreach-call.i out of memory 640      630     15000   wit - -
heap-manipulation/merge_sort_true-unreach-call.i unknown 900      900     12000   wit - -
heap-manipulation/sll_to_dll_rev_true-unreach-call.i out of memory 550      550     15000   wit - -
list-properties/alternating_list_false-unreach-call.i false(reach) 230      120     3900   wit false(reach) 22   12   520 true 11   7.6 330
list-properties/list_false-unreach-call.i unknown 900      900     2800   wit - -
list-properties/list_flag_false-unreach-call.i false(reach) 180      100     1500   wit false(reach) 8.7 5.0 360 true 12   8.4 330
list-properties/list_search_false-unreach-call.i false(reach) 180      100     2700   wit false(reach) 9.6 5.2 380 true 11   6.0 330
list-properties/simple_false-unreach-call.i error (1) 150      99     1300   wit - -
list-properties/splice_false-unreach-call.i unknown 890      900     1600   wit - -
list-properties/alternating_list_true-unreach-call.i true 3.2    3.2   320   wit - -
list-properties/list_flag_true-unreach-call.i true 16      16     1000   wit - -
list-properties/list_search_true-unreach-call.i true .25   .26  27   wit - -
list-properties/list_true-unreach-call.i unknown 900      900     2800   wit - -
list-properties/simple_built_from_end_true-unreach-call.i true 19      19     1400   wit - -
list-properties/simple_true-unreach-call.i error (1) 150      110     1200   wit - -
list-properties/splice_true-unreach-call.i unknown 890      900     1600   wit - -
ldv-regression/1_3.c_false-unreach-call.i false(reach) 49      20     1000   wit false(reach) 5.1 2.9 240 true 10   6.4 320
ldv-regression/alt_test.c_false-unreach-call.i false(reach) 16      14     390   wit false(reach) 9.2 5.1 390 true 11   6.2 350
ldv-regression/callfpointer.c_false-unreach-call.i unknown .037  .043 3.8 wit - -
ldv-regression/fo_test.c_false-unreach-call.i witness unconfirmed 19      13     500   wit unknown 6.5 3.7 250 unknown 9.2 5.7 300
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 11      10     440   wit false(reach) 4.7 2.9 220 true 12   7.1 340
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 11      10     460   wit false(reach) 4.9 2.9 230 true 11   6.2 340
ldv-regression/recursive_list.c_false-unreach-call.i witness timeout 9.5    10     340   wit timeout 91   73   2700 true 12   6.7 360
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) 29      20     1500   wit false(reach) 6.8 3.9 330 true 11   7.5 320
ldv-regression/rule60_list2.c_false-unreach-call_1.i witness invalid (exception) 6.1    12     220   wit exception 5.7 3.2 240 true 11   6.5 340
ldv-regression/stateful_check_false-unreach-call.i false(reach) 13      12     370   wit false(reach) 31   16   800 true 12   8.3 330
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 4.6    10     230   wit false(reach) 6.2 3.7 320 true 10   6.4 310
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 4.3    10     230   wit false(reach) 5.1 3.0 230 true 11   6.3 330
ldv-regression/alias_of_return.c_true-unreach-call.i true .065  .078 13   wit - -
ldv-regression/alias_of_return.c_true-unreach-call_1.i true .063  .076 13   wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call.i true .064  .077 13   wit - -
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true .062  .070 13   wit - -
ldv-regression/ex3_forlist.c_true-unreach-call.i true .097  .11  13   wit - -
ldv-regression/just_assert.c_true-unreach-call.i true .071  .080 13   wit - -
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true .071  .084 13   wit - -
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true .091  .10  13   wit - -
ldv-regression/nested_structure.c_true-unreach-call.i true .066  .075 13   wit - -
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true .099  .11  13   wit - -
ldv-regression/nested_structure_noptr_true-unreach-call.i true .071  .081 13   wit - -
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true .062  .072 13   wit - -
ldv-regression/nested_structure_ptr_true-unreach-call.i true .096  .11  13   wit - -
ldv-regression/nested_structure_true-unreach-call.i true .066  .079 13   wit - -
ldv-regression/oomInt.c_true-unreach-call.i true .060  .072 13   wit - -
ldv-regression/oomInt.c_true-unreach-call_1.i true .071  .080 13   wit - -
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true .089  .10  14   wit - -
ldv-regression/rule60_list.c_true-unreach-call.i true .090  .10  18   wit - -
ldv-regression/rule60_list2.c_true-unreach-call.i true .12   .13  18   wit - -
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true .13   .14  17   wit - -
ldv-regression/structure_assignment.c_true-unreach-call.i true .060  .072 13   wit - -
ldv-regression/test_address.c_true-unreach-call.i true .096  .11  18   wit - -
ldv-regression/test_cut_trace.c_true-unreach-call.i true .069  .081 13   wit - -
ldv-regression/test_malloc-1_true-unreach-call.i true .13   .15  18   wit - -
ldv-regression/test_malloc-2_true-unreach-call.i true .11   .12  18   wit - -
ldv-regression/test_overflow.c_true-unreach-call.i true .076  .087 22   wit - -
ldv-regression/test_union.c_true-unreach-call.i true .094  .11  13   wit - -
ldv-regression/test_union.c_true-unreach-call_1.i true .095  .11  13   wit - -
ldv-regression/test_union_cast-1_true-unreach-call.i unknown .020  .034 3.0 wit - -
ldv-regression/test_union_cast-2_true-unreach-call.i unknown .012  .022 2.9 wit - -
ldv-regression/test_union_cast.c_true-unreach-call.i unknown .0094 .018 2.8 wit - -
ldv-regression/test_union_cast.c_true-unreach-call_1.i unknown .014  .026 3.1 wit - -
ldv-regression/volatile_alias.c_true-unreach-call.i true .059  .070 13   wit - -
ldv-regression/volatile_alias.c_true-unreach-call_1.i true .063  .072 13   wit - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i out of memory 140      140     15000   wit - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i out of memory 140      140     15000   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 11000 10000 340000 81 220   140   7300   81 150   95   4600  
    correct results 46 790 500 19000 11 110   63   4000   11 120   76   3600  
        correct true 35 67 67 6700 0 0   0   0   11 0   0   0  
        correct false 11 720 430 13000 11 110   63   4000   0 120   76   3600  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (81 tasks, max score: 137) 81
Run set sv-comp16.HeapReach