Tool 2LS 0.5.0
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 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 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/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.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/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.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 (134) 0 wit inspect .30  .30  2.8  35 .0082 0     error (invalid witness file) .51 .34 4.3 40 error (invalid witness file) 6.9 3.6 44 290 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .19  .19  1.4  27 .0082 0     error (invalid witness file) .48 .31 8.7 39 error (invalid witness file) 6.9 3.6 79 310 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i error (8) 0 wit inspect .29  .29  3.5  29 .0082 0     error (invalid witness file) .50 .35 5.0 40 error (invalid witness file) 5.5 2.9 80 300 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .24  .23  2.3  27 .0082 0     false(unreach-call) 7.5  4.1  160   360 true 9.0 4.9 140 320 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-free) 0 wit inspect .59  .58  6.4  35 .0082 0     true 7.8  4.1  97   350 true 7.9 4.3 120 320 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900     900     9100    11000 .0082 0     error (invalid witness file) .48 .31 6.0 40 error (invalid witness file) 5.9 3.1 93 300 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .30  .30  2.6  36 .0082 0     - - error (invalid witness file) .62 .40 7.0 39 error (invalid witness file) 5.7 3.1 87 290
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .16  .16  1.5  26 .0082 0     - - error (invalid witness file) .65 .42 7.4 40 error (invalid witness file) 6.9 3.6 130 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .19  .19  1.7  27 .0082 0     - - error (invalid witness file) .53 .35 10   39 error (invalid witness file) 6.9 3.6 140 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .29  .29  2.9  29 .0082 0     - - error (invalid witness file) .52 .35 6.6 40 error (invalid witness file) 6.6 3.5 120 310
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect .24  .23  1.9  27 .0082 0     - - timeout 900    890    20000   650 true 8.8 4.7 180 320
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900     900     9800    10000 .0082 0     - - error (invalid witness file) .64 .41 6.9 40 error (invalid witness file) 7.2 3.8 110 310
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i error (8) 0 wit inspect .33  .32  2.9  28 .0082 0     error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.1 3.2 120 290 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900     900     12000    3700 .0082 0     error (invalid witness file) .56 .37 9.7 41 error (invalid witness file) 5.5 3.0 110 290 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900     900     11000    3100 .0082 0     error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.8 3.1 110 290 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .22  .21  2.3  26 .0082 0     false(unreach-call) 5.7  3.1  74   300 true 17   9.9 310 560 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900     900     11000    2900 .0082 0     error (invalid witness file) .57 .36 13   41 error (invalid witness file) 7.4 3.9 83 300 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect .18  .17  2.0  26 .0082 0     unknown 8.5  4.5  140   330 false(unreach-call) 10   5.4 190 360 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .29  .28  3.7  28 .0082 0     - - error (invalid witness file) .58 .37 14   43 error (invalid witness file) 6.2 3.3 120 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     13000    3100 .0082 0     - - error (invalid witness file) .74 .46 7.4 41 error (invalid witness file) 6.9 3.6 130 320
list-properties/list_search_true-unreach-call_false-valid-memtrack.i error (8) 0 wit inspect .20  .20  1.6  28 .0082 0     - - error (invalid witness file) .61 .39 8.6 42 error (invalid witness file) 6.1 3.2 110 300
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     9600    3700 .0082 0     - - error (invalid witness file) .63 .40 7.4 40 error (invalid witness file) 6.6 3.5 99 290
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     10000    2700 .0082 0     - - error (invalid witness file) .56 .36 9.8 39 error (invalid witness file) 6.4 3.4 120 300
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     10000    2900 .0082 0     - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.0 3.2 120 300
list-properties/splice_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .21  .21  1.8  26 .0082 0     - - timeout 900    870    13000   6200 timeout 960   910   18000 1700
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect .15  .15  2.0  24 .0082 0     false(unreach-call) 3.8  2.2  30   270 true 6.9 3.7 150 310 - -
ldv-regression/alt_test.c_false-unreach-call.i true -32 wit inspect .18  .18  1.9  28 .0082 0     false(unreach-call) 7.4  3.9  120   310 false(unreach-call) 10   5.4 150 340 - -
ldv-regression/callfpointer.c_false-unreach-call.i false(unreach-call) 1 wit inspect .12  .12  .75 22 0      .16  false(unreach-call) 3.6  2.0  77   280 false(unreach-call) 7.3 3.9 150 310 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .19  .18  2.0  27 .0082 0     false(unreach-call) 5.1  2.8  69   290 unknown 15   7.9 240 350 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .094 .087 .79 22 0      0     false(unreach-call) 3.6  2.0  67   270 false(unreach-call) 8.5 4.6 150 320 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect .10  .096 .83 22 0      0     false(unreach-call) 3.7  2.1  60   270 false(unreach-call) 10   5.5 130 330 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect .21  .20  1.5  24 .0082 0     false(unreach-call) 4.2  2.3  90   280 true 7.2 3.9 150 310 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i error (134) 0 wit inspect .090 .088 .77 23 0      0     error (invalid witness file) .53 .33 13   39 error (invalid witness file) 5.9 3.1 110 300 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .13  .12  .91 24 0      0     false(unreach-call) 5.6  3.0  100   290 false(unreach-call) 13   6.8 140 360 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect .89  .89  13    36 0      .20  false(unreach-call) 4.5  2.5  43   280 false(unreach-call) 9.4 5.0 170 350 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .14  .13  1.4  23 0      0     false(unreach-call) 4.0  2.2  87   280 false(unreach-call) 7.4 3.9 150 320 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .15  .14  1.3  23 0      0     false(unreach-call) 3.7  2.1  74   270 false(unreach-call) 7.2 3.9 93 320 - -
ldv-regression/alias_of_return.c_true-unreach-call.i false(unreach-call) -16 wit inspect .13  .12  .86 22 0      .16  - - true 3.4  1.9  59   270 true 9.6 5.1 110 310
ldv-regression/alias_of_return.c_true-unreach-call_1.i false(unreach-call) -16 wit inspect .097 .091 .72 22 0      0     - - true 4.5  2.5  45   280 true 8.0 4.3 140 320
ldv-regression/alias_of_return_2.c_true-unreach-call.i false(unreach-call) -16 wit inspect .10  .097 .72 22 0      0     - - true 4.5  2.5  51   280 true 9.2 4.9 150 320
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i false(unreach-call) -16 wit inspect .090 .086 .79 22 0      .24  - - true 3.6  2.0  79   270 true 7.8 4.2 160 330
ldv-regression/ex3_forlist.c_true-unreach-call.i false(unreach-call) -16 wit inspect .43  .42  5.2  33 0      0     - - true 10    5.3  79   450 true 19   10   420 550
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect .089 .085 .81 22 0      0     - - true 3.4  1.9  52   250 true 6.8 3.6 93 320
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect .11  .11  .78 22 0      0     - - true 3.7  2.0  73   260 true 8.7 4.7 170 320
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect .12  .11  .72 22 0      0     - - true 3.4  1.9  54   260 true 8.5 4.5 180 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect .11  .11  .73 22 0      0     - - true 3.2  1.8  56   260 true 9.6 5.2 180 320
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect .11  .10  .73 22 0      0     - - true 4.0  2.2  51   260 true 7.0 3.8 140 310
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect .088 .086 .79 22 0      0     - - true 3.7  2.1  65   260 true 8.5 4.5 120 320
ldv-regression/nested_structure_ptr.c_true-unreach-call.i false(unreach-call) -16 wit inspect .13  .12  .89 22 0      0     - - true 3.3  1.9  79   260 true 7.2 3.8 120 310
ldv-regression/nested_structure_ptr_true-unreach-call.i false(unreach-call) -16 wit inspect .10  .095 .87 22 0      0     - - true 4.3  2.5  51   270 true 7.1 3.8 130 310
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect .10  .099 .72 22 0      0     - - true 3.6  2.1  59   260 true 14   7.5 150 350
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect .10  .098 .76 22 0      0     - - true 4.4  2.4  53   260 true 8.0 4.3 160 320
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect .11  .10  .70 22 0      0     - - true 4.3  2.5  41   250 true 7.5 4.0 110 320
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect .098 .099 .74 22 0      0     - - true 5.4  3.0  52   260 true 9.1 4.9 180 350
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect .17  .17  1.4  26 .0082 0     - - true 5.9  3.2  59   270 true 11   6.2 160 370
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect .13  .12  1.0  25 0      0     - - true 5.5  3.1  79   270 true 29   17   550 720
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect .12  .11  .77 24 0      0     - - true 4.4  2.5  74   260 true 7.4 4.0 94 330
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect .11  .10  .74 22 0      0     - - true 3.5  1.9  55   260 true 8.2 4.4 110 310
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect .11  .11  .91 24 0      .16  - - true 5.4  3.0  51   270 true 8.3 4.4 160 330
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect .085 .081 .85 22 0      0     - - true 3.3  1.9  50   260 true 7.8 4.2 150 320
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect .18  .18  1.6  26 .0082 0     - - true 5.7  3.2  69   260 true 8.5 4.5 180 330
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect .13  .12  .86 25 0      0     - - true 5.3  2.9  63   270 true 8.3 4.5 170 330
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect .13  .13  .92 26 0      0     - - true 5.3  2.8  69   280 true 7.5 4.0 120 320
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect .098 .095 .90 22 0      0     - - true 3.3  1.9  62   260 true 7.2 3.9 160 320
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect .12  .11  .65 22 0      0     - - true 4.5  2.5  44   260 true 7.3 3.9 84 320
ldv-regression/test_union_cast-1_true-unreach-call.i true 2 wit inspect .094 .090 .76 22 0      0     - - true 3.6  2.0  63   260 unknown 6.0 3.2 120 290
ldv-regression/test_union_cast-2_true-unreach-call.i true 2 wit inspect .085 .083 .86 22 0      0     - - true 4.2  2.3  45   260 unknown 6.5 3.4 140 290
ldv-regression/test_union_cast.c_true-unreach-call.i true 2 wit inspect .12  .11  .74 22 0      0     - - true 4.5  2.5  44   260 unknown 6.6 3.5 140 310
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2 wit inspect .090 .087 .74 22 0      0     - - true 3.4  1.9  78   260 unknown 6.2 3.3 130 290
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect .089 .086 .98 22 0      0     - - true 3.8  2.1  46   260 true 8.1 4.3 140 310
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect .080 .078 .87 22 0      0     - - true 4.4  2.5  45   260 true 9.3 5.0 130 320
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect .13  .13  .85 22 .0041 0     false(unreach-call) 3.6  2.0  70   270 false(unreach-call) 6.5 3.5 140 300 - -
ldv-regression/test06_false-unreach-call.c true -32 wit inspect .12  .12  .69 22 .0041 0     false(unreach-call) 5.0  2.8  77   280 false(unreach-call) 12   6.3 130 340 - -
ldv-regression/test08_false-unreach-call.c true -32 wit inspect .12  .12  .74 22 .0041 0     false(unreach-call) 4.3  2.4  73   270 false(unreach-call) 7.2 3.9 150 310 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .10  .91 22 .0041 0     false(unreach-call) 3.8  2.2  66   280 true 8.5 4.5 100 320 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect .14  .13  .90 22 .0041 0     false(unreach-call) 4.3  2.4  96   280 true 7.7 4.1 140 330 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .13  .12  .92 23 .0041 0     timeout 91    85    1100   360 true 7.6 4.1 160 320 - -
ldv-regression/test23_false-unreach-call.c error (134) 0 wit inspect .15  .15  .98 25 .0041 0     error (invalid witness file) .54 .33 10   40 error (invalid witness file) 5.9 3.1 120 300 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 2.6   2.6   28    130 .0041 0     exception 4.6  2.5  56   280 out of memory 59   37   800 7000 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect .14  .13  .94 24 .0041 0     false(unreach-call) 16    9.8  350   360 true 7.9 4.2 180 320 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect .097 .091 .96 22 .0041 0     false(unreach-call) 3.6  2.0  78   280 true 7.9 4.1 180 330 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect .17  .17  1.5  29 .0041 0     false(unreach-call) 3.8  2.1  49   280 false(unreach-call) 9.5 5.1 110 310 - -
ldv-regression/test28_false-unreach-call.c error (134) 0 wit inspect .082 .080 .84 22 .0041 0     error (invalid witness file) .49 .32 9.6 40 error (invalid witness file) 5.1 2.8 110 290 - -
ldv-regression/test29_false-unreach-call.c error (134) 0 wit inspect .12  .12  .67 22 .0041 0     error (invalid witness file) .50 .32 10   42 error (invalid witness file) 5.7 3.1 110 300 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .097 .96 22 .0041 0     false(unreach-call) 3.8  2.1  81   280 true 7.8 4.2 120 320 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect .11  .11  .76 22 .0041 0     - - true 3.6  2.0  77   250 true 8.0 4.2 180 310
ldv-regression/test03_true-unreach-call.c true 2 wit inspect .11  .11  .65 22 .0041 0     - - true 4.1  2.3  56   260 true 9.0 4.9 150 330
ldv-regression/test04_true-unreach-call.c true 2 wit inspect .11  .11  .78 22 .0041 .16  - - true 3.5  2.0  70   260 true 8.7 4.7 170 320
ldv-regression/test05_true-unreach-call.c false(unreach-call) -16 wit inspect .13  .12  .85 22 .0041 0     - - true 4.9  2.7  65   280 true 7.5 4.0 140 310
ldv-regression/test07_true-unreach-call.c false(unreach-call) -16 wit inspect .10  .097 .95 22 .0041 0     - - true 4.1  2.3  60   270 true 9.1 4.8 190 330
ldv-regression/test09_true-unreach-call.c true 2 wit inspect .11  .11  .74 22 .0041 0     - - true 4.0  2.3  70   260 true 11   5.9 210 360
ldv-regression/test10_true-unreach-call.c false(unreach-call) -16 wit inspect .10  .097 .90 22 .0041 0     - - true 4.4  2.5  78   270 true 21   12   300 590
ldv-regression/test11_true-unreach-call.c true 2 wit inspect .12  .12  .82 22 .0041 0     - - true 3.7  2.1  74   270 true 9.4 5.1 200 330
ldv-regression/test13_true-unreach-call.c true 2 wit inspect .12  .12  .72 22 .0041 0     - - true 4.1  2.3  47   260 true 8.2 4.4 170 320
ldv-regression/test14_true-unreach-call.c true 2 wit inspect .13  .13  .78 22 .0041 0     - - true 4.0  2.2  44   270 true 9.9 5.2 180 320
ldv-regression/test15_true-unreach-call.c true 2 wit inspect .10  .10  .93 22 .0041 .16  - - true 4.0  2.2  58   260 true 11   6.1 170 360
ldv-regression/test16_true-unreach-call.c true 2 wit inspect .080 .078 .89 22 .0041 0     - - true 3.4  1.9  74   260 true 9.7 5.3 190 350
ldv-regression/test17_true-unreach-call.c true 2 wit inspect .088 .086 .84 22 .0041 0     - - true 4.3  2.4  52   260 true 7.6 4.0 120 320
ldv-regression/test18_true-unreach-call.c true 2 wit inspect .11  .10  .82 22 .0041 0     - - true 3.6  2.0  67   260 true 9.4 5.1 160 320
ldv-regression/test19_true-unreach-call.c true 2 wit inspect .11  .11  .71 22 .0041 0     - - true 3.9  2.2  68   260 true 11   6.1 210 470
ldv-regression/test20_true-unreach-call.c true 2 wit inspect .10  .10  .79 22 .0041 0     - - true 3.9  2.2  43   260 true 8.0 4.3 150 320
ldv-regression/test21_true-unreach-call.c true 2 wit inspect .12  .12  .74 22 .0041 0     - - true 3.7  2.1  77   260 true 9.8 5.4 190 330
ldv-regression/test22_true-unreach-call.c false(unreach-call) -16 wit inspect .14  .13  .92 22 .0041 0     - - true 480    470    10000   630 true 8.1 4.3 160 330
ldv-regression/test23_true-unreach-call.c error (134) 0 wit inspect .13  .13  .96 25 .0041 0     - - error (invalid witness file) .53 .33 5.3 40 error (invalid witness file) 6.0 3.2 120 290
ldv-regression/test24_true-unreach-call.c false(unreach-call) -16 wit inspect .16  .15  1.1  24 .0041 0     - - exception 4.4  2.5  43   270 true 14   7.6 220 370
ldv-regression/test25_true-unreach-call.c false(unreach-call) -16 wit inspect 1.1   1.1   16    49 .0041 0     - - timeout 910    900    19000   1700 out of memory 83   50   1500 7000
ldv-regression/test26_true-unreach-call.c true 2 wit inspect .10  .10  .91 22 .0041 0     - - true 3.6  2.0  78   260 true 10   5.8 160 340
ldv-regression/test27_true-unreach-call.c false(unreach-call) -16 wit inspect .17  .17  1.5  28 .0041 0     - - false(unreach-call) 21    13    510   360 true 23   14   410 600
ldv-regression/test28_true-unreach-call.c true 2 wit inspect .12  .12  .79 22 .0041 0     - - true 3.8  2.1  72   260 true 9.0 4.8 160 330
ldv-regression/test29_true-unreach-call.c true 2 wit inspect .11  .11  .94 22 .0041 .053 - - true 4.0  2.2  57   260 true 8.8 4.8 180 330
ldv-regression/test30_true-unreach-call.c false(unreach-call) -16 wit inspect .14  .13  .67 22 .0041 0     - - true 4.3  2.4  45   270 true 7.5 3.9 130 320
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true -32 wit inspect 2.3   2.3   23    330 .0082 0     timeout 96    69    1500   3400 timeout 96   79   1700 1200 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true -32 wit inspect 2.0   2.0   23    280 .0082 0     timeout 95    73    1000   2900 timeout 97   80   860 1100 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true -32 wit inspect 2.2   2.2   25    310 .0082 0     timeout 97    73    1400   2900 timeout 97   79   1200 1200 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 1.0   1.0   11    210 .0082 0     - - true 13    6.7  220   420 true 13   7.1 240 440
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .97  1.0   11    220 .0082 11     - - true 12    6.1  210   430 true 12   6.7 220 440
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .96  .95  10    210 .0082 0     - - true 13    6.7  230   440 true 12   6.4 230 440
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .97  .97  10    210 .0082 0     - - true 15    7.9  160   430 true 15   8.2 170 440
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .98  .97  9.9  210 .0082 0     - - true 13    6.9  240   440 true 12   6.4 190 430
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .97  .97  11    210 .0082 0     - - true 12    6.5  160   440 true 16   8.4 170 430
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .96  .95  11    210 .0082 0     - - true 15    7.8  190   440 true 12   6.7 240 450
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .97  .96  9.5  210 .0082 0     - - true 14    7.3  200   430 true 16   8.6 140 450
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .97  .97  9.7  210 .0082 0     - - true 14    7.3  100   440 true 14   7.2 260 460
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 1.0   .99  8.6  210 .0082 0     - - true 12    6.4  230   440 true 12   6.7 200 440
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .26  .25  1.7  28 .0082 0     false(unreach-call) 6.1  3.3  120   300 false(unreach-call) 16   9.1 340 510 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i error (134) 0 wit inspect .18  .18  1.8  28 .0082 0     error (invalid witness file) .54 .34 13   41 error (invalid witness file) 6.0 3.2 100 300 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21  .21  1.9  26 .0082 0     false(unreach-call) 5.3  2.9  110   300 false(unreach-call) 9.8 5.3 140 350 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900     900     9200    12000 .0082 0     error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.2 3.3 120 300 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .22  .21  1.9  29 .0082 0     false(unreach-call) 5.0  2.8  99   290 false(unreach-call) 9.8 5.3 130 350 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     900     9200    9200 .0082 0     error (invalid witness file) .69 .44 10   42 error (invalid witness file) 5.9 3.1 99 300 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21  .21  2.3  28 .0082 0     true 4.8  2.6  98   280 false(unreach-call) 7.8 4.2 150 320 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i error (8) 0 wit inspect .30  .30  2.9  29 .0082 0     error (invalid witness file) .51 .32 12   40 error (invalid witness file) 7.6 4.0 80 310 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i error (134) 0 wit inspect .18  .18  2.3  26 .0082 0     error (invalid witness file) .55 .35 12   41 error (invalid witness file) 5.7 3.1 100 300 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i out of memory 0 wit inspect 400     400     3700    15000 .0082 0     error (invalid witness file) .51 .32 12   40 error (invalid witness file) 5.9 3.2 99 310 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i error (8) 0 wit inspect .26  .26  2.1  28 .0082 0     error (invalid witness file) .49 .31 7.9 39 error (invalid witness file) 5.9 3.1 120 300 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i error (134) 0 wit inspect .17  .17  1.9  26 .0082 0     error (invalid witness file) .50 .32 9.8 41 error (invalid witness file) 6.9 3.6 89 300 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .24  .24  1.8  26 .0082 0     false(unreach-call) 5.1  2.8  58   290 false(unreach-call) 9.0 4.8 180 350 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900     900     9400    12000 .0082 0     error (invalid witness file) .52 .34 13   39 error (invalid witness file) 7.0 3.7 130 320 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .21  .21  2.4  28 .0082 0     false(unreach-call) 5.6  3.0  110   290 false(unreach-call) 8.9 4.7 170 350 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900     900     7400    7100 .0082 0     error (invalid witness file) .63 .39 7.7 40 error (invalid witness file) 5.7 3.0 93 300 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .23  .26  2.2  36 .0082 10     true 4.4  2.5  95   280 false(unreach-call) 8.1 4.4 160 320 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i error (8) 0 wit inspect .31  .31  3.2  29 .0082 0     error (invalid witness file) .50 .33 9.4 39 error (invalid witness file) 7.8 4.1 89 300 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i error (134) 0 wit inspect .20  .20  1.6  26 .0082 0     error (invalid witness file) .59 .39 8.7 40 error (invalid witness file) 5.9 3.1 86 300 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 330     330     3800    15000 .0082 0     - - error (invalid witness file) .53 .34 6.3 42 error (invalid witness file) 6.0 3.2 120 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .34  .34  3.2  30 .0082 0     - - error (invalid witness file) .65 .40 11   45 error (invalid witness file) 6.1 3.3 100 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    10000 .0082 0     - - error (invalid witness file) .50 .34 13   41 error (invalid witness file) 5.5 3.0 95 280
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    12000 .0082 0     - - error (invalid witness file) .69 .44 6.6 40 error (invalid witness file) 5.9 3.2 120 290
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     7400    9300 .0082 0     - - error (invalid witness file) .52 .32 12   39 error (invalid witness file) 6.0 3.2 110 290
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     7200    8900 .0082 0     - - error (invalid witness file) .67 .42 7.6 39 error (invalid witness file) 7.7 4.0 85 290
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .39  .38  3.9  31 .0082 0     - - error (invalid witness file) .53 .33 9.9 40 error (invalid witness file) 6.1 3.3 130 300
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (8) 0 wit inspect .27  .26  2.6  29 .0082 0     - - error (invalid witness file) .50 .32 13   41 error (invalid witness file) 5.8 3.0 110 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .33  .33  3.5  30 .0082 0     - - error (invalid witness file) .47 .31 10   40 error (invalid witness file) 6.2 3.3 110 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .28  .28  2.5  28 .0082 0     - - error (invalid witness file) .63 .40 10   42 error (invalid witness file) 6.1 3.2 110 310
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 340     340     3600    15000 .0082 0     - - error (invalid witness file) .54 .35 10   39 error (invalid witness file) 8.0 4.2 110 320
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .26  .26  2.1  29 .0082 0     - - error (invalid witness file) .48 .30 9.8 39 error (invalid witness file) 6.2 3.3 110 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .36  .35  3.1  29 .0082 0     - - error (invalid witness file) .51 .33 13   39 error (invalid witness file) 6.4 3.4 82 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     8700    10000 .0082 10     - - error (invalid witness file) .50 .33 8.3 43 error (invalid witness file) 7.0 3.7 100 310
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    12000 .0082 0     - - error (invalid witness file) .47 .32 10   39 error (invalid witness file) 5.9 3.1 97 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     8800    9500 .0082 0     - - error (invalid witness file) .67 .42 7.9 40 error (invalid witness file) 6.0 3.2 120 290
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     900     6300    6800 .0082 0     - - error (invalid witness file) .55 .34 10   40 error (invalid witness file) 7.4 3.9 76 290
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .40  .40  3.8  30 .0082 0     - - error (invalid witness file) .61 .40 8.1 39 error (invalid witness file) 5.7 3.1 120 300
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (8) 0 wit inspect .25  .24  3.0  28 .0082 0     - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 7.1 3.7 110 320
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .38  .38  3.9  30 .0082 0     - - error (invalid witness file) .64 .41 8.3 44 error (invalid witness file) 7.8 4.1 97 310
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .26  .26  2.9  28 .0082 0     - - error (invalid witness file) .62 .41 8.6 40 error (invalid witness file) 7.7 4.0 91 300
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .20  .20  2.3  27 .0082 .16  false(unreach-call) 5.1  2.8  94   280 false(unreach-call) 11   5.7 94 320 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i error (8) 0 wit inspect .52  .52  5.8  31 .0082 0     error (invalid witness file) .49 .34 7.4 39 error (invalid witness file) 6.4 3.4 110 300 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19  .18  1.7  26 .0082 0     false(unreach-call) 5.0  2.7  57   290 false(unreach-call) 8.3 4.3 170 320 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i error (8) 0 wit inspect .65  .65  7.1  34 .0082 0     error (invalid witness file) .55 .35 14   41 error (invalid witness file) 6.0 3.2 120 300 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i error (8) 0 wit inspect .59  .59  7.8  33 .0082 0     - - error (invalid witness file) .56 .36 9.6 40 error (invalid witness file) 6.1 3.2 110 300
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i error (8) 0 wit inspect .46  .46  4.7  31 .0082 0     error (invalid witness file) .47 .31 11   40 error (invalid witness file) 5.6 3.0 110 280 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i error (8) 0 wit inspect .44  .45  4.5  31 .0082 0     - - error (invalid witness file) .57 .37 11   39 error (invalid witness file) 7.6 4.0 66 300
list-ext2-properties/simple_search_value_false-unreach-call.i true -32 wit inspect 1.2   1.2   18    41 .0082 0     unknown 52    44    870   710 timeout 97   77   2400 1400 - -
list-ext2-properties/simple_search_value_true-unreach-call.i true 2 wit inspect 1.2   1.2   13    41 .0082 0     - - timeout 900    890    16000   1500 timeout 960   930   17000 2700
../../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 -370 20000   20000   210000 210000 .93  33    173 620 450 9400 21000   173 930 610 15000 31000   173 4500 4200 85000 32000   173 2900 2400 52000 47000  
    correct results 86 142 24   24   240 4100 .34  22    28 240 170 3800 8700   28 330 180 5400 17000   54 2100 1900 34000 24000   50 2500 2100 44000 24000  
        correct true 56 112 16   16   150 3200 .18  11    2 0 0 0 0   10 0 0 0 0   54 2100 1900 34000 24000   50 2500 2100 44000 24000  
        correct false 30 30 8.3 8.1 83 870 .15  11    26 240 170 3800 8700   18 330 180 5400 17000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 24 -512 12   11   130 1500 .098 .40 3 370 270 5200 11000   4 430 340 6800 6200   13 2400 2300 51000 6800   15 250 140 4400 13000  
        incorrect true 8 -256 8.3 8.3 95 1100 .057 0    0 370 270 5200 11000   0 430 340 6800 6200   12 0 0 0 0   15 0 0 0 0  
        incorrect false 16 -256 3.3 3.2 35 400 .041 .40 3 0 0 0 0   4 0 0 0 0   1 2400 2300 51000 6800   0 250 140 4400 13000  
score (173 tasks, max score: 280) -370
Run set sv-comp17.ReachSafety-Heap