Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.2  8.2  69   490 1.8  0      timeout 92    83    2200   470 true 10   5.6 120 320 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.8  3.8  47   400 3.7  0      true 9.2  4.9  110   320 true 8.8 4.7 140 330 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.9  1.9  28   240 3.5  .12   false(unreach-call) 7.0  3.7  98   310 true 9.5 5.1 140 350 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.3  1.3  16   410 .86 0      false(unreach-call) 7.3  4.0  120   330 true 11   5.6 120 320 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 1.4  1.4  18   190 3.5  0      false(unreach-call) 7.6  4.2  90   300 true 8.1 4.3 150 320 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.4  1.4  19   190 3.5  0      timeout 92    83    1800   480 true 8.8 4.7 110 320 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    8000   930 5.1  0      - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.9 3.1 63 300
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    13000   200 62    0      - - error (invalid witness file) .54 .35 8.2 39 error (invalid witness file) 6.1 3.3 130 290
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9400   690 15    0      - - error (invalid witness file) .62 .39 8.0 39 error (invalid witness file) 5.8 3.1 87 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   840 11    0      - - error (invalid witness file) .55 .35 9.3 39 error (invalid witness file) 5.7 3.0 72 310
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9800   410 15    0      - - error (invalid witness file) .64 .41 9.4 42 error (invalid witness file) 6.5 3.4 130 300
heap-manipulation/tree_true-unreach-call.i unknown 0 wit inspect 890    900    9100   200 25    0      - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 7.0 3.7 97 300
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.5  1.4  21   190 4.3  .78   false(unreach-call) 6.0  3.2  120   300 false(unreach-call) 8.5 4.5 94 360 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.4  1.4  17   240 3.5  .045  timeout 91    85    2200   460 true 9.4 5.0 100 320 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.2  1.2  14   180 3.4  .45   false(unreach-call) 6.9  3.7  79   320 true 11   5.5 110 330 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 2.7  2.6  37   100 8.6  0      false(unreach-call) 5.6  3.1  110   290 true 15   8.2 170 430 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.3  1.4  16   190 3.4  34      false(unreach-call) 5.8  3.2  99   290 true 6.8 3.6 80 320 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.5  1.7  22   250 4.3  35      false(unreach-call) 6.6  3.6  83   300 true 7.9 4.3 150 320 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    11000   510 210    .10   - - error (invalid witness file) .54 .35 12   41 error (invalid witness file) 6.2 3.2 130 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    9700   340 160    .10   - - error (invalid witness file) .68 .43 7.7 40 error (invalid witness file) 5.4 2.9 71 300
list-properties/list_search_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 33    33    300   490 11    0      - - true 27    15    440   690 true 38   26   400 870
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    11000   260 37    0      - - error (invalid witness file) .50 .33 8.4 40 error (invalid witness file) 5.9 3.1 69 300
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    13000   220 130    0      - - error (invalid witness file) .64 .41 8.5 42 error (invalid witness file) 5.8 3.1 120 290
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    10000   430 190    .045  - - error (invalid witness file) .66 .43 7.5 42 error (invalid witness file) 5.4 2.9 66 290
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    10000   210 84    .10   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.7 3.0 71 300
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect .47 .47 5.5 49 .85 0      false(unreach-call) 4.1  2.3  84   280 true 8.1 4.3 140 330 - -
ldv-regression/alt_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.3  4.3  33   460 .85 0      exception 4.7  2.5  72   290 false(unreach-call) 8.8 4.8 160 350 - -
ldv-regression/callfpointer.c_false-unreach-call.i unknown 0 wit inspect 16    16    220   30 84    .0041 error (invalid witness file) .62 .40 7.8 39 error (invalid witness file) 6.8 3.6 77 290 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .53 .53 6.1 29 .85 .10   exception 4.7  2.5  71   280 unknown 15   8.1 330 350 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .39 .38 4.4 49 .85 0      true 4.6  2.5  46   270 false(unreach-call) 6.5 3.5 71 310 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect .37 .37 4.1 49 .85 0      false(unreach-call) 4.5  2.5  57   280 false(unreach-call) 11   5.7 100 340 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect .57 .57 8.1 49 .85 0      false(unreach-call) 5.4  3.0  61   280 true 7.7 4.1 100 310 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect .42 .42 4.8 50 .85 0      false(unreach-call) 4.6  2.5  83   280 true 7.4 4.0 150 310 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 5.0  5.0  42   430 .85 0      exception 2.8  1.5  45   180 false(unreach-call) 13   7.1 130 360 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect 2.1  2.1  25   77 8.5  0      false(unreach-call) 11    5.7  120   360 true 7.4 4.0 160 320 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 1.5  1.5  21   75 6.8  0      false(unreach-call) 4.0  2.2  77   280 false(unreach-call) 6.9 3.7 140 310 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 1.5  1.5  17   75 6.8  0      false(unreach-call) 4.8  2.7  45   270 false(unreach-call) 8.0 4.4 130 340 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect 3.8  2.1  32   310 3.4  33      - - true 3.3  1.8  54   250 true 8.4 4.4 130 330
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect 3.4  1.9  33   260 3.4  0      - - true 4.1  2.3  49   260 true 7.6 4.0 79 320
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect 3.7  1.9  36   270 3.4  0      - - true 4.3  2.4  49   260 true 8.2 4.5 160 330
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect 3.6  1.9  37   270 3.4  0      - - true 3.6  2.0  54   250 true 8.6 4.6 99 310
ldv-regression/ex3_forlist.c_true-unreach-call.i true 2 wit inspect 4.2  2.6  42   280 5.9  0      - - true 20    11    320   540 true 29   17   400 690
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect 3.0  1.7  34   230 3.4  .0041 - - true 3.7  2.1  49   250 true 6.7 3.5 75 320
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect 3.9  2.2  33   300 3.4  33      - - true 3.7  2.1  49   260 true 8.5 4.5 130 320
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect 3.7  2.0  35   260 3.4  0      - - true 3.7  2.1  68   260 true 8.2 4.4 150 310
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect 3.9  2.0  38   270 3.4  .14   - - true 4.0  2.2  45   250 true 9.3 5.0 110 330
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect 3.0  1.7  28   250 3.4  0      - - true 4.0  2.2  57   260 true 7.5 4.0 150 310
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect 3.0  1.7  30   250 3.4  0      - - true 3.4  1.9  73   260 true 8.3 4.4 140 340
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect 3.9  2.0  39   270 3.4  0      - - true 3.7  2.1  49   250 true 11   6.1 140 420
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect 3.7  2.0  37   270 3.4  .0041 - - true 4.7  2.6  42   270 true 13   7.0 150 470
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect 3.8  2.0  39   270 3.4  0      - - true 4.3  2.4  57   260 true 9.8 5.3 160 340
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect 3.2  1.7  33   270 3.4  0      - - true 3.3  1.9  51   260 true 7.6 4.1 93 320
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect 3.1  1.7  30   270 3.4  0      - - true 3.6  2.0  56   260 true 8.1 4.3 70 310
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect 3.6  1.9  31   270 3.4  .0041 - - true 4.1  2.3  72   260 true 9.6 5.1 170 350
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect 5.5  2.8  52   300 3.5  .0041 - - true 5.2  2.8  80   280 true 11   6.0 160 360
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect 9.0  7.5  96   410 3.4  0      - - true 5.9  3.2  66   260 true 28   16   510 700
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect 3.4  1.9  31   270 3.4  0      - - true 5.3  2.9  59   270 true 7.4 3.9 120 330
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect 3.4  1.9  34   260 3.4  0      - - true 4.3  2.4  50   260 true 7.3 3.9 89 320
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect 5.1  2.7  50   280 3.4  .0041 - - true 4.9  2.7  62   260 true 7.2 3.9 130 320
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect 3.1  1.7  32   260 3.4  0      - - true 3.7  2.1  62   260 true 7.9 4.2 160 320
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect 5.1  2.8  53   280 3.4  0      - - true 5.2  2.9  83   260 true 7.1 3.9 64 320
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect 5.0  2.7  51   280 3.4  0      - - true 5.9  3.2  53   260 true 8.4 4.5 140 320
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect .95 .94 11   48 3.4  0      - - true 5.7  3.0  81   260 true 8.0 4.3 110 320
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect 3.0  1.7  29   250 3.4  0      - - true 3.2  1.8  49   260 true 6.9 3.7 65 310
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect 3.2  1.7  31   270 3.4  0      - - true 3.7  2.1  49   260 true 7.6 4.1 110 320
ldv-regression/test_union_cast-1_true-unreach-call.i true 2 wit inspect 3.1  1.7  30   250 3.4  0      - - true 3.4  1.9  60   260 unknown 5.6 3.0 89 300
ldv-regression/test_union_cast-2_true-unreach-call.i true 2 wit inspect 3.6  1.9  36   280 3.4  .0041 - - true 3.5  2.0  73   260 unknown 6.0 3.2 110 310
ldv-regression/test_union_cast.c_true-unreach-call.i true 2 wit inspect 3.6  1.9  35   270 3.4  0      - - true 3.4  1.9  53   260 unknown 7.2 3.8 79 310
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2 wit inspect 3.3  2.0  28   290 3.4  34      - - true 3.4  1.9  44   260 unknown 6.2 3.3 79 310
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect 3.6  1.9  32   280 3.4  .0041 - - true 4.6  2.5  49   270 true 7.9 4.3 120 320
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect 3.6  1.9  34   270 3.4  0      - - true 4.3  2.4  46   260 true 7.6 4.1 120 330
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect .36 .36 4.5 48 .85 0      false(unreach-call) 3.7  2.1  67   280 false(unreach-call) 8.4 4.4 110 310 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect .38 .38 4.2 49 .85 0      true 4.3  2.4  67   270 false(unreach-call) 8.9 4.7 140 320 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect .36 .36 4.9 49 .85 0      true 4.2  2.3  79   280 false(unreach-call) 7.7 4.1 170 320 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect .37 .37 4.5 27 .85 0      true 4.2  2.3  52   270 false(unreach-call) 7.2 3.8 110 330 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect .37 .37 4.1 40 .85 0      false(unreach-call) 5.1  2.8  57   270 true 7.6 4.0 120 320 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .39 .39 4.4 66 .85 0      false(unreach-call) 4.8  2.6  73   280 true 7.9 4.2 150 320 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 16    16    200   66 29    0      true 12    7.5  200   320 true 8.9 4.7 120 310 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 1.3  1.3  17   100 4.3  0      false(unreach-call) 18    14    270   500 false(unreach-call) 42   28   660 1900 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect 6.7  6.6  74   76 27    0      true 4.4  2.4  69   280 false(unreach-call) 21   12   230 540 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect .37 .37 4.3 49 .85 0      true 3.6  2.0  68   280 false(unreach-call) 7.2 3.8 130 320 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect .70 .69 7.8 78 1.7  0      false(unreach-call) 4.8  2.7  60   280 true 7.5 4.0 150 330 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect .39 .39 4.2 49 .85 0      false(unreach-call) 4.0  2.2  62   280 false(unreach-call) 9.4 5.0 130 340 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect .38 .37 4.9 49 .85 0      false(unreach-call) 4.1  2.3  85   270 false(unreach-call) 10   5.4 130 340 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect .35 .35 4.9 48 .85 0      true 3.6  2.0  75   270 false(unreach-call) 8.0 4.3 120 320 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect 3.4  1.9  32   260 3.4  0      - - true 3.8  2.2  35   260 true 6.9 3.7 62 320
ldv-regression/test03_true-unreach-call.c true 2 wit inspect 3.7  2.0  34   280 3.4  0      - - true 4.6  2.6  45   260 true 9.2 4.9 110 320
ldv-regression/test04_true-unreach-call.c true 2 wit inspect 3.4  1.9  34   260 3.4  0      - - true 3.5  1.9  67   260 true 7.9 4.3 90 320
ldv-regression/test05_true-unreach-call.c true 2 wit inspect 4.1  2.0  38   280 3.4  0      - - true 3.9  2.2  64   260 true 14   7.8 210 530
ldv-regression/test07_true-unreach-call.c true 2 wit inspect 3.9  2.1  37   280 3.4  0      - - true 4.4  2.5  50   260 true 12   6.6 250 450
ldv-regression/test09_true-unreach-call.c true 2 wit inspect 4.0  2.0  37   270 3.4  0      - - true 3.4  1.9  48   260 true 12   6.8 140 430
ldv-regression/test10_true-unreach-call.c true 2 wit inspect 3.9  2.1  35   270 3.4  0      - - true 4.4  2.5  40   260 true 16   9.4 140 500
ldv-regression/test11_true-unreach-call.c true 2 wit inspect 3.8  2.0  34   270 3.4  0      - - true 3.7  2.1  73   260 true 8.9 4.8 140 320
ldv-regression/test13_true-unreach-call.c true 2 wit inspect 3.7  2.0  35   280 3.4  0      - - true 4.1  2.3  45   250 true 7.1 3.8 91 310
ldv-regression/test14_true-unreach-call.c true 2 wit inspect 3.8  2.0  37   270 3.4  0      - - true 4.4  2.5  49   260 true 8.5 4.5 84 320
ldv-regression/test15_true-unreach-call.c true 2 wit inspect 3.5  1.9  32   270 3.4  0      - - true 4.2  2.3  52   260 true 9.5 5.2 96 340
ldv-regression/test16_true-unreach-call.c true 2 wit inspect 3.6  1.9  34   270 3.4  0      - - true 4.1  2.4  44   260 true 10   5.5 170 350
ldv-regression/test17_true-unreach-call.c true 2 wit inspect 3.4  1.9  36   260 3.4  0      - - true 3.7  2.1  58   260 true 7.9 4.2 130 320
ldv-regression/test18_true-unreach-call.c true 2 wit inspect 3.6  1.9  37   280 3.4  0      - - true 4.5  2.5  46   260 true 11   5.7 170 350
ldv-regression/test19_true-unreach-call.c true 2 wit inspect 3.8  2.0  34   280 3.4  .0041 - - true 3.6  2.0  62   260 true 11   6.1 180 450
ldv-regression/test20_true-unreach-call.c true 2 wit inspect 3.7  1.9  30   270 3.4  0      - - true 4.2  2.3  42   260 true 7.8 4.1 57 330
ldv-regression/test21_true-unreach-call.c true 2 wit inspect 4.0  2.3  38   310 3.4  34      - - true 3.6  2.0  58   260 true 11   6.1 120 340
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 6.7  4.0  74   290 3.4  0      - - true 7.5  4.4  92   310 true 37   24   510 640
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 21    15    220   420 3.4  0      - - true 11    8.1  260   400 timeout 960   830   10000 2200
ldv-regression/test24_true-unreach-call.c true 2 wit inspect 43    40    540   490 4.2  0      - - true 5.6  3.3  100   300 true 17   9.1 160 380
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 220    210    1600   1200 4.3  0      - - true 30    24    440   490 true 26   14   300 670
ldv-regression/test26_true-unreach-call.c true 2 wit inspect 3.7  2.0  31   260 3.4  0      - - true 3.7  2.1  68   260 true 9.7 5.3 170 330
ldv-regression/test27_true-unreach-call.c true 2 wit inspect 16    12    190   360 4.2  .0041 - - exception 4.2  2.4  76   280 true 580   560   15000 1100
ldv-regression/test28_true-unreach-call.c true 2 wit inspect 3.7  2.0  39   270 3.4  .0041 - - true 3.5  1.9  63   260 true 10   5.4 130 320
ldv-regression/test29_true-unreach-call.c true 2 wit inspect 3.9  2.0  40   270 3.4  .0041 - - true 3.5  2.0  75   260 true 8.6 4.6 120 330
ldv-regression/test30_true-unreach-call.c true 2 wit inspect 3.6  2.0  33   280 3.4  0      - - true 3.6  2.0  71   260 true 11   6.0 150 460
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9700   1400 18    0      error (invalid witness file) .58 .36 11   42 error (invalid witness file) 6.3 3.3 100 300 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   940 18    34      error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.6 3.5 72 320 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9300   1200 18    0      error (invalid witness file) .59 .37 9.7 40 error (invalid witness file) 6.3 3.3 82 310 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    8000   1200 39    .10   - - error (invalid witness file) .53 .33 13   41 error (invalid witness file) 6.0 3.2 81 300
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    7300   1200 39    .21   - - error (invalid witness file) .54 .34 9.8 42 error (invalid witness file) 6.0 3.2 75 310
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    7200   1200 39    .10   - - error (invalid witness file) .66 .42 7.3 45 error (invalid witness file) 6.6 3.4 110 310
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    7100   1200 39    .13   - - error (invalid witness file) .51 .35 8.6 40 error (invalid witness file) 6.1 3.2 110 300
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    7900   1200 37    0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.8 3.6 110 290
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    8000   1200 37    .10   - - error (invalid witness file) .59 .37 9.6 40 error (invalid witness file) 6.4 3.4 100 300
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    9700   1300 41    .020  - - error (invalid witness file) .63 .40 7.9 39 error (invalid witness file) 6.2 3.3 100 300
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    7900   1300 39    35      - - error (invalid witness file) .57 .36 11   43 error (invalid witness file) 7.3 3.8 68 320
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    7900   1200 39    .55   - - error (invalid witness file) .50 .33 12   41 error (invalid witness file) 6.3 3.4 74 300
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    7900   1200 39    0      - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.5 3.4 140 300
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.2  1.2  16   160 1.7  0      timeout 92    82    1400   480 true 8.4 4.5 150 320 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .81 .81 11   130 1.7  0      false(unreach-call) 5.1  2.8  96   290 true 9.6 5.2 190 360 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .69 .68 8.7 130 .86 0      false(unreach-call) 5.5  3.0  65   290 true 9.1 4.8 140 350 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.5  3.5  51   140 9.5  0      timeout 91    87    3200   470 true 7.8 4.2 130 310 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 2.3  2.3  6.8 130 .86 0      false(unreach-call) 6.5  3.5  68   290 true 8.3 4.4 120 330 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect 1.8  1.8  23   130 3.5  0      false(unreach-call) 5.9  3.2  71   290 error 13   7.0 110 310 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .70 .70 8.4 190 .86 0      false(unreach-call) 7.3  3.9  72   300 true 7.8 4.2 110 320 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.8  1.8  21   220 4.3  0      timeout 92    83    2100   470 true 11   5.9 110 330 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .72 .71 7.9 130 .86 0      false(unreach-call) 5.1  2.8  97   290 true 10   5.4 120 320 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 2.1  2.1  25   160 4.4  0      false(unreach-call) 6.9  3.7  110   300 true 8.3 4.5 140 320 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.7  1.7  19   190 3.5  0      timeout 91    83    1800   450 true 12   6.1 100 330 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .81 .81 9.7 130 1.7  0      false(unreach-call) 6.0  3.3  74   290 true 9.2 5.0 120 340 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .67 .67 7.7 130 .86 0      false(unreach-call) 5.5  3.0  100   290 true 11   5.6 110 320 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.4  3.4  45   140 9.4  0      timeout 91    86    2100   450 true 9.6 5.1 120 320 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .56 .56 6.3 130 .86 0      false(unreach-call) 5.7  3.1  76   280 true 9.3 5.0 160 350 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.5  1.5  21   130 3.5  0      false(unreach-call) 5.7  3.1  87   280 error 14   7.5 140 310 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .69 .69 8.2 190 .86 0      false(unreach-call) 5.6  3.1  110   290 true 8.3 4.4 150 320 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.8  1.8  21   210 4.3  0      true 6.6  3.6  82   290 true 9.3 4.9 120 320 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .70 .69 8.8 130 .86 0      false(unreach-call) 5.9  3.2  84   300 true 8.0 4.3 190 320 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    11000   540 61    0      - - error (invalid witness file) .54 .34 9.8 40 error (invalid witness file) 5.8 3.1 94 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   210 83    0      - - error (invalid witness file) .57 .36 10   40 error (invalid witness file) 6.6 3.5 140 320
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    11000   480 93    0      - - error (invalid witness file) .64 .42 7.8 39 error (invalid witness file) 5.9 3.2 81 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    13000   920 220    0      - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 5.9 3.1 80 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    8500   280 21    .13   - - error (invalid witness file) .51 .33 13   44 error (invalid witness file) 6.6 3.4 77 310
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   410 19    34      - - error (invalid witness file) .61 .39 8.7 40 error (invalid witness file) 5.5 3.0 91 290
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    12000   190 31    0      - - error (invalid witness file) .57 .37 7.9 43 error (invalid witness file) 8.0 4.2 90 340
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    11000   190 52    0      - - error (invalid witness file) .63 .41 8.3 40 error (invalid witness file) 5.7 3.1 84 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   220 45    0      - - error (invalid witness file) .54 .34 12   41 error (invalid witness file) 5.5 3.0 100 280
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    12000   280 90    0      - - error (invalid witness file) .64 .40 8.6 40 error (invalid witness file) 5.5 3.0 81 290
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    12000   630 70    0      - - error (invalid witness file) .70 .45 6.9 39 error (invalid witness file) 6.1 3.2 100 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    9300   190 24    0      - - error (invalid witness file) .74 .47 7.6 44 error (invalid witness file) 5.6 3.0 49 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    12000   190 88    0      - - error (invalid witness file) .65 .41 7.6 41 error (invalid witness file) 5.4 2.9 61 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9800   520 100    0      - - error (invalid witness file) .50 .32 10   41 error (invalid witness file) 6.3 3.3 110 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    11000   940 250    0      - - error (invalid witness file) .51 .33 11   42 error (invalid witness file) 5.9 3.2 90 310
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   190 29    0      - - error (invalid witness file) .65 .41 7.5 39 error (invalid witness file) 6.6 3.5 76 310
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9600   200 26    0      - - error (invalid witness file) .69 .43 7.0 42 error (invalid witness file) 6.0 3.2 120 290
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   190 39    0      - - error (invalid witness file) .56 .36 7.9 40 error (invalid witness file) 5.8 3.1 66 300
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    9900   190 75    0      - - error (invalid witness file) .64 .39 11   41 error (invalid witness file) 5.7 3.0 70 290
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    12000   220 63    0      - - error (invalid witness file) .65 .43 8.0 41 error (invalid witness file) 6.2 3.3 83 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    11000   340 120    0      - - error (invalid witness file) .50 .33 9.9 40 error (invalid witness file) 5.7 3.0 52 300
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .98 1.1  11   300 1.7  34      false(unreach-call) 6.2  3.3  83   290 true 7.9 4.2 97 330 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 15    15    210   190 30    .45   timeout 97    81    1600   2400 true 8.8 4.7 110 330 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .81 .80 9.7 180 1.7  0      false(unreach-call) 6.7  3.7  61   290 false(unreach-call) 11   5.7 91 340 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i false(unreach-call) 1 wit inspect 1.9  1.9  25   350 3.5  .10   timeout 92    84    1300   480 true 8.1 4.3 140 320 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i unknown 0 wit inspect 890    900    9900   360 17    .10   - - error (invalid witness file) .56 .36 13   45 error (invalid witness file) 6.1 3.3 110 300
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect 1.5  1.5  16   270 3.5  0      false(unreach-call) 9.1  4.8  93   310 true 9.8 5.3 110 320 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i unknown 0 wit inspect 890    900    11000   270 30    .10   - - error (invalid witness file) .61 .39 7.4 39 error (invalid witness file) 5.9 3.1 96 290
list-ext2-properties/simple_search_value_false-unreach-call.i false(unreach-call) 1 wit inspect 9.1  9.0  130   160 30    .10   timeout 92    86    1800   600 timeout 97   74   1300 1300 - -
list-ext2-properties/simple_search_value_true-unreach-call.i unknown 0 wit inspect 900    900    9800   560 220    .12   - - error (invalid witness file) .63 .41 8.8 40 error (invalid witness file) 5.9 3.1 82 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 184 45000 44000 500000 57000 3800 340 173 1300 1100 26000 22000   173 730 420 10000 24000   173 350 210 5200 19000   173 2500 1900 38000 39000  
    correct results 123 184 670 550 6500 28000 490 240 48 1300 1100 26000 22000   58 700 400 9900 23000   60 320 190 4800 17000   56 2200 1800 34000 26000  
        correct true 61 122 540 420 4900 18000 220 130 10 0 0 0 0   40 0 0 0 0   60 320 190 4800 17000   56 2200 1800 34000 26000  
        correct false 62 62 130 130 1600 9600 270 100 38 1300 1100 26000 22000   18 700 400 9900 23000   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) 184
Run set sv-comp17.ReachSafety-Heap