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