Tool Forester
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-13 10:46:53 CET [[ 2017-01-15 01:19:51 CET ]] [[ 2017-01-15 01:22:27 CET ]] [[ 2017-01-15 01:21:29 CET ]] [[ 2017-01-15 01:24:32 CET ]]
Run set sv-comp17
Options --trace error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/forester.2017-01-13_1046.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/forester.2017-01-13_1046.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/forester.2017-01-13_1046.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/forester.2017-01-13_1046.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 .083 .083 .47 11   .0082 0      .53 .33 13   40 6.3 3.3 130 300
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 .053 .054 .64 11   .012  .090  .59 .38 14   45 5.8 3.1 120 290
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 0 .053 .054 .54 11   .0082 0      .54 .35 11   43 6.9 3.6 85 300
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 0 .28  .29  3.5  16   .037  .31   3.3  1.8  67   210 96   84   2600 880
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 0 .075 .076 .48 11   .0041 .061  .51 .33 11   40 6.2 3.3 120 300
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 0 .058 .058 .57 11   .0041 .061  .50 .33 11   40 6.7 3.6 100 300
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 .12  .14  .58 19   .0082 8.0    .53 .34 12   42 6.2 3.3 110 300
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 2 .086 .086 .94 15   .0082 0      5.0  2.7  91   320 730   700   20000 760
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 .056 .056 .60 11   .012  .061  .53 .34 14   42 6.0 3.1 140 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 .072 .073 .56 11   .0082 .32   .49 .31 10   40 6.7 3.5 140 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 1.3   1.3   14    55   .0082 8.3    3.3  1.8  51   230 9.3 4.9 180 330
heap-manipulation/tree_true-unreach-call.i 0 .098 .13  .66 18   .0041 7.9    .54 .34 13   39 6.2 3.2 110 300
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 1 .063 .063 .72 11   .0041 .061  3.1  1.7  50   180 9.0 4.8 200 340
list-properties/list_false-unreach-call_false-valid-memcleanup.i 0 2.3   930     840    38   .68   7.7    .61 .39 15   47 6.0 3.2 120 300
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 0 .050 .051 .52 10   .0041 0      .51 .32 13   40 5.8 3.0 130 300
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 0 .099 .10  1.1  14   .016  .31   2.8  1.5  58   180 91   57   1200 7000
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 1 .060 .061 .63 11   .0041 .25   3.0  1.6  70   180 8.3 4.4 150 330
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 1 .12  .12  1.3  13   .029  .19   2.9  1.6  60   180 10   5.3 210 350
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 2 .22  .26  2.3  24   .066  13      3.9  2.2  73   260 960   920   17000 2300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 .049 .050 .55 10   .0041 .061  .54 .35 13   42 5.9 3.1 110 300
list-properties/list_search_true-unreach-call_false-valid-memtrack.i 2 .24  .26  2.8  27   .0041 7.5    4.3  2.4  86   270 39   27   890 790
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 2.6   930     850    30   .64   0      .56 .35 12   42 5.7 3.1 120 290
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 2 .052 .052 .51 11   .0041 .061  .61 .38 15   45 5.8 3.1 110 290
list-properties/simple_true-unreach-call_false-valid-memtrack.i 2 .082 .082 .53 11   .0041 0      3.8  2.1  55   270 960   890   13000 2100
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 5.5   930     870    81   .73   7.7    .57 .37 12   44 6.8 3.6 130 300
ldv-regression/1_3.c_false-unreach-call.i 0 2.8   930     880    46   1.0    7.7    .56 .36 15   44 6.2 3.2 120 300
ldv-regression/alt_test.c_false-unreach-call.i 1 .060 .060 .61 11   .0041 0      3.1  1.7  72   180 10   5.4 190 360
ldv-regression/callfpointer.c_false-unreach-call.i 0 .066 .067 .43 10   .0041 .13   .55 .35 14   42 6.3 3.3 120 300
ldv-regression/fo_test.c_false-unreach-call.i 0 .067 .067 .50 10   .0041 0      .53 .33 11   41 5.6 3.0 120 300
ldv-regression/mutex_lock_int.c_false-unreach-call.i 0 .077 .11  .56 18   .0041 7.8    2.4  1.3  43   160 7.5 3.9 150 320
ldv-regression/mutex_lock_struct.c_false-unreach-call.i 0 .082 .082 .57 10   .0041 0      2.3  1.3  47   160 7.8 4.1 150 320
ldv-regression/recursive_list.c_false-unreach-call.i 0 .054 .054 .53 10   .0041 0      2.2  1.3  44   160 7.2 3.8 140 320
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i 0 .050 .051 .72 10   .0082 .0041 2.5  1.4  50   170 7.7 4.1 140 310
ldv-regression/rule60_list2.c_false-unreach-call_1.i 0 .055 .055 .65 10   .0041 0      2.6  1.5  57   180 7.8 4.1 140 330
ldv-regression/stateful_check_false-unreach-call.i 0 .055 .055 .56 11   .0082 0      .55 .35 11   43 5.9 3.1 110 300
ldv-regression/test_while_int.c_false-unreach-call.i 0 .079 .11  .57 18   .0041 7.8    2.2  1.2  36   160 9.2 4.9 180 340
ldv-regression/test_while_int.c_false-unreach-call_1.i 0 .051 .053 .50 11   .0041 .52   2.4  1.3  52   170 7.7 4.2 140 340
ldv-regression/alias_of_return.c_true-unreach-call.i 2 .077 .077 .68 12   .012  0      .66 .41 15   45 6.1 3.2 120 300
ldv-regression/alias_of_return.c_true-unreach-call_1.i 2 .084 .084 .55 12   .012  0      .64 .39 15   47 6.3 3.3 120 300
ldv-regression/alias_of_return_2.c_true-unreach-call.i 2 .087 .13  1.0  23   .012  12      .62 .38 13   44 5.8 3.1 120 300
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i 2 .090 .090 .60 12   .012  0      .56 .37 12   41 6.0 3.2 140 300
ldv-regression/ex3_forlist.c_true-unreach-call.i 0 .049 .049 .49 9.9 .0041 .0041 .60 .39 8.9 40 6.1 3.2 110 300
ldv-regression/just_assert.c_true-unreach-call.i 2 .10  .14  .69 22   .0082 12      3.2  1.8  38   260 7.0 3.7 130 310
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i 2 .067 .080 .78 16   .012  5.0    .55 .35 14   41 5.8 3.1 120 300
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i 2 .062 .077 .84 15   .012  4.8    .57 .36 14   43 6.7 3.5 130 300
ldv-regression/nested_structure.c_true-unreach-call.i 2 .082 .11  .82 19   .012  7.3    3.4  1.9  62   260 9.4 5.1 170 330
ldv-regression/nested_structure_noptr.c_true-unreach-call.i 2 .087 .087 .57 12   .012  0      3.7  2.0  70   270 7.0 3.7 130 310
ldv-regression/nested_structure_noptr_true-unreach-call.i 2 .087 .13  .74 23   .012  12      3.4  1.9  82   250 7.5 4.0 140 320
ldv-regression/nested_structure_ptr.c_true-unreach-call.i 2 .099 .14  .57 23   .012  12      3.9  2.1  75   270 13   7.0 180 440
ldv-regression/nested_structure_ptr_true-unreach-call.i 2 .062 .063 .72 12   .012  .26   3.7  2.1  76   260 12   6.9 210 470
ldv-regression/nested_structure_true-unreach-call.i 2 .062 .075 .85 15   .012  4.9    3.6  2.0  56   260 10   5.4 190 350
ldv-regression/oomInt.c_true-unreach-call.i 0 .061 .090 .63 18   .0041 7.9    .51 .33 12   42 6.3 3.3 110 300
ldv-regression/oomInt.c_true-unreach-call_1.i 0 .075 .077 .51 10   .0041 .45   .53 .34 12   41 5.9 3.1 140 290
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i 0 .071 .071 .54 10   .0082 0      2.2  1.3  42   170 8.1 4.3 140 320
ldv-regression/rule60_list.c_true-unreach-call.i 2 .065 .065 .72 12   .012  .13   4.5  2.5  96   280 11   6.0 200 360
ldv-regression/rule60_list2.c_true-unreach-call.i 0 .079 .079 .60 11   .0041 .12   2.6  1.5  42   170 7.6 4.1 160 320
ldv-regression/sizeofparameters_test.c_true-unreach-call.i 0 .082 .083 .45 10   .0041 .14   2.6  1.4  48   170 7.9 4.2 160 320
ldv-regression/structure_assignment.c_true-unreach-call.i 2 .060 .073 .77 16   .012  4.8    3.4  1.9  45   250 7.5 4.0 140 320
ldv-regression/test_address.c_true-unreach-call.i 2 .12  .13  .69 15   .012  4.9    .54 .34 13   41 6.3 3.3 110 300
ldv-regression/test_cut_trace.c_true-unreach-call.i 2 .058 .058 .82 12   .012  0      4.0  2.2  42   260 7.9 4.2 140 330
ldv-regression/test_malloc-1_true-unreach-call.i 2 .065 .067 .69 12   .012  0      4.7  2.6  100   270 8.2 4.4 170 330
ldv-regression/test_malloc-2_true-unreach-call.i 2 .062 .077 .97 16   .012  5.1    4.6  2.5  90   280 8.0 4.3 180 330
ldv-regression/test_overflow.c_true-unreach-call.i 2 .090 .090 .62 12   .012  0      4.7  2.5  59   270 8.0 4.2 160 330
ldv-regression/test_union.c_true-unreach-call.i 0 .047 .047 .49 9.9 .0041 0      .50 .33 12   41 6.0 3.2 120 290
ldv-regression/test_union.c_true-unreach-call_1.i 0 .074 .10  .55 17   .0041 7.6    .50 .32 11   40 5.7 3.1 120 290
ldv-regression/test_union_cast-1_true-unreach-call.i 0 .045 .045 .45 9.8 .0041 .0041 .52 .33 11   40 6.0 3.2 120 300
ldv-regression/test_union_cast-2_true-unreach-call.i 0 .065 .066 .44 10   .0041 .14   .54 .34 12   42 5.8 3.0 110 300
ldv-regression/test_union_cast.c_true-unreach-call.i 0 .077 .10  .51 17   .0041 7.7    .52 .33 12   45 5.5 3.0 110 290
ldv-regression/test_union_cast.c_true-unreach-call_1.i 0 .047 .047 .49 9.7 .0041 0      .49 .32 12   40 5.4 2.9 120 280
ldv-regression/volatile_alias.c_true-unreach-call.i 2 .099 .14  .67 23   .012  12      3.3  1.9  57   260 7.7 4.2 150 320
ldv-regression/volatile_alias.c_true-unreach-call_1.i 2 .060 .073 .81 15   .012  4.8    3.4  1.9  44   250 7.9 4.2 160 310
ldv-regression/test02_false-unreach-call.c 0 .046 .046 .55 10   .0041 0      2.2  1.3  45   160 7.5 3.9 140 310
ldv-regression/test06_false-unreach-call.c 0 .059 .062 .85 12   .0041 .88   2.4  1.4  40   160 9.1 4.9 170 330
ldv-regression/test08_false-unreach-call.c 0 .056 .056 .61 11   .0041 0      2.3  1.3  40   160 7.7 4.1 140 320
ldv-regression/test12_false-unreach-call.c 0 .049 .049 .50 10   .0041 0      2.2  1.2  49   150 7.4 3.9 150 320
ldv-regression/test21_false-unreach-call.c 0 .071 .098 .69 18   .0041 8.0    .49 .31 11   39 6.3 3.3 120 300
ldv-regression/test22_false-unreach-call.c 0 .048 .051 .59 11   .0041 .71   .48 .32 12   40 6.4 3.3 150 310
ldv-regression/test23_false-unreach-call.c 0 .050 .052 .51 11   .0041 .66   .49 .31 11   40 5.7 3.0 130 290
ldv-regression/test24_false-unreach-call.c 0 .085 .15  .67 28   .0041 18      .48 .30 11   39 6.2 3.2 120 300
ldv-regression/test25_false-unreach-call.c 0 .053 .053 .53 10   .0041 0      2.2  1.3  51   160 7.6 4.0 160 320
ldv-regression/test26_false-unreach-call.c 0 .051 .053 .52 10   .0041 0      2.2  1.2  47   160 7.6 4.0 130 320
ldv-regression/test27_false-unreach-call.c 0 .048 .048 .47 10   .0041 0      .50 .31 9.0 40 6.9 3.6 85 300
ldv-regression/test28_false-unreach-call.c 0 .051 .052 .51 10   .0041 .30   2.5  1.4  47   160 8.7 4.6 170 340
ldv-regression/test29_false-unreach-call.c 0 .058 .092 .65 18   .0041 8.0    .53 .33 13   40 6.3 3.3 96 300
ldv-regression/test30_false-unreach-call.c 0 2.2   930     950    32   .98   0      .56 .34 13   42 5.6 3.0 120 300
ldv-regression/test01_true-unreach-call.c 2 .074 .088 .68 15   .012  4.8    3.4  1.9  70   250 8.7 4.6 170 330
ldv-regression/test03_true-unreach-call.c 2 .11  .15  .79 23   .012  12      3.6  2.0  74   260 8.3 4.5 160 320
ldv-regression/test04_true-unreach-call.c 2 .13  .17  .65 23   .012  12      3.4  1.9  53   260 9.0 4.9 180 320
ldv-regression/test05_true-unreach-call.c 0 .060 .062 .70 12   .0041 .30   2.3  1.3  41   150 8.7 4.8 180 330
ldv-regression/test07_true-unreach-call.c 0 .056 .056 .56 11   .0041 0      2.3  1.3  41   160 11   6.2 190 370
ldv-regression/test09_true-unreach-call.c 0 .056 .087 .77 19   .0041 8.0    2.1  1.2  35   160 10   5.8 190 360
ldv-regression/test10_true-unreach-call.c 0 .080 .11  .57 18   .0041 7.7    .51 .32 10   39 6.1 3.2 130 300
ldv-regression/test11_true-unreach-call.c 0 .050 .050 .51 10   .0041 .12   .50 .30 11   39 6.9 3.6 130 320
ldv-regression/test13_true-unreach-call.c 2 .097 .14  .75 23   .012  12      3.3  1.9  56   260 8.0 4.2 170 320
ldv-regression/test14_true-unreach-call.c 0 .081 .11  .62 18   .0041 7.8    .54 .34 11   41 5.5 2.9 120 280
ldv-regression/test15_true-unreach-call.c 0 .049 .050 .49 10   .0041 .25   .49 .31 10   40 5.9 3.1 110 300
ldv-regression/test16_true-unreach-call.c 2 .086 .085 .62 12   .012  0      3.6  2.0  54   260 10   5.6 250 350
ldv-regression/test17_true-unreach-call.c 2 .081 .095 .72 16   .012  5.0    3.4  1.9  52   260 7.1 3.8 150 310
ldv-regression/test18_true-unreach-call.c 2 .063 .064 .65 12   .012  .12   3.4  1.9  54   260 9.3 5.0 170 320
ldv-regression/test19_true-unreach-call.c 0 .047 .047 .52 10   .0041 0      .50 .32 11   41 6.2 3.3 110 310
ldv-regression/test20_true-unreach-call.c 2 .089 .090 .59 12   .012  .14   3.5  1.9  79   260 7.2 3.9 150 320
ldv-regression/test21_true-unreach-call.c 0 .049 .049 .46 9.9 .0041 0      .49 .32 10   39 6.1 3.2 130 300
ldv-regression/test22_true-unreach-call.c 0 .084 .11  .60 18   .0041 8.0    .50 .33 11   40 5.9 3.2 120 300
ldv-regression/test23_true-unreach-call.c 0 .069 .099 .66 18   .0041 7.9    .57 .36 13   43 6.0 3.1 140 290
ldv-regression/test24_true-unreach-call.c 0 .076 .076 .41 10   .0041 0      .48 .31 11   39 6.1 3.2 120 300
ldv-regression/test25_true-unreach-call.c 0 .049 .049 .50 10   .0041 0      .54 .33 14   41 6.0 3.2 120 300
ldv-regression/test26_true-unreach-call.c 0 .053 .053 .56 10   .0041 0      2.4  1.3  50   160 9.8 5.3 190 350
ldv-regression/test27_true-unreach-call.c 0 .10  .13  .58 18   .0041 8.1    .53 .34 12   40 5.5 2.9 58 300
ldv-regression/test28_true-unreach-call.c 0 .046 .046 .54 10   .0041 0      .50 .32 11   40 5.7 3.0 110 300
ldv-regression/test29_true-unreach-call.c 0 .046 .047 .48 10   .0041 .25   .53 .33 13   40 6.0 3.2 130 300
ldv-regression/test30_true-unreach-call.c 0 2.0   930     860    33   1.0    0      .59 .37 13   42 6.2 3.3 120 290
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 0 .13  .16  1.6  26   .11   8.3    .52 .33 12   43 6.2 3.3 120 290
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 0 .13  .13  1.5  17   .11   0      .49 .31 5.6 40 5.6 3.0 69 290
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 0 .14  .14  1.3  17   .11   0      .52 .34 13   42 6.5 3.4 120 290
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 0 .13  .15  1.8  26   .11   8.3    .50 .33 11   40 6.4 3.4 130 300
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 0 .15  .18  1.4  26   .11   8.3    .50 .32 12   40 6.5 3.4 120 310
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 0 .14  .14  1.5  18   .11   .32   .55 .36 12   43 6.7 3.6 130 310
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 0 .15  .15  1.6  18   .11   .88   .54 .34 13   40 5.8 3.2 110 290
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 0 .14  .14  1.5  17   .11   0      .49 .32 10   39 6.5 3.4 110 300
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 0 .15  .17  1.6  26   .11   8.3    .51 .33 12   42 7.0 3.7 140 310
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 0 .12  .12  1.3  17   .11   .20   .52 .33 11   41 7.0 3.7 150 320
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 0 .14  .18  1.5  26   .11   8.3    .51 .32 8.9 40 5.9 3.2 120 290
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 0 .15  .18  1.6  25   .11   8.3    .51 .32 12   40 5.9 3.1 130 280
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 0 .12  .12  1.4  17   .11   .20   .52 .32 12   40 6.5 3.4 120 310
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 1 .094 .094 1.1  13   .025  0      3.0  1.7  53   170 16   8.4 310 550
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 1 .090 .12  .82 18   .0041 7.8    3.1  1.7  56   180 19   10   380 410
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 1 .071 .072 .66 11   .0041 .13   3.0  1.6  38   180 10   5.4 190 380
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 1 1.2   1.2   16    25   .090  .0082 3.3  1.9  47   170 15   7.7 270 560
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .073 .10  .60 18   .0041 7.6    2.7  1.5  46   170 11   5.5 210 360
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 1 .41  .41  4.4  19   .094  0      3.0  1.7  51   180 11   5.8 220 300
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .071 .072 .79 12   .012  0      3.0  1.6  61   180 10   5.3 220 350
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 1 .10  .13  .90 20   .0041 7.7    2.9  1.6  51   170 15   7.6 270 450
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 1 .057 .086 .71 19   .0041 7.8    3.0  1.6  63   180 11   5.7 190 370
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 0 .089 .12  .93 20   .016  7.8    3.0  1.6  46   180 23   13   320 800
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 1 .085 .086 .77 12   .0041 0      2.9  1.6  35   180 13   6.5 200 410
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 1 .058 .058 .59 11   .0041 0      3.0  1.6  71   180 17   9.2 250 420
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 1 .056 .059 .59 11   .0041 .13   2.9  1.6  62   180 11   5.7 210 390
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 1 .13  .13  1.5  14   .029  .0082 3.1  1.7  50   180 13   7.0 210 540
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .070 .071 .56 11   .0041 0      2.9  1.6  52   180 11   5.6 200 380
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 1 .31  .34  3.1  25   .057  7.7    3.4  1.8  47   170 10   5.5 220 300
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .068 .068 .87 12   .012  .074  2.7  1.5  35   170 9.4 5.0 180 350
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 1 .15  .15  1.4  13   .053  0      3.0  1.6  52   180 74   43   1100 7000
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 1 .071 .073 .52 11   .0041 0      2.8  1.5  54   180 10   5.5 180 360
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 2 .51  .51  6.8  29   .041  0      4.1  2.2  62   280 960   910   15000 1100
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 2 30     30     370    130   .27   .18   4.1  2.3  69   270 960   890   26000 1200
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 2 1.3   1.3   17    42   .041  .13   4.0  2.2  58   270 960   870   14000 2400
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 2 10     10     120    78   .26   .14   3.9  2.1  51   270 960   870   19000 1900
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 2 1.4   1.5   17    44   .094  13      4.3  2.4  81   270 960   860   14000 1600
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 2 1.3   1.3   15    37   .098  0      3.9  2.1  48   280 11   5.8 230 310
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 2 140     140     1600    490   .57   12      4.0  2.2  58   270 960   910   21000 1700
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 2 1.7   1.7   20    45   .078  7.8    3.8  2.1  49   260 960   880   18000 2400
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 2 120     120     1300    450   .37   4.2    4.2  2.3  80   280 960   860   24000 1700
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 2 .12  .12  1.3  14   .025  0      4.1  2.2  77   270 960   890   19000 2200
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 2 .89  .90  12    39   .053  5.0    4.1  2.2  75   270 960   910   20000 1100
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 2 680     680     8100    1600   3.1    0      4.6  2.5  84   270 960   890   17000 1100
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 2 2.1   2.1   28    47   .082  4.8    4.3  2.3  95   270 960   870   23000 1700
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 2 .93  .93  13    35   .033  0      4.0  2.2  51   270 960   890   15000 1600
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 2 17     17     200    99   .30   13      4.1  2.2  54   270 960   910   17000 1800
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 2 6.0   6.0   71    52   .21   0      3.9  2.1  66   260 960   890   20000 2200
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 2 .49  .53  5.9  30   .061  13      3.9  2.1  55   270 11   5.9 260 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 2 4.3   4.3   61    66   .38   0      4.2  2.3  79   270 960   920   24000 1400
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 2 .66  .66  8.2  24   .074  .29   4.0  2.2  58   270 960   870   24000 1900
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 2 190     190     2900    360   .45   .0082 4.0  2.1  47   270 960   900   13000 2000
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 2 .14  .14  1.7  14   .049  0      4.2  2.3  70   270 960   900   16000 2600
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 .081 .082 .89 12   .016  .061  2.8  1.5  42   170 10   5.4 190 360
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 .057 .058 .59 11   .0041 .11   2.9  1.6  56   180 8.2 4.4 180 330
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i 1 .053 .053 .52 11   .0041 0      2.8  1.6  61   170 9.2 4.9 170 330
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i 0 5.2   930     890    67   .91   7.9    .56 .35 13   44 6.1 3.3 120 320
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i 0 6.6   930     950    73   .98   7.8    .57 .38 12   43 5.9 3.2 120 300
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 1 .11  .14  .90 21   .0082 7.9    3.0  1.7  63   200 8.6 4.6 160 330
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 2 .59  .59  6.9  31   .0082 .061  4.0  2.2  83   260 960   890   26000 3600
list-ext2-properties/simple_search_value_false-unreach-call.i 0 2.4   930     840    52   .97   7.8    .64 .40 17   45 6.1 3.2 140 300
list-ext2-properties/simple_search_value_true-unreach-call.i 0 2.6   930     870    52   1.0    7.8    .58 .37 14   42 6.3 3.4 140 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 139 1200   11000   24000 6300 18    550 173 130 74 2500 8400   173 820 480 15000 37000   173 240 130 4200 17000   173 23000 21000 440000 69000  
local summary 1100  
    correct results 82 139 1200   1200   15000 4700 7.6  290 0 74 41 1300 4500   22 350 190 6300 16000   23 200 110 3400 13000   25 22000 20000 440000 54000  
        correct true 57 114 1200   1200   15000 4300 7.1  240 0 0 0 0 0   0 0 0 0 0   23 200 110 3400 13000   25 22000 20000 440000 54000  
        correct false 25 25 3.7 3.9 42 370 .48 47 0 74 41 1300 4500   22 350 190 6300 16000   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) 139
Run set sv-comp17