Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .15  .15  1.8  26 .84 0   timeout 93    81    1600   790 true 8.5 4.6 190 320 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .40  .39  5.3  51 .84 0   true 5.2  2.8  72   280 true 9.7 5.2 160 330 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18  .18  1.6  26 .84 0   true 11    5.8  180   450 true 9.3 5.0 140 350 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .11  .11  .99 25 .84 0   false(unreach-call) 6.6  3.6  130   350 true 8.8 4.7 170 320 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .14  .14  1.2  25 .84 0   false(unreach-call) 9.0  5.6  180   310 true 8.8 4.7 140 350 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .11  .11  1.2  25 .84 0   true 7.3  3.9  84   290 true 9.7 5.1 110 330 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    1300 .84 0   - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 5.8 3.1 120 290
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     10000    970 .84 0   - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.3 3.3 120 290
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    920 .84 0   - - error (invalid witness file) .53 .33 12   39 error (invalid witness file) 6.3 3.3 110 310
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    860 .84 0   - - error (invalid witness file) .51 .33 13   39 error (invalid witness file) 6.1 3.2 83 310
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     9900    500 .84 0   - - error (invalid witness file) .52 .34 10   39 error (invalid witness file) 6.3 3.3 120 300
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900     900     10000    510 .84 0   - - error (invalid witness file) .56 .36 9.6 45 error (invalid witness file) 6.1 3.2 120 300
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .10  .10  1.1  24 .84 0   false(unreach-call) 5.4  3.0  81   290 true 7.7 4.1 130 320 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  1.4  24 .84 0   false(unreach-call) 5.4  3.0  100   290 true 7.6 4.1 120 320 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .095 .094 1.3  24 .84 0   false(unreach-call) 6.2  3.4  88   290 false(unreach-call) 8.4 4.5 120 360 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  1.2  24 .84 0   true 5.7  3.1  75   280 true 7.1 3.9 110 320 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .13  .13  .93 24 .84 0   true 5.3  2.9  110   290 true 15   8.1 280 420 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .10  .10  1.1  24 .84 0   false(unreach-call) 5.6  3.1  78   300 false(unreach-call) 8.4 4.5 170 350 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     9500    8900 .84 0   - - error (invalid witness file) .52 .34 14   40 error (invalid witness file) 6.1 3.2 110 290
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     9500    4100 .84 0   - - error (invalid witness file) .54 .36 4.1 41 error (invalid witness file) 5.8 3.1 110 300
list-properties/list_search_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 380     380     4200    15000 .84 0   - - error (invalid witness file) .48 .32 9.2 40 error (invalid witness file) 5.7 3.0 110 290
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     3100    380 .84 0   - - error (invalid witness file) .53 .33 13   40 error (invalid witness file) 5.8 3.1 110 300
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     12000    1800 .84 0   - - error (invalid witness file) .55 .36 9.9 40 error (invalid witness file) 5.4 2.9 110 290
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     12000    6100 .84 0   - - error (invalid witness file) .48 .30 8.7 40 error (invalid witness file) 5.8 3.1 110 290
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     12000    1100 .84 0   - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 5.7 3.1 96 300
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect .099 .099 .76 23 .99 0   false(unreach-call) 3.6  2.0  41   270 false(unreach-call) 7.2 3.9 97 330 - -
ldv-regression/alt_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .13  .13  .85 25 .84 0   false(unreach-call) 5.6  3.0  120   300 true 7.1 3.9 110 330 - -
ldv-regression/callfpointer.c_false-unreach-call.i unknown 0 wit inspect .099 .10  .65 23 .84 0   error (invalid witness file) .50 .32 11   39 error (invalid witness file) 5.9 3.1 120 300 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .083 .082 1.1  25 .84 0   false(unreach-call) 5.0  2.7  80   280 true 8.3 4.4 93 330 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .10  .10  .73 23 .84 0   false(unreach-call) 3.6  2.0  38   270 true 7.2 3.9 120 310 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect .11  .11  .71 23 .84 0   false(unreach-call) 4.2  2.4  43   270 false(unreach-call) 7.3 3.8 110 320 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect .083 .084 .84 23 .84 0   false(unreach-call) 4.7  2.6  75   280 true 7.9 4.2 130 320 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect .092 .091 1.1  24 .84 0   false(unreach-call) 4.4  2.4  71   290 false(unreach-call) 8.5 4.6 190 340 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .16  .16  1.3  24 .84 0   false(unreach-call) 6.9  3.8  79   280 true 7.9 4.2 120 330 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect .13  .13  1.2  23 .84 0   false(unreach-call) 4.7  2.5  72   280 true 8.2 4.4 160 340 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .071 .072 .92 23 .99 0   false(unreach-call) 3.7  2.0  80   270 true 6.8 3.6 110 320 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .072 .073 .81 23 .84 0   false(unreach-call) 4.4  2.5  59   290 true 6.9 3.7 110 320 - -
ldv-regression/alias_of_return.c_true-unreach-call.i timeout 0 wit inspect 900     840     12000    14000 .84 0   - - error (invalid witness file) .52 .33 7.6 40 error (invalid witness file) 5.8 3.1 110 300
ldv-regression/alias_of_return.c_true-unreach-call_1.i timeout 0 wit inspect 900     830     14000    9900 .98 0   - - error (invalid witness file) .52 .34 7.0 40 error (invalid witness file) 5.9 3.1 95 300
ldv-regression/alias_of_return_2.c_true-unreach-call.i timeout 0 wit inspect 900     860     12000    15000 .84 0   - - error (invalid witness file) .51 .32 7.8 39 error (invalid witness file) 6.6 3.5 130 320
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i timeout 0 wit inspect 900     830     12000    10000 .84 0   - - error (invalid witness file) .50 .32 7.5 41 error (invalid witness file) 5.8 3.1 120 290
ldv-regression/ex3_forlist.c_true-unreach-call.i out of memory 0 wit inspect 130     130     1900    15000 .84 0   - - error (invalid witness file) .53 .35 12   42 error (invalid witness file) 6.0 3.2 120 290
ldv-regression/just_assert.c_true-unreach-call.i timeout 0 wit inspect 900     810     12000    13000 .84 0   - - error (invalid witness file) .51 .33 6.5 41 error (invalid witness file) 6.1 3.2 120 300
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i timeout 0 wit inspect 900     850     11000    15000 .84 0   - - error (invalid witness file) .50 .32 13   42 error (invalid witness file) 6.0 3.2 120 300
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i out of memory 0 wit inspect 59     57     790    15000 .84 0   - - error (invalid witness file) .50 .31 12   39 error (invalid witness file) 5.8 3.1 110 300
ldv-regression/nested_structure.c_true-unreach-call.i timeout 0 wit inspect 900     860     12000    11000 .84 0   - - error (invalid witness file) .51 .33 13   41 error (invalid witness file) 5.9 3.1 120 300
ldv-regression/nested_structure_noptr.c_true-unreach-call.i timeout 0 wit inspect 900     830     12000    8900 .84 0   - - error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.2 3.3 120 300
ldv-regression/nested_structure_noptr_true-unreach-call.i timeout 0 wit inspect 900     840     13000    11000 .84 0   - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 5.5 3.0 110 290
ldv-regression/nested_structure_ptr.c_true-unreach-call.i timeout 0 wit inspect 900     870     13000    12000 .84 0   - - error (invalid witness file) .51 .32 8.9 42 error (invalid witness file) 6.1 3.3 130 300
ldv-regression/nested_structure_ptr_true-unreach-call.i timeout 0 wit inspect 900     870     12000    13000 .84 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.0 3.2 110 300
ldv-regression/nested_structure_true-unreach-call.i timeout 0 wit inspect 900     830     12000    11000 .84 0   - - error (invalid witness file) .49 .31 9.1 39 error (invalid witness file) 6.2 3.3 120 300
ldv-regression/oomInt.c_true-unreach-call.i out of memory 0 wit inspect 860     800     12000    15000 .84 0   - - error (invalid witness file) .48 .30 7.0 39 error (invalid witness file) 5.4 2.9 83 300
ldv-regression/oomInt.c_true-unreach-call_1.i timeout 0 wit inspect 900     830     11000    13000 .84 0   - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 5.7 3.0 120 290
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i out of memory 0 wit inspect 110     99     1500    15000 .84 0   - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.1 3.2 100 300
ldv-regression/rule60_list.c_true-unreach-call.i out of memory 0 wit inspect 120     110     1300    15000 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.4 3.4 130 300
ldv-regression/rule60_list2.c_true-unreach-call.i out of memory 0 wit inspect 120     110     1400    15000 .84 0   - - error (invalid witness file) .49 .32 4.3 40 error (invalid witness file) 6.3 3.3 120 300
ldv-regression/sizeofparameters_test.c_true-unreach-call.i timeout 0 wit inspect 900     830     10000    5100 .84 0   - - error (invalid witness file) .51 .33 11   42 error (invalid witness file) 6.2 3.3 110 310
ldv-regression/structure_assignment.c_true-unreach-call.i timeout 0 wit inspect 900     830     11000    10000 .84 0   - - error (invalid witness file) .51 .32 8.1 41 error (invalid witness file) 6.0 3.2 120 300
ldv-regression/test_address.c_true-unreach-call.i out of memory 0 wit inspect 74     67     950    15000 .84 0   - - error (invalid witness file) .51 .34 9.9 39 error (invalid witness file) 6.3 3.3 120 300
ldv-regression/test_cut_trace.c_true-unreach-call.i timeout 0 wit inspect 900     830     11000    9200 .84 0   - - error (invalid witness file) .56 .35 13   42 error (invalid witness file) 6.5 3.5 120 310
ldv-regression/test_malloc-1_true-unreach-call.i out of memory 0 wit inspect 92     85     1100    15000 .84 0   - - error (invalid witness file) .54 .35 12   40 error (invalid witness file) 6.3 3.3 120 300
ldv-regression/test_malloc-2_true-unreach-call.i out of memory 0 wit inspect 80     73     870    15000 .84 0   - - error (invalid witness file) .49 .33 14   40 error (invalid witness file) 6.2 3.3 110 300
ldv-regression/test_overflow.c_true-unreach-call.i timeout 0 wit inspect 900     830     11000    4300 .84 0   - - error (invalid witness file) .47 .31 4.2 40 error (invalid witness file) 6.0 3.2 110 300
ldv-regression/test_union.c_true-unreach-call.i out of memory 0 wit inspect 60     54     680    15000 .84 0   - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.0 3.2 110 300
ldv-regression/test_union.c_true-unreach-call_1.i out of memory 0 wit inspect 60     54     630    15000 .84 0   - - error (invalid witness file) .47 .30 11   40 error (invalid witness file) 6.0 3.2 98 300
ldv-regression/test_union_cast-1_true-unreach-call.i out of memory 0 wit inspect 74     68     840    15000 .84 0   - - error (invalid witness file) .53 .33 11   40 error (invalid witness file) 5.4 2.9 110 290
ldv-regression/test_union_cast-2_true-unreach-call.i out of memory 0 wit inspect 56     54     700    15000 .84 0   - - error (invalid witness file) .61 .38 7.7 39 error (invalid witness file) 5.9 3.2 110 300
ldv-regression/test_union_cast.c_true-unreach-call.i out of memory 0 wit inspect 56     51     620    15000 .84 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.0 3.2 110 300
ldv-regression/test_union_cast.c_true-unreach-call_1.i out of memory 0 wit inspect 72     66     850    15000 .84 0   - - error (invalid witness file) .49 .31 9.1 40 error (invalid witness file) 6.0 3.2 110 300
ldv-regression/volatile_alias.c_true-unreach-call.i timeout 0 wit inspect 900     830     12000    9500 .84 0   - - error (invalid witness file) .49 .32 8.0 39 error (invalid witness file) 5.9 3.1 130 300
ldv-regression/volatile_alias.c_true-unreach-call_1.i timeout 0 wit inspect 900     830     13000    9500 .84 0   - - error (invalid witness file) .52 .35 9.3 40 error (invalid witness file) 6.1 3.2 100 300
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .80 23 .95 0   false(unreach-call) 4.4  2.5  50   270 true 8.3 4.4 110 320 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect .27  .27  .94 23 .84 0   false(unreach-call) 4.9  2.7  59   290 true 9.3 5.0 110 320 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect .075 .074 .83 23 .84 0   false(unreach-call) 4.0  2.2  75   280 true 7.1 3.8 130 310 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect .075 .075 .75 23 .84 0   false(unreach-call) 3.5  1.9  55   280 true 7.0 3.8 140 320 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect .081 .080 .90 23 .84 0   false(unreach-call) 4.9  2.8  63   280 false(unreach-call) 7.5 4.0 170 320 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .096 .097 .98 23 .84 0   false(unreach-call) 5.2  2.9  59   280 false(unreach-call) 13   7.4 250 410 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 2.5   2.5   30    83 .84 0   true 14    8.6  170   330 false(unreach-call) 66   47   590 870 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect .52  .51  1.1  23 .84 0   false(unreach-call) 15    12    220   510 timeout 92   54   1000 7000 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect .63  .63  7.9  27 .99 0   true 4.1  2.3  73   280 false(unreach-call) 19   11   190 560 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect .073 .073 .79 23 .84 0   false(unreach-call) 3.7  2.1  80   280 true 7.0 3.7 86 310 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect .12  .12  .90 23 .84 0   false(unreach-call) 3.9  2.2  86   280 true 7.8 4.2 110 330 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect .28  .28  .80 23 .84 0   false(unreach-call) 4.0  2.2  74   270 false(unreach-call) 10   5.5 120 340 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .10  .80 23 .84 0   true 3.5  2.0  49   270 false(unreach-call) 9.3 5.0 110 350 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .69 23 .84 0   false(unreach-call) 4.0  2.2  88   270 true 6.8 3.7 130 310 - -
ldv-regression/test01_true-unreach-call.c out of memory 0 wit inspect 50     47     620    15000 .84 0   - - error (invalid witness file) .56 .36 11   43 error (invalid witness file) 5.8 3.1 120 300
ldv-regression/test03_true-unreach-call.c out of memory 0 wit inspect 57     51     620    15000 .84 0   - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.0 3.2 120 300
ldv-regression/test04_true-unreach-call.c out of memory 0 wit inspect 57     51     610    15000 .84 0   - - error (invalid witness file) .53 .34 8.8 40 error (invalid witness file) 6.5 3.4 130 300
ldv-regression/test05_true-unreach-call.c out of memory 0 wit inspect 660     630     9400    15000 .84 0   - - error (invalid witness file) .50 .34 6.4 40 error (invalid witness file) 6.0 3.2 120 290
ldv-regression/test07_true-unreach-call.c out of memory 0 wit inspect 51     49     720    15000 .84 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.9 3.1 110 300
ldv-regression/test09_true-unreach-call.c timeout 0 wit inspect 900     850     11000    7800 .84 0   - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.4 3.4 120 310
ldv-regression/test10_true-unreach-call.c timeout 0 wit inspect 900     860     11000    6700 .84 0   - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 7.0 3.7 140 310
ldv-regression/test11_true-unreach-call.c out of memory 0 wit inspect 66     60     720    15000 .84 0   - - error (invalid witness file) .48 .30 9.0 40 error (invalid witness file) 6.0 3.2 120 300
ldv-regression/test13_true-unreach-call.c out of memory 0 wit inspect 46     45     600    15000 .84 0   - - error (invalid witness file) .49 .33 6.3 39 error (invalid witness file) 5.9 3.2 110 300
ldv-regression/test14_true-unreach-call.c out of memory 0 wit inspect 63     58     720    15000 .84 0   - - error (invalid witness file) .52 .35 10   44 error (invalid witness file) 5.6 3.0 110 290
ldv-regression/test15_true-unreach-call.c out of memory 0 wit inspect 46     44     650    15000 .84 0   - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.1 3.2 120 300
ldv-regression/test16_true-unreach-call.c timeout 0 wit inspect 900     850     14000    14000 .84 0   - - error (invalid witness file) .50 .33 8.0 40 error (invalid witness file) 5.4 2.9 110 290
ldv-regression/test17_true-unreach-call.c out of memory 0 wit inspect 45     43     580    15000 .84 0   - - error (invalid witness file) .55 .35 13   44 error (invalid witness file) 6.0 3.2 130 300
ldv-regression/test18_true-unreach-call.c out of memory 0 wit inspect 540     500     7300    15000 .84 0   - - error (invalid witness file) .53 .34 13   40 error (invalid witness file) 6.0 3.2 130 300
ldv-regression/test19_true-unreach-call.c out of memory 0 wit inspect 52     50     660    15000 .84 0   - - error (invalid witness file) .56 .35 11   42 error (invalid witness file) 5.5 3.0 93 300
ldv-regression/test20_true-unreach-call.c out of memory 0 wit inspect 54     48     620    15000 .84 0   - - error (invalid witness file) .48 .31 9.4 39 error (invalid witness file) 5.8 3.1 120 310
ldv-regression/test21_true-unreach-call.c out of memory 0 wit inspect 73     69     870    15000 .84 0   - - error (invalid witness file) .51 .34 8.1 41 error (invalid witness file) 6.1 3.3 120 300
ldv-regression/test22_true-unreach-call.c timeout 0 wit inspect 900     900     10000    4100 .84 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.0 3.2 120 290
ldv-regression/test23_true-unreach-call.c out of memory 0 wit inspect 850     850     8500    15000 .84 0   - - error (invalid witness file) .54 .34 11   41 error (invalid witness file) 5.3 2.9 82 290
ldv-regression/test24_true-unreach-call.c out of memory 0 wit inspect 210     200     2200    15000 .84 0   - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 6.1 3.2 110 290
ldv-regression/test25_true-unreach-call.c timeout 0 wit inspect 900     900     11000    1400 .84 0   - - error (invalid witness file) .53 .35 9.2 43 error (invalid witness file) 6.4 3.4 120 310
ldv-regression/test26_true-unreach-call.c timeout 0 wit inspect 900     860     12000    12000 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.9 3.1 130 290
ldv-regression/test27_true-unreach-call.c timeout 0 wit inspect 900     900     7200    13000 .84 0   - - error (invalid witness file) .55 .35 8.5 40 error (invalid witness file) 6.0 3.2 120 300
ldv-regression/test28_true-unreach-call.c out of memory 0 wit inspect 76     69     850    15000 .84 0   - - error (invalid witness file) .49 .32 6.2 40 error (invalid witness file) 5.3 2.8 72 300
ldv-regression/test29_true-unreach-call.c out of memory 0 wit inspect 370     340     790    15000 .84 0   - - error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.8 3.6 120 310
ldv-regression/test30_true-unreach-call.c out of memory 0 wit inspect 770     740     8700    15000 .84 0   - - error (invalid witness file) .50 .32 9.0 40 error (invalid witness file) 5.9 3.1 110 300
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 650     650     8200    620 .84 0   true 12    6.1  120   320 true 15   7.8 170 440 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     8900    1100 .84 0   error (invalid witness file) .50 .33 12   39 error (invalid witness file) 7.3 3.8 120 320 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     9100    1400 .84 0   error (invalid witness file) .69 .43 6.9 40 error (invalid witness file) 6.3 3.3 74 310 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     12000    1400 .84 0   - - error (invalid witness file) .51 .33 14   41 error (invalid witness file) 6.5 3.4 120 310
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     12000    1400 .84 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.4 3.4 120 310
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     11000    1400 .84 0   - - error (invalid witness file) .50 .32 9.8 40 error (invalid witness file) 6.2 3.3 110 300
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     13000    1400 .84 0   - - error (invalid witness file) .54 .36 9.8 40 error (invalid witness file) 5.9 3.2 110 290
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     11000    1400 .84 0   - - error (invalid witness file) .51 .33 8.6 42 error (invalid witness file) 6.3 3.3 130 300
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     11000    1400 .84 0   - - error (invalid witness file) .48 .31 6.3 40 error (invalid witness file) 6.7 3.5 100 310
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     11000    1400 .84 0   - - error (invalid witness file) .51 .32 9.6 40 error (invalid witness file) 7.5 3.9 150 300
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     12000    1400 .84 0   - - error (invalid witness file) .51 .33 7.8 41 error (invalid witness file) 6.6 3.5 130 300
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     11000    1400 .84 0   - - error (invalid witness file) .51 .32 7.2 42 error (invalid witness file) 6.8 3.5 120 310
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     1700    670 .84 0   - - error (invalid witness file) .51 .32 8.8 40 error (invalid witness file) 6.5 3.4 120 300
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .13  .13  1.1  25 .84 0   timeout 91    81    1700   600 true 15   8.1 250 510 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .098 .097 1.1  24 .84 0   false(unreach-call) 5.1  2.8  98   280 true 10   5.4 180 360 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .093 .092 1.0  25 .84 0   false(unreach-call) 5.0  2.8  56   290 true 8.7 4.6 100 340 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20  .20  2.1  27 .86 0   true 5.5  3.0  86   280 true 8.6 4.6 87 340 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .086 .086 .90 25 .84 0   false(unreach-call) 5.6  3.0  65   280 true 9.2 5.0 160 350 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect .21  .21  2.0  36 .84 0   false(unreach-call) 6.2  3.4  110   310 error 10   5.5 160 300 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .13  .13  1.1  25 .84 0   false(unreach-call) 5.9  3.2  82   290 false(unreach-call) 9.1 4.8 180 350 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .14  .14  1.3  25 .84 0   timeout 92    84    1700   470 true 9.2 4.9 120 350 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .088 .087 .93 24 .84 0   false(unreach-call) 6.3  3.4  60   290 true 13   7.3 140 430 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .17  .17  1.7  26 .84 0   timeout 92    82    1700   470 true 11   5.8 190 390 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  1.4  25 .84 0   false(unreach-call) 7.7  4.3  94   310 true 9.2 4.9 100 330 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  .81 25 .84 0   false(unreach-call) 5.7  3.1  74   280 true 9.5 5.1 150 360 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .093 .093 1.1  25 .84 0   false(unreach-call) 5.1  2.8  83   290 true 7.6 4.0 120 320 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .14  .14  2.1  25 .84 0   true 6.7  3.6  73   280 true 8.2 4.4 120 330 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .10  .10  1.0  24 .84 0   false(unreach-call) 5.6  3.1  80   280 true 8.4 4.4 98 330 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  1.2  24 .84 0   false(unreach-call) 6.4  3.5  97   290 error 11   6.1 180 300 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .13  .13  1.1  24 .84 0   false(unreach-call) 4.9  2.6  61   280 false(unreach-call) 8.8 4.7 140 340 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .10  .10  1.3  25 .84 0   true 7.0  3.8  78   290 true 11   5.6 160 350 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .087 .086 .96 24 .84 0   false(unreach-call) 6.3  3.4  70   290 false(unreach-call) 8.9 4.8 160 350 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     9800    2900 .84 0   - - error (invalid witness file) .54 .36 9.0 40 error (invalid witness file) 6.2 3.2 110 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    1100 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.3 3.4 120 310
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     9800    4100 .84 0   - - error (invalid witness file) .51 .32 9.1 39 error (invalid witness file) 6.2 3.3 130 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 840     840     8000    15000 .84 0   - - error (invalid witness file) .48 .31 3.9 40 error (invalid witness file) 6.0 3.2 130 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    480 .84 0   - - error (invalid witness file) .48 .31 12   39 error (invalid witness file) 6.3 3.3 120 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    560 .84 0   - - error (invalid witness file) .50 .32 13   41 error (invalid witness file) 5.9 3.1 76 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     13000    440 .84 0   - - error (invalid witness file) .49 .32 14   40 error (invalid witness file) 7.1 3.7 130 310
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     9700    580 .84 0   - - error (invalid witness file) .49 .31 9.9 40 error (invalid witness file) 6.7 3.5 130 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     1800    200 .84 0   - - error (invalid witness file) .50 .32 6.9 40 error (invalid witness file) 5.8 3.1 100 290
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    2800 .84 0   - - error (invalid witness file) .49 .31 13   39 error (invalid witness file) 5.7 3.1 100 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    3500 .84 0   - - error (invalid witness file) .51 .33 9.0 41 error (invalid witness file) 6.4 3.4 120 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    190 .84 0   - - error (invalid witness file) .51 .33 10   42 error (invalid witness file) 6.3 3.3 120 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    1200 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.0 3.2 90 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     9900    4700 .84 0   - - error (invalid witness file) .55 .35 13   43 error (invalid witness file) 6.3 3.3 130 310
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 540     540     4500    15000 .92 0   - - error (invalid witness file) .53 .34 3.7 40 error (invalid witness file) 6.3 3.3 120 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    510 .84 0   - - error (invalid witness file) .51 .32 8.4 39 error (invalid witness file) 5.6 3.1 120 290
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    440 .84 0   - - error (invalid witness file) .48 .32 9.4 39 error (invalid witness file) 6.8 3.6 120 320
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     5700    360 .84 0   - - error (invalid witness file) .48 .31 8.6 39 error (invalid witness file) 6.1 3.2 130 300
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     12000    890 .84 0   - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 5.5 3.0 120 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     2500    320 .84 0   - - error (invalid witness file) .52 .33 11   42 error (invalid witness file) 5.7 3.0 120 290
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    3800 .84 0   - - error (invalid witness file) .51 .33 13   41 error (invalid witness file) 6.3 3.3 110 300
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .11  .11  .96 24 .84 0   false(unreach-call) 5.1  2.8  120   280 true 8.5 4.5 99 330 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 2.5   2.5   32    96 .99 0   timeout 96    77    1300   2400 timeout 97   78   1000 1100 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .086 .087 1.1  24 .84 0   false(unreach-call) 5.3  2.9  87   280 false(unreach-call) 8.2 4.4 130 360 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i false(unreach-call) 1 wit inspect .20  .20  2.2  29 .84 0   false(unreach-call) 6.3  3.5  130   330 true 8.4 4.5 130 320 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i timeout 0 wit inspect 900     900     11000    1700 .84 0   - - error (invalid witness file) .53 .35 9.2 39 error (invalid witness file) 7.0 3.7 150 310
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect .14  .14  1.3  25 .99 0   true 8.1  4.4  110   350 true 13   7.3 200 420 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i timeout 0 wit inspect 900     900     9300    6300 .84 0   - - error (invalid witness file) .51 .34 8.6 41 error (invalid witness file) 6.3 3.3 120 300
list-ext2-properties/simple_search_value_false-unreach-call.i false(unreach-call) 1 wit inspect .18  .17  2.3  28 .84 0   false(unreach-call) 10    6.2  120   430 timeout 97   85   1200 890 - -
list-ext2-properties/simple_search_value_true-unreach-call.i timeout 0 wit inspect 900     900     8100    12000 .84 0   - - error (invalid witness file) .51 .33 7.6 40 error (invalid witness file) 6.3 3.3 130 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 173 63 73000 72000 850000 910000 150 0   173 810 600 13000 22000 173 920 570 12000 31000 173 55 35 1100 4300   173 650 350 12000 32000  
    correct results 63 63 670 670 8300 2300 54 0   58 810 600 13000 22000 58 900 560 12000 30000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 63 63 670 670 8300 2300 54 0   45 810 600 13000 22000 15 900 560 12000 30000 0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (173 tasks, max score: 280) 63
Run set sv-comp17.ReachSafety-Heap