Tool CBMC 5.6
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-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-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.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 error (1) 0 wit inspect .24 .24  2.4  21 .0082 0      error (invalid witness file) .58 .38 9.6 43 error (invalid witness file) 6.7 3.5 100 300 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .39 .38  4.4  30 .0082 0      true 7.4  4.0  150   290 true 9.6 5.2 180 340 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .62 .61  6.7  44 .0082 0      false(unreach-call) 6.5  3.5  150   340 false(unreach-call) 12   6.2 190 380 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .36 .35  4.0  30 .0082 0      false(unreach-call) 7.3  4.0  110   300 false(unreach-call) 15   8.1 150 400 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .36 .35  4.1  31 .0082 0      false(unreach-call) 5.5  3.0  92   290 false(unreach-call) 14   7.6 130 360 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .36 .35  4.8  32 .0082 0      false(unreach-call) 6.9  3.7  100   300 false(unreach-call) 12   6.2 210 380 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (1) 0 wit inspect .22 .22  2.9  21 .0082 0      - - error (invalid witness file) .51 .32 9.7 40 error (invalid witness file) 6.5 3.4 120 310
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     11000    930 2.4    .11   - - error (invalid witness file) .55 .34 12   41 error (invalid witness file) 5.6 3.0 130 290
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     8300    1900 6.0    .0041 - - error (invalid witness file) .52 .35 8.9 39 error (invalid witness file) 8.1 4.2 100 320
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect 290    290     2700    12000 3.0    0      - - error (invalid witness file) .54 .36 13   43 error (invalid witness file) 6.8 3.6 90 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     4600    7300 2.7    0      - - error (invalid witness file) .54 .34 10   41 error (invalid witness file) 5.8 3.1 89 290
heap-manipulation/tree_true-unreach-call.i error (42) 0 wit inspect 850    850     7600    7900 9.4    0      - - error (invalid witness file) .56 .36 9.8 39 error (invalid witness file) 5.5 2.9 110 290
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20 .19  2.1  20 .0082 0      false(unreach-call) 5.8  3.1  120   290 false(unreach-call) 10   5.3 120 320 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .24 .24  2.6  23 .0082 0      false(unreach-call) 5.5  3.0  93   280 false(unreach-call) 8.0 4.3 130 320 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 .21  1.6  20 .0082 0      false(unreach-call) 5.3  2.9  94   290 false(unreach-call) 8.1 4.3 130 330 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .52 .51  4.8  20 .061  0      false(unreach-call) 5.8  3.2  80   310 false(unreach-call) 21   12   500 630 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .22 .21  1.8  20 .0082 0      false(unreach-call) 5.4  2.9  85   290 false(unreach-call) 8.7 4.7 130 330 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 .20  2.1  22 .0082 0      false(unreach-call) 6.6  3.6  95   290 false(unreach-call) 8.4 4.5 170 330 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     5600    3600 1.7    0      - - error (invalid witness file) .58 .36 9.9 43 error (invalid witness file) 6.1 3.2 130 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     4100    3400 1.2    0      - - error (invalid witness file) .61 .39 7.8 40 error (invalid witness file) 5.7 3.0 80 300
list-properties/list_search_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .70 .69  6.9  21 .082  0      - - exception 5.9  3.2  71   270 true 43   29   710 870
list-properties/list_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     6700    6200 1.1    0      - - error (invalid witness file) .55 .35 11   42 error (invalid witness file) 6.4 3.4 120 310
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (1) 0 wit inspect 74    74     810    1300 3.9    0      - - error (invalid witness file) .54 .35 11   41 error (invalid witness file) 5.9 3.1 84 300
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (1) 0 wit inspect 260    260     2300    3300 8.2    .0041 - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.0 3.2 84 290
list-properties/splice_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect 670    670     7200    13000 2.0    0      - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.7 3.5 100 320
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect .17 .16  1.7  18 .0082 0      assertion 3.4  1.9  74   270 false(unreach-call) 9.5 5.0 110 320 - -
ldv-regression/alt_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .20 .19  1.6  21 .0082 0      true 5.4  2.9  110   280 false(unreach-call) 9.5 5.1 180 350 - -
ldv-regression/callfpointer.c_false-unreach-call.i false(unreach-call) 1 wit inspect .10 .093 .89 17 0      0      false(unreach-call) 3.6  2.0  68   280 false(unreach-call) 8.6 4.6 120 330 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .26 .30  1.8  33 .0082 13      false(unreach-call) 5.3  2.9  99   280 unknown 15   8.2 300 350 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .11 .10  .95 17 0      0      true 3.4  1.9  59   270 false(unreach-call) 8.2 4.4 87 310 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect .12 .11  .86 17 0      0      true 4.2  2.3  59   270 false(unreach-call) 8.0 4.2 150 330 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect .18 .17  1.8  18 .0082 0      false(unreach-call) 4.0  2.2  35   280 false(unreach-call) 8.5 4.5 150 320 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect .12 .12  .99 18 0      0      false(unreach-call) 4.7  2.6  84   290 false(unreach-call) 9.5 5.1 120 340 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .15 .14  .95 19 0      0      false(unreach-call) 5.6  3.0  95   290 false(unreach-call) 15   8.1 140 390 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect .27 .26  3.4  21 .020  0      false(unreach-call) 5.0  2.8  100   280 false(unreach-call) 18   9.9 220 810 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .27 .26  2.1  17 .012  0      false(unreach-call) 3.8  2.1  52   270 false(unreach-call) 9.3 4.9 110 320 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .27 .26  2.2  17 .0082 0      false(unreach-call) 3.7  2.1  47   270 false(unreach-call) 7.8 4.2 160 330 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect .19 .19  1.5  17 0      0      - - true 4.3  2.4  47   260 true 7.5 4.1 160 310
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect .18 .17  1.5  17 0      0      - - true 4.1  2.3  51   260 true 7.2 3.9 150 310
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect .19 .18  1.4  17 0      0      - - true 3.4  1.9  57   260 true 8.0 4.3 150 320
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect .18 .17  1.6  17 0      0      - - true 4.3  2.4  59   260 true 8.2 4.4 160 320
ldv-regression/ex3_forlist.c_true-unreach-call.i true 2 wit inspect .31 .30  2.9  17 .025  0      - - exception 4.6  2.6  43   270 true 32   18   580 710
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect .18 .18  1.6  17 0      0      - - true 4.0  2.2  41   250 true 7.1 3.8 120 320
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect .17 .17  1.8  17 0      0      - - true 4.4  2.5  47   260 true 8.3 4.5 130 320
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect .16 .16  1.5  17 0      0      - - true 3.4  1.9  68   250 true 8.8 4.7 160 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect .19 .19  1.4  17 0      0      - - true 4.5  2.5  46   260 true 10   5.6 190 350
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect .17 .16  1.5  19 0      0      - - true 3.4  1.9  59   260 true 7.6 4.0 120 320
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect .18 .17  1.4  17 0      0      - - true 4.5  2.5  49   270 true 8.2 4.3 130 330
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect .16 .16  1.3  17 0      0      - - true 4.7  2.6  41   270 true 14   7.5 250 450
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect .17 .17  1.6  17 0      .29   - - true 4.6  2.6  52   270 true 13   7.0 200 470
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect .16 .16  1.6  17 0      0      - - true 4.3  2.4  52   260 true 12   6.4 200 370
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect .14 .14  2.0  17 0      0      - - true 3.4  1.9  80   260 true 8.3 4.5 190 320
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect .19 .19  1.7  19 0      2.5    - - true 3.3  1.9  54   260 true 9.8 5.2 73 330
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect .19 .18  1.6  20 0      0      - - true 4.2  2.3  74   260 true 9.2 4.9 150 350
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect .33 .33  3.2  21 .016  0      - - true 4.5  2.5  83   270 true 11   6.2 200 360
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect .22 .21  1.7  19 0      0      - - true 6.5  3.5  66   270 true 29   17   450 640
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect .18 .17  2.0  18 0      0      - - true 5.4  3.0  57   260 true 6.9 3.7 150 310
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect .19 .19  1.4  17 0      0      - - true 4.1  2.3  45   260 true 8.3 4.4 180 340
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect .17 .17  1.6  18 0      0      - - true 5.5  3.0  61   270 true 8.1 4.3 180 330
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect .15 .15  1.5  17 0      0      - - true 3.3  1.9  67   260 true 8.5 4.5 110 320
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect .33 .33  3.4  20 .016  0      - - true 4.9  2.7  76   260 true 8.5 4.6 160 340
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect .17 .17  1.5  18 0      0      - - true 4.2  2.4  85   260 true 8.1 4.3 150 330
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect .22 .21  1.7  19 0      0      - - true 6.6  3.5  65   280 true 7.9 4.2 140 320
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect .14 .14  1.5  17 0      0      - - true 3.3  1.8  54   250 true 7.7 4.1 140 320
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect .17 .17  1.6  17 0      0      - - true 3.2  1.8  53   250 true 7.7 4.1 180 330
ldv-regression/test_union_cast-1_true-unreach-call.i true 2 wit inspect .15 .15  1.9  17 0      .16   - - true 4.2  2.3  56   260 unknown 6.2 3.3 110 300
ldv-regression/test_union_cast-2_true-unreach-call.i true 2 wit inspect .18 .17  1.5  17 0      0      - - true 3.7  2.0  79   260 unknown 7.3 3.8 110 310
ldv-regression/test_union_cast.c_true-unreach-call.i true 2 wit inspect .19 .19  1.6  17 0      0      - - true 4.2  2.4  49   260 unknown 6.6 3.5 130 300
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2 wit inspect .17 .16  1.3  17 0      0      - - true 4.3  2.4  51   260 unknown 8.2 4.3 92 320
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect .19 .18  1.5  17 0      0      - - true 4.3  2.4  40   260 true 8.0 4.3 160 310
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect .17 .16  1.7  19 0      0      - - true 4.2  2.4  42   270 true 7.9 4.3 150 330
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect .12 .11  1.1  17 .0041 0      false(unreach-call) 3.6  2.0  72   270 false(unreach-call) 8.5 4.5 110 310 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect .12 .11  .96 17 .0041 0      true 3.7  2.1  75   270 false(unreach-call) 11   5.6 130 310 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect .14 .14  .95 17 .0041 0      false(unreach-call) 3.8  2.1  52   280 false(unreach-call) 7.5 4.0 160 310 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .12  .78 17 .0041 0      true 3.4  1.9  73   270 false(unreach-call) 8.9 4.7 98 320 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect .12 .12  1.0  17 .0041 0      false(unreach-call) 3.9  2.2  55   280 false(unreach-call) 8.3 4.5 150 320 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .15 .14  1.0  18 .0041 0      false(unreach-call) 4.3  2.4  86   280 false(unreach-call) 12   6.8 240 380 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect .70 .69  7.6  25 .074  0      false(unreach-call) 6.1  3.4  78   320 timeout 98   62   1700 4700 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect .92 .91  10    27 .21   0      false(unreach-call) 15    12    290   500 out of memory 80   48   1400 7000 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect .75 .75  9.7  23 .057  0      assertion 3.4  1.9  51   270 timeout 98   58   1800 6500 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect .14 .13  .86 17 .0041 0      false(unreach-call) 3.6  2.1  86   270 false(unreach-call) 11   5.7 130 340 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect .19 .18  1.5  23 .0041 0      assertion 3.5  2.0  72   270 false(unreach-call) 8.1 4.4 180 330 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect .12 .12  .91 17 .0041 .16   false(unreach-call) 3.6  2.0  42   280 false(unreach-call) 11   6.0 110 350 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect .12 .12  .89 17 .0041 0      false(unreach-call) 3.8  2.1  44   280 false(unreach-call) 10   5.4 170 370 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect .12 .12  .96 17 .0041 0      false(unreach-call) 3.8  2.1  78   280 false(unreach-call) 8.8 4.6 140 330 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect .16 .16  1.5  17 .0082 0      - - true 3.8  2.2  54   260 true 7.7 4.1 150 320
ldv-regression/test03_true-unreach-call.c true 2 wit inspect .17 .16  1.8  17 .0082 0      - - true 3.7  2.1  62   260 true 8.4 4.5 160 320
ldv-regression/test04_true-unreach-call.c true 2 wit inspect .18 .17  1.5  17 .0082 0      - - true 4.2  2.3  51   260 true 8.4 4.6 170 310
ldv-regression/test05_true-unreach-call.c true 2 wit inspect .18 .17  1.8  17 .0082 0      - - true 4.6  2.5  51   260 true 13   7.7 270 520
ldv-regression/test07_true-unreach-call.c true 2 wit inspect .19 .19  1.6  17 .0082 0      - - true 3.7  2.0  40   260 true 11   6.1 190 350
ldv-regression/test09_true-unreach-call.c true 2 wit inspect .20 .19  1.4  17 .0082 0      - - true 4.4  2.5  52   260 true 12   6.5 190 380
ldv-regression/test10_true-unreach-call.c true 2 wit inspect .17 .17  1.6  17 .0082 .16   - - true 4.2  2.4  44   260 true 20   11   370 500
ldv-regression/test11_true-unreach-call.c true 2 wit inspect .20 .19  1.4  17 .0082 0      - - true 3.8  2.1  75   270 true 12   6.2 110 340
ldv-regression/test13_true-unreach-call.c true 2 wit inspect .21 .20  1.3  17 .0082 0      - - true 3.8  2.1  64   260 true 7.8 4.1 150 310
ldv-regression/test14_true-unreach-call.c true 2 wit inspect .20 .19  1.6  17 .0082 0      - - true 3.6  2.1  63   260 true 9.4 5.1 130 310
ldv-regression/test15_true-unreach-call.c true 2 wit inspect .18 .17  1.6  17 .0082 0      - - true 4.2  2.4  46   250 true 10   5.6 200 350
ldv-regression/test16_true-unreach-call.c true 2 wit inspect .18 .17  1.8  17 .0082 0      - - true 4.2  2.3  43   260 true 9.1 5.0 160 350
ldv-regression/test17_true-unreach-call.c true 2 wit inspect .19 .18  2.0  17 .0082 0      - - true 3.3  1.8  55   260 true 7.6 4.1 160 320
ldv-regression/test18_true-unreach-call.c true 2 wit inspect .18 .18  1.8  17 .0082 0      - - true 3.4  1.9  50   260 true 9.8 5.3 190 340
ldv-regression/test19_true-unreach-call.c true 2 wit inspect .18 .18  1.7  17 .0082 0      - - true 3.3  1.9  46   260 true 11   6.5 210 450
ldv-regression/test20_true-unreach-call.c true 2 wit inspect .17 .17  1.7  17 .0082 0      - - true 3.3  1.8  74   260 true 7.8 4.1 130 310
ldv-regression/test21_true-unreach-call.c true 2 wit inspect .21 .20  1.4  17 .0082 .16   - - true 3.6  2.0  76   260 true 12   6.2 160 350
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 1.2  1.2   14    20 .061  .10   - - true 8.2  4.8  95   310 true 38   25   520 750
ldv-regression/test23_true-unreach-call.c true 2 wit inspect .88 .87  9.3  25 .070  .27   - - true 13    9.8  210   400 true 150   130   3200 1000
ldv-regression/test24_true-unreach-call.c true 2 wit inspect .71 .71  9.1  23 .061  0      - - true 6.2  3.6  130   320 true 14   7.5 190 370
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 2.6  2.6   29    26 .082  0      - - true 33    26    450   510 true 30   16   450 710
ldv-regression/test26_true-unreach-call.c true 2 wit inspect .19 .22  1.7  29 .0082 13      - - true 4.2  2.4  55   250 true 10   5.6 150 340
ldv-regression/test27_true-unreach-call.c true 2 wit inspect .77 .76  7.3  24 .061  0      - - true 8.2  5.6  220   310 true 96   76   1500 870
ldv-regression/test28_true-unreach-call.c true 2 wit inspect .19 .19  1.5  17 .0082 0      - - true 4.6  2.6  49   260 true 8.7 4.7 150 330
ldv-regression/test29_true-unreach-call.c true 2 wit inspect .16 .16  1.6  17 .0082 0      - - true 3.9  2.2  59   260 true 9.0 4.9 160 340
ldv-regression/test30_true-unreach-call.c true 2 wit inspect .18 .18  1.9  17 .0082 0      - - true 4.4  2.4  54   270 true 11   6.0 230 460
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 23    23     250    660 1.6    0      false(unreach-call) 14    7.8  270   520 false(unreach-call) 69   45   1300 770 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 19    19     230    650 1.3    0      false(unreach-call) 13    7.3  150   530 false(unreach-call) 65   43   1400 740 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 22    22     240    650 1.5    0      false(unreach-call) 14    7.4  160   530 false(unreach-call) 74   48   880 790 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     6500    1200 14      0      - - error (invalid witness file) .70 .45 8.5 42 error (invalid witness file) 6.9 3.6 130 310
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     6300    1200 14      12      - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.5 3.4 120 300
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     6300    1200 14      0      - - error (invalid witness file) .55 .35 8.4 40 error (invalid witness file) 6.3 3.3 120 300
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     6300    1200 14      0      - - error (invalid witness file) .77 .48 8.6 43 error (invalid witness file) 6.9 3.6 130 310
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     8500    1200 14      0      - - error (invalid witness file) .65 .42 9.4 41 error (invalid witness file) 6.4 3.4 140 300
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     6000    1200 14      0      - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.2 3.3 94 310
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     5800    1200 14      0      - - error (invalid witness file) .64 .42 8.7 40 error (invalid witness file) 6.1 3.2 140 310
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     7400    1200 14      .10   - - error (invalid witness file) .61 .39 7.6 39 error (invalid witness file) 6.9 3.6 130 310
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     5800    1200 14      0      - - error (invalid witness file) .48 .30 12   40 error (invalid witness file) 6.7 3.5 120 300
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     8100    1200 14      0      - - error (invalid witness file) .47 .31 8.2 40 error (invalid witness file) 6.6 3.5 120 300
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 .21  2.1  21 .0082 0      false(unreach-call) 6.6  3.5  130   310 false(unreach-call) 19   11   290 570 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .24 .24  2.6  26 .0082 0      false(unreach-call) 5.2  2.9  100   300 false(unreach-call) 15   8.3 230 390 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .23 .22  2.0  20 .0082 0      false(unreach-call) 5.2  2.8  64   300 false(unreach-call) 9.3 4.9 170 360 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .60 .59  5.2  24 .066  0      false(unreach-call) 7.0  3.8  130   300 false(unreach-call) 16   8.6 170 460 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .30 .29  2.9  28 .0082 .16   false(unreach-call) 5.9  3.2  120   300 false(unreach-call) 12   6.2 200 380 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect .35 .34  4.8  30 .0082 0      false(unreach-call) 6.1  3.3  65   310 error 10   5.6 150 310 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .28 .28  2.6  24 .0082 0      false(unreach-call) 6.1  3.3  140   300 false(unreach-call) 13   6.7 130 370 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .24 .23  2.5  24 .0082 0      false(unreach-call) 5.9  3.2  110   290 false(unreach-call) 12   6.1 250 370 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .26 .25  2.4  24 .0082 0      false(unreach-call) 4.9  2.7  44   290 false(unreach-call) 11   5.8 220 360 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .24 .23  2.0  21 .0082 0      false(unreach-call) 7.2  3.9  130   310 false(unreach-call) 17   9.5 270 560 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .29 .28  2.6  24 .0082 0      false(unreach-call) 5.8  3.2  84   310 false(unreach-call) 14   7.2 130 380 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .25 .24  2.4  26 .0082 0      false(unreach-call) 5.3  2.9  86   300 false(unreach-call) 13   7.2 270 390 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 .21  2.2  20 .0082 0      false(unreach-call) 5.4  2.9  84   300 false(unreach-call) 8.6 4.6 180 350 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .58 .57  5.2  22 .061  0      false(unreach-call) 6.3  3.4  82   290 false(unreach-call) 13   6.7 270 450 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .23 .23  2.5  23 .0082 0      false(unreach-call) 5.8  3.2  75   300 false(unreach-call) 10   5.4 180 370 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .25 .24  2.4  23 .0082 0      false(unreach-call) 5.8  3.2  88   300 error 10   5.6 210 300 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .25 .25  2.3  22 .0082 0      false(unreach-call) 5.3  2.9  110   290 false(unreach-call) 10   5.3 120 320 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .24 .23  2.2  21 .0082 0      false(unreach-call) 6.5  3.5  110   300 false(unreach-call) 17   8.9 260 410 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .23 .22  1.9  21 .0082 0      false(unreach-call) 5.6  3.1  100   290 false(unreach-call) 11   5.8 200 360 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (1) 0 wit inspect 670    670     6300    2200 10      0      - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 6.6 3.5 110 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 290    290     4100    15000 10      0      - - error (invalid witness file) .66 .43 7.9 41 error (invalid witness file) 5.9 3.1 120 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (1) 0 wit inspect 72    72     850    200 1.5    0      - - error (invalid witness file) .57 .37 12   45 error (invalid witness file) 5.3 2.9 100 290
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     2800    1500 1.1    0      - - error (invalid witness file) .58 .37 11   40 error (invalid witness file) 6.5 3.4 100 310
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     6400    2900 1.4    0      - - error (invalid witness file) .58 .37 10   40 error (invalid witness file) 6.2 3.3 130 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     5300    3100 1.4    0      - - error (invalid witness file) .53 .33 11   39 error (invalid witness file) 6.2 3.3 92 290
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     7000    5300 3.5    0      - - error (invalid witness file) .62 .39 6.7 41 error (invalid witness file) 6.2 3.3 110 300
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     7300    10000 1.9    0      - - error (invalid witness file) .70 .46 9.7 44 error (invalid witness file) 8.4 4.3 110 310
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     11000    870 3.6    0      - - error (invalid witness file) .53 .35 7.5 41 error (invalid witness file) 7.2 3.8 96 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     11000    900 2.3    0      - - error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.2 3.3 130 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (1) 0 wit inspect 600    600     6500    1400 9.4    0      - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 6.2 3.3 120 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     11000    570 .64   0      - - error (invalid witness file) .62 .39 8.3 40 error (invalid witness file) 6.4 3.4 93 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 300    300     3300    15000 11      0      - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.5 3.4 110 290
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (1) 0 wit inspect 72    72     970    170 1.4    0      - - error (invalid witness file) .54 .34 9.4 40 error (invalid witness file) 6.0 3.2 120 290
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     3200    1100 1.1    0      - - error (invalid witness file) .65 .43 8.8 41 error (invalid witness file) 6.5 3.4 110 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     5900    2100 1.3    0      - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 7.0 3.7 96 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     5500    2200 1.4    0      - - error (invalid witness file) .62 .40 8.3 39 error (invalid witness file) 8.0 4.2 77 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     6900    2200 12      0      - - error (invalid witness file) .63 .39 8.4 40 error (invalid witness file) 6.3 3.3 110 310
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 850    850     5800    6100 1.8    0      - - error (invalid witness file) .57 .36 9.9 41 error (invalid witness file) 6.4 3.4 120 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     5900    7400 3.4    0      - - error (invalid witness file) .54 .34 8.2 42 error (invalid witness file) 5.8 3.1 110 290
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850     10000    930 1.9    0      - - error (invalid witness file) .58 .38 10   42 error (invalid witness file) 6.1 3.3 120 300
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .27 .26  2.3  23 .0082 0      timeout 98    82    1100   2800 false(unreach-call) 12   6.3 110 330 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-free) 0 wit inspect .21 .21  2.1  20 .0082 0      timeout 98    78    1100   3400 true 7.4 4.0 130 310 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 .20  1.8  20 .0082 0      false(unreach-call) 5.4  2.9  81   300 false(unreach-call) 8.2 4.4 160 320 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i false(unreach-call) 1 wit inspect .46 .46  5.3  36 .0082 0      true 6.5  3.5  140   320 false(unreach-call) 12   6.5 220 370 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i error (42) 0 wit inspect 850    850     5500    1700 .65   0      - - error (invalid witness file) .64 .41 7.8 39 error (invalid witness file) 6.1 3.2 90 300
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect .25 .24  2.7  23 .0082 0      false(unreach-call) 6.1  3.3  110   310 false(unreach-call) 8.7 4.6 170 320 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i error (42) 0 wit inspect 850    850     11000    360 .33   0      - - error (invalid witness file) .51 .33 13   39 error (invalid witness file) 6.4 3.4 120 300
list-ext2-properties/simple_search_value_false-unreach-call.i false(unreach-call) 1 wit inspect .79 .79  11    20 .15   0      false(unreach-call) 9.2  5.6  190   390 timeout 97   84   1700 1000 - -
list-ext2-properties/simple_search_value_true-unreach-call.i error (1) 0 wit inspect 110    110     1000    2900 8.7    0      - - error (invalid witness file) .68 .42 8.6 41 error (invalid witness file) 5.7 3.1 110 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 186 32000 32000 270000 160000 280    43 173 560 360 8300 26000   173 1200 740 20000 43000   173 330 200 4700 18000   173 1200 740 21000 38000  
    correct results 125 186 98 98 1100 4400 6.2  30 60 460 290 7300 22000   57 1200 730 20000 43000   59 300 180 4300 16000   57 930 580 16000 24000  
        correct true 61 122 17 17 170 1100 .65 16 7 0 0 0 0   1 0 0 0 0   59 300 180 4300 16000   57 930 580 16000 24000  
        correct false 64 64 81 81 900 3300 5.5  14 53 460 290 7300 22000   56 1200 730 20000 43000   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) 186
Run set sv-comp17.ReachSafety-Heap