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-13 04:51:53 CET [[ 2017-01-15 00:05:22 CET ]] [[ 2017-01-15 00:31:32 CET ]] [[ 2017-01-15 00:11:25 CET ]] [[ 2017-01-15 00:39:18 CET ]]
Run set [sv-comp17.MemSafety-Arrays; sv-comp17.MemSafety-Heap; sv-comp17.MemSafety-LinkedLists; sv-comp17.MemSafety-Other]
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status 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)
array-memsafety/add_last_unsafe_false-valid-deref.i false(valid-deref) .50 .49 6.9 29 .99 0      false(valid-deref) 4.6  2.5  92   260 true 7.7 4.2 120 330 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) .36 .36 3.8 28 .84 0      timeout 93    70    1000   4400 true 7.6 4.1 170 320 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) .55 .55 6.3 29 .84 0      true 4.1  2.2  44   260 true 9.1 4.8 130 340 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) .33 .32 4.1 28 .99 0      true 3.5  2.0  54   250 false(valid-deref) 7.3 3.9 100 330 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) .36 .36 4.2 29 .84 0      false(valid-deref) 4.8  2.6  72   260 true 8.6 4.7 110 360 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) .37 .37 4.3 29 .84 0      error 4.1  2.2  68   270 true 7.5 4.0 140 320 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) .36 .35 3.8 28 .99 0      true 3.3  1.9  63   260 false(valid-deref) 8.3 4.4 170 330 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) .36 .36 3.8 28 .99 0      true 3.5  2.0  61   260 true 8.0 4.3 100 310 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) .35 .35 4.5 29 .99 0      error 4.2  2.3  68   260 true 7.4 4.0 130 310 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) .35 .35 3.7 28 .84 0      timeout 95    75    1100   3900 false(valid-deref) 7.5 4.1 110 330 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) .88 .88 12   29 .84 0      error 5.5  2.9  49   260 true 16   9.0 210 440 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) .73 .72 7.9 29 .99 0      error 5.2  2.8  55   270 false(valid-deref) 11   5.7 130 370 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) .64 .63 8.8 29 .99 0      true 4.8  2.6  59   260 true 8.8 4.8 160 350 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1.8  1.8  25   29 4.0  0      true 4.4  2.4  51   260 true 8.2 4.5 130 350 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) .59 .58 8.1 29 .99 0      true 4.6  2.5  75   260 true 9.9 5.3 140 360 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) .36 .36 4.1 28 .99 0      false(valid-deref) 3.8  2.1  67   260 true 8.6 4.5 150 330 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) .35 .35 3.9 27 .84 0      false(valid-deref) 3.5  2.0  54   250 false(valid-deref) 7.6 4.1 130 320 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i unknown 900    900    2100   69 170    0      - - error (invalid witness file) .54 .34 10   43 error (invalid witness file) 6.4 3.4 130 310
array-memsafety/array01-alloca_true-valid-memsafety.i unknown 890    900    10000   280 20    0      - - error (invalid witness file) .54 .34 9.2 41 error (invalid witness file) 6.2 3.3 130 300
array-memsafety/array02-alloca_true-valid-memsafety.i unknown 890    900    9300   280 14    0      - - error (invalid witness file) .52 .34 9.2 40 error (invalid witness file) 5.7 3.1 100 300
array-memsafety/array03-alloca_true-valid-memsafety.i unknown 890    900    1700   280 17    0      - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 6.8 3.5 140 310
array-memsafety/bubblesort-alloca_true-valid-memsafety.i unknown 890    900    8600   310 20    0      - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.0 3.2 130 310
array-memsafety/count_down-alloca_true-valid-memsafety.i unknown 890    900    11000   300 23    0      - - error (invalid witness file) .57 .36 6.7 40 error (invalid witness file) 5.8 3.1 100 300
array-memsafety/cstrcat-alloca_true-valid-memsafety.i unknown 900    900    12000   84 250    0      - - error (invalid witness file) .51 .33 13   42 error (invalid witness file) 6.1 3.3 120 300
array-memsafety/cstrchr-alloca_true-valid-memsafety.i unknown 170    170    2400   46 260    0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.4 3.4 140 300
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i unknown 39    39    520   35 86    0      - - error (invalid witness file) .53 .33 9.8 40 error (invalid witness file) 6.2 3.3 120 310
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i unknown 140    140    1600   48 260    0      - - error (invalid witness file) .53 .34 11   40 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i unknown 900    900    12000   170 72    0      - - error (invalid witness file) .50 .33 13   39 error (invalid witness file) 5.7 3.1 120 290
array-memsafety/cstrlen-alloca_true-valid-memsafety.i unknown 100    100    1300   30 300    0      - - error (invalid witness file) .51 .32 13   39 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i unknown 900    900    10000   150 100    0      - - error (invalid witness file) .54 .34 13   43 error (invalid witness file) 6.3 3.3 110 290
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i unknown 62    62    870   79 86    0      - - error (invalid witness file) .59 .37 11   41 error (invalid witness file) 5.8 3.2 120 300
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i timeout 900    890    11000   960 240    0      - - error (invalid witness file) .58 .37 8.0 40 error (invalid witness file) 6.7 3.5 120 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i unknown 900    900    11000   140 56    0      - - error (invalid witness file) .54 .36 11   40 error (invalid witness file) 6.1 3.3 110 300
array-memsafety/cstrspn-alloca_true-valid-memsafety.i unknown 900    900    12000   150 65    0      - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.2 3.3 110 310
array-memsafety/diff-alloca_true-valid-memsafety.i unknown 890    900    7800   180 37    0      - - error (invalid witness file) .55 .36 11   39 error (invalid witness file) 6.0 3.2 110 300
array-memsafety/insertionsort-alloca_true-valid-memsafety.i unknown 890    900    9000   180 25    0      - - error (invalid witness file) .57 .37 7.8 40 error (invalid witness file) 6.7 3.5 130 310
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i unknown 890    900    8900   300 17    0      - - error (invalid witness file) .54 .34 12   43 error (invalid witness file) 5.8 3.1 120 300
array-memsafety/lis-alloca_true-valid-memsafety.i unknown 890    900    10000   190 20    0      - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 5.9 3.1 120 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i unknown 320    320    3600   89 300    0      - - error (invalid witness file) .53 .35 11   40 error (invalid witness file) 6.9 3.6 150 310
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i unknown 100    100    1300   33 280    0      - - error (invalid witness file) .55 .35 8.8 39 error (invalid witness file) 5.3 2.9 100 300
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i unknown 110    110    1300   43 260    0      - - error (invalid witness file) .55 .35 9.7 39 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i unknown 32    32    410   34 86    0      - - error (invalid witness file) .48 .31 12   39 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i unknown 93    93    1200   32 300    0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 7.2 3.7 140 320
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i unknown 130    130    2000   45 300    0      - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 5.6 3.0 120 290
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i timeout 900    890    13000   940 250    0      - - error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.0 3.2 130 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i unknown 900    900    13000   85 250    0      - - error (invalid witness file) .64 .40 8.2 40 error (invalid witness file) 6.2 3.3 130 300
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i unknown 270    270    3800   81 300    0      - - error (invalid witness file) .69 .43 8.2 41 error (invalid witness file) 6.4 3.4 120 320
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i unknown 130    130    1600   45 300    0      - - error (invalid witness file) .52 .33 11   43 error (invalid witness file) 5.6 3.0 110 300
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i unknown 900    900    12000   1100 180    0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 5.7 3.1 110 290
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i unknown 900    900    9500   95 200    0      - - error (invalid witness file) .50 .33 8.8 40 error (invalid witness file) 5.9 3.2 130 290
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i unknown 390    390    760   30 260    0      - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i unknown 900    900    11000   64 160    0      - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.0 3.2 110 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i unknown 220    220    2600   120 300    0      - - error (invalid witness file) .53 .34 11   41 error (invalid witness file) 6.4 3.4 140 310
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i timeout 900    890    10000   970 250    0      - - error (invalid witness file) .55 .36 11   40 error (invalid witness file) 5.7 3.1 110 290
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i unknown 110    110    1500   32 300    0      - - error (invalid witness file) .48 .32 11   40 error (invalid witness file) 6.2 3.3 130 300
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i unknown 900    900    10000   370 130    0      - - error (invalid witness file) .61 .39 9.4 42 error (invalid witness file) 5.6 3.0 110 290
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i unknown 890    900    9900   120 24    0      - - error (invalid witness file) .50 .32 13   40 error (invalid witness file) 6.4 3.4 130 300
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i unknown 900    900    14000   590 31    0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.2 3.3 130 300
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i true 1.1  1.1  13   29 3.4  0      - - error 4.9  2.7  52   260 true 25   18   320 520
array-memsafety/selectionsort-alloca_true-valid-memsafety.i unknown 890    900    6500   310 26    0      - - error (invalid witness file) .54 .34 11   41 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/stroeder1-alloca_true-valid-memsafety.i unknown 100    100    1400   53 260    0      - - error (invalid witness file) .60 .38 7.9 39 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/stroeder2-alloca_true-valid-memsafety.i unknown 890    900    8800   270 28    0      - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.9 3.2 120 300
array-memsafety/strreplace-alloca_true-valid-memsafety.i unknown 890    900    10000   59 100    0      - - error (invalid witness file) .47 .31 8.4 40 error (invalid witness file) 5.9 3.1 120 290
array-memsafety/subseq-alloca_true-valid-memsafety.i unknown 890    900    13000   59 98    0      - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.9 3.1 120 310
array-memsafety/substring-alloca_true-valid-memsafety.i unknown 900    900    12000   220 63    0      - - error (invalid witness file) .52 .32 8.7 41 error (invalid witness file) 6.4 3.3 140 300
array-examples/relax_false-valid-deref.i false(valid-deref) .63 .62 7.4 29 .99 0      error 5.1  2.8  54   250 true 11   5.8 180 370 - -
array-examples/sanfoundry_24_false-valid-deref.i unknown 440    440    830   100 260    0      error (invalid witness file) .51 .33 5.4 42 error (invalid witness file) 6.2 3.3 93 300 - -
array-examples/standard_strcpy_false-valid-deref_ground.i unknown 67    66    920   31 300    0      error (invalid witness file) .63 .40 7.3 41 error (invalid witness file) 6.1 3.2 120 300 - -
array-examples/standard_strcpy_original_false-valid-deref.i unknown 67    66    710   31 300    0      error (invalid witness file) .60 .39 8.3 40 error (invalid witness file) 6.9 3.6 94 310 - -
memsafety/960521-1_false-valid-deref.i unknown 440    440    1000   75 300    0      error (invalid witness file) .66 .42 8.4 41 error (invalid witness file) 5.7 3.0 93 290 - -
memsafety/test-0137_false-valid-deref.i false(valid-deref) .51 .50 6.9 29 .99 0      timeout 98    53    760   5300 true 8.3 4.5 130 320 - -
memsafety/test-0235_false-valid-deref.i unknown 600    600    6600   510 310    0      error (invalid witness file) .54 .34 11   42 error (invalid witness file) 5.6 3.0 69 300 - -
memsafety/960521-1_false-valid-free.i unknown 110    110    1500   77 260    0      error (invalid witness file) .58 .37 14   42 error (invalid witness file) 5.9 3.1 110 290 - -
memsafety/test-0158_false-valid-free.i false(valid-deref) 16    16    110   490 .99 0      true 4.3  2.4  73   270 true 10   5.4 140 350 - -
memsafety/test-0232_false-valid-free.i false(valid-deref) 1.4  1.4  16   29 3.5  0      true 5.4  3.0  54   260 true 7.5 4.0 130 310 - -
memsafety/20020406-1_false-valid-memtrack.i unknown 890    900    6600   4800 30    0      error (invalid witness file) .50 .32 13   40 error (invalid witness file) 6.0 3.2 110 300 - -
memsafety/20051113-1.c_false-valid-memtrack.i unknown 530    530    6600   170 300    0      error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.0 3.2 120 300 - -
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 7.3  7.3  88   40 19    0      false(valid-memtrack) 6.8  3.6  110   280 true 8.5 4.5 150 330 - -
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) 1.2  1.1  14   29 3.4  0      false(valid-memtrack) 5.6  3.0  91   270 true 8.2 4.4 150 320 - -
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 42    42    530   83 31    0      false(valid-memtrack) 7.4  3.9  120   290 true 8.1 4.3 160 320 - -
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) .54 .53 6.7 29 .84 0      false(valid-memtrack) 5.1  2.8  110   270 true 10   5.6 170 360 - -
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) 11    11    130   110 3.6  0      timeout 94    51    770   4600 true 7.9 4.2 120 310 - -
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) 1.7  1.7  3.4 29 .84 0      false(valid-memtrack) 33    24    640   2200 true 7.8 4.3 160 350 - -
memsafety/test-0220_false-valid-memtrack.i unknown 900    900    4500   8300 20    0      error (invalid witness file) .55 .36 11   39 error (invalid witness file) 6.3 3.4 130 310 - -
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) 2.2  2.2  4.4 29 .84 0      timeout 93    50    1000   3800 true 7.8 4.2 170 320 - -
memsafety/test-0234_false-valid-memtrack.i unknown 630    630    5300   520 270    0      error (invalid witness file) .56 .37 6.3 39 error (invalid witness file) 6.1 3.3 130 300 - -
memsafety/test-0235_false-valid-memtrack.i unknown 600    600    5400   510 310    0      error (invalid witness file) .48 .31 8.8 40 error (invalid witness file) 6.1 3.2 100 300 - -
memsafety/960521-1_true-valid-memsafety.i unknown 440    440    1600   72 300    0      - - error (invalid witness file) .54 .35 8.7 39 error (invalid witness file) 5.7 3.0 120 280
memsafety/lockfree-3.0_true-valid-memsafety.i unknown 890    900    9800   200 47    0      - - error (invalid witness file) .58 .38 8.9 40 error (invalid witness file) 5.9 3.2 120 300
memsafety/test-0019_true-valid-memsafety.i true .88 .87 8.9 29 4.0  0      - - true 4.7  2.6  47   250 true 16   9.2 200 540
memsafety/test-0102_true-valid-memsafety.i unknown 890    900    8500   550 4.2  0      - - error (invalid witness file) .50 .33 10   40 error (invalid witness file) 6.1 3.2 120 300
memsafety/test-0134_true-valid-memsafety.i unknown 890    900    12000   290 14    0      - - error (invalid witness file) .49 .30 11   40 error (invalid witness file) 6.0 3.2 120 300
memsafety/test-0158_true-valid-memsafety.i true 3.5  3.5  13   29 4.0  0      - - true 4.1  2.3  48   250 true 11   6.1 170 390
memsafety/test-0214_true-valid-memsafety.i unknown 890    900    7800   2000 5.0  0      - - error (invalid witness file) .48 .30 9.2 40 error (invalid witness file) 7.0 3.6 140 310
memsafety/test-0217_true-valid-memsafety.i unknown 890    900    6000   1900 1.7  0      - - error (invalid witness file) .64 .40 8.2 41 error (invalid witness file) 5.9 3.1 130 290
memsafety/test-0218_true-valid-memsafety.i unknown 890    900    5800   1900 2.0  0      - - error (invalid witness file) .51 .33 11   42 error (invalid witness file) 6.3 3.3 130 300
memsafety/test-0219_true-valid-memsafety.i unknown 900    900    5600   8500 20    0      - - error (invalid witness file) .51 .33 8.1 40 error (invalid witness file) 6.0 3.2 110 300
memsafety/test-0232_true-valid-memsafety.i unknown 890    900    9500   260 77    0      - - error (invalid witness file) .54 .35 11   39 error (invalid witness file) 6.2 3.3 130 300
memsafety/test-0234_true-valid-memsafety.i unknown 590    590    6500   510 310    0      - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.1 3.2 120 300
memsafety/test-0235_true-valid-memsafety.i unknown 590    590    6400   510 310    0      - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.4 3.4 130 300
memsafety/test-0236_true-valid-memsafety.i unknown 690    690    5700   510 300    0      - - error (invalid witness file) .64 .41 7.1 40 error (invalid witness file) 6.1 3.2 110 290
memsafety/test-0237_true-valid-memsafety.i unknown 660    650    5600   510 310    0      - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 6.0 3.2 140 300
memsafety/test-0504_true-valid-memsafety.i unknown 890    900    9800   380 11    0      - - error (invalid witness file) .51 .32 9.0 40 error (invalid witness file) 6.0 3.2 120 300
memsafety/test-0513_true-valid-memsafety.i unknown 890    900    11000   250 15    0      - - error (invalid witness file) .50 .33 12   42 error (invalid witness file) 6.3 3.3 110 310
memsafety/test-0521_true-valid-memsafety.i unknown 890    900    11000   750 9.3  0      - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.4 3.4 120 300
memsafety/test-memleak_nexttime_true-valid-memsafety.i unknown 890    900    6900   630 11    0      - - error (invalid witness file) .51 .34 13   40 error (invalid witness file) 6.2 3.3 120 310
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i unknown 890    900    12000   220 23    0      - - error (invalid witness file) .50 .32 9.3 39 error (invalid witness file) 6.9 3.6 110 300
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i unknown 890    900    9900   93 19    0      - - error (invalid witness file) .57 .37 7.4 40 error (invalid witness file) 5.8 3.1 110 300
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i unknown 890    900    12000   110 16    0      - - error (invalid witness file) .58 .35 7.6 40 error (invalid witness file) 7.0 3.7 140 320
memsafety-ext/tree_cnstr_true-valid-memsafety.i unknown 890    900    10000   160 13    0      - - error (invalid witness file) .58 .37 7.8 40 error (invalid witness file) 6.1 3.3 100 300
memsafety-ext/tree_dsw_true-valid-memsafety.i unknown 890    900    10000   340 10    0      - - error (invalid witness file) .47 .31 9.6 41 error (invalid witness file) 6.1 3.2 110 310
memsafety-ext/tree_of_cslls_true-valid-memsafety.i unknown 890    900    11000   520 8.0  0      - - error (invalid witness file) .51 .33 8.2 40 error (invalid witness file) 6.0 3.2 120 300
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i unknown 890    900    12000   270 11    0      - - error (invalid witness file) .64 .41 8.4 40 error (invalid witness file) 5.8 3.1 120 290
memsafety-ext/tree_stack_true-valid-memsafety.i unknown 890    900    12000   330 13    0      - - error (invalid witness file) .58 .36 8.5 39 error (invalid witness file) 6.4 3.4 130 310
memsafety-ext2/split_list_test05_false-valid-deref.i unknown 900    900    10000   15000 2.0  0      error (invalid witness file) .51 .33 3.8 40 error (invalid witness file) 6.9 3.6 130 300 - -
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i unknown 890    900    6800   550 22    0      error (invalid witness file) .53 .35 5.9 40 error (invalid witness file) 5.9 3.1 89 300 - -
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i unknown 890    900    7200   490 8.4  0      error (invalid witness file) .47 .31 3.7 40 error (invalid witness file) 5.9 3.2 110 310 - -
memsafety-ext2/length_test03_false-valid-memtrack.i false(valid-memtrack) 10    10    130   48 19    0      timeout 93    50    620   3800 true 8.3 4.5 160 320 - -
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i false(valid-deref) .82 .83 9.6 29 .99 0      timeout 97    59    940   4700 true 8.8 4.6 110 330 - -
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i unknown 890    900    7100   640 26    0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.3 3.3 120 300
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i unknown 890    900    6600   500 6.7  0      - - error (invalid witness file) .49 .32 13   40 error (invalid witness file) 7.4 3.9 130 320
memsafety-ext2/length_test03_true-valid-memsafety.i unknown 890    900    9200   190 62    0      - - error (invalid witness file) .61 .39 10   40 error (invalid witness file) 5.3 2.9 100 290
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i false(valid-deref) .79 .79 11   29 .99 0      - - out of memory 430    300    5900   7000 true 7.9 4.3 130 320
memsafety-ext2/split_list_test05_true-valid-memsafety.i unknown 900    900    10000   15000 2.0  0      - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.2 3.3 120 300
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 1.5  1.5  19   29 3.5  0      false(valid-deref) 5.7  3.0  78   270 true 8.7 4.7 160 350 - -
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(valid-deref) 1.3  1.3  19   30 4.0  0      false(valid-deref) 5.5  2.9  89   260 true 8.5 4.6 110 330 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) 1.3  1.3  15   29 4.0  0      false(valid-deref) 5.0  2.7  74   260 true 8.5 4.6 130 350 - -
list-ext-properties/960521-1_1_false-valid-free.i unknown 1.5  1.5  21   29 4.1  0      false(valid-free) 5.7  3.1  96   260 true 8.4 4.6 160 350 - -
list-ext-properties/test-0158_1_false-valid-free.i false(valid-deref) .57 .56 6.6 29 .84 0      false(valid-free) 33    20    290   1900 true 9.5 5.0 200 360 - -
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) .52 .52 5.9 29 .99 0      false(valid-memtrack) 5.0  2.7  73   270 true 20   12   240 580 - -
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) .47 .46 5.8 29 .84 0      false(valid-memtrack) 28    17    290   1700 true 8.1 4.4 130 350 - -
list-ext-properties/test-0232_1_false-valid-memtrack.i false(valid-memtrack) .57 .57 6.7 29 .99 0      false(valid-memtrack) 8.8  4.6  140   300 true 8.0 4.3 130 330 - -
list-ext-properties/960521-1_1_true-valid-memsafety.i unknown 890    900    10000   110 55    0      - - error (invalid witness file) .53 .35 7.4 40 error (invalid witness file) 6.6 3.4 120 310
list-ext-properties/list-ext_1_true-valid-memsafety.i unknown 890    900    10000   220 29    0      - - error (invalid witness file) .49 .31 9.8 39 error (invalid witness file) 6.9 3.6 120 310
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i unknown 890    900    9600   200 41    0      - - error (invalid witness file) .61 .39 11   44 error (invalid witness file) 6.0 3.2 130 300
list-ext-properties/simple-ext_1_true-valid-memsafety.i unknown 890    900    10000   190 59    0      - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.4 3.4 130 290
list-ext-properties/test-0019_1_true-valid-memsafety.i true .84 .83 10   29 3.4  0      - - true 3.8  2.1  59   260 true 39   26   480 820
list-ext-properties/test-0158_1_true-valid-memsafety.i true 1.1  1.1  12   29 4.0  0      - - true 3.6  2.0  44   250 true 11   6.1 170 380
list-ext-properties/test-0214_1_true-valid-memsafety.i unknown 890    900    2700   870 2.5  0      - - error (invalid witness file) .58 .37 6.6 40 error (invalid witness file) 5.5 2.9 120 290
list-ext-properties/test-0217_1_true-valid-memsafety.i unknown 890    900    5300   1100 3.4  0      - - error (invalid witness file) .56 .35 10   42 error (invalid witness file) 6.3 3.3 110 310
list-ext-properties/test-0232_1_true-valid-memsafety.i true 190    190    2100   150 55    0      - - true 9.3  4.9  80   290 timeout 960   910   9700 1100
list-ext-properties/test-0504_1_true-valid-memsafety.i unknown 890    900    8100   440 11    0      - - error (invalid witness file) .61 .38 7.9 39 error (invalid witness file) 6.0 3.2 120 300
list-ext-properties/test-0513_1_true-valid-memsafety.i unknown 890    900    8900   2600 16    0      - - true 7.3  3.9  120   280 timeout 960   870   17000 1700
memory-alloca/c.03-alloca_true-valid-memsafety.i unknown 160    150    1800   71 260    0      - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.5 3.4 130 300
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) .39 .39 4.7 28 1.0  0      true 3.7  2.0  61   270 true 8.6 4.6 110 330 - -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c unknown .36 .35 4.2 28 1.0  0      true 3.5  1.9  54   260 true 9.2 4.9 130 350 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c unknown .36 .36 4.0 27 .84 0      true 3.6  2.0  74   250 true 8.8 4.8 120 350 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c unknown .37 .36 4.3 27 .84 0      true 3.3  1.9  41   260 true 8.8 4.7 120 340 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 610    610    5600   570 100    0      true 11    5.7  140   420 true 27   14   280 900 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c unknown 900    900    1900   430 76    0      error (invalid witness file) .55 .35 6.6 39 error (invalid witness file) 6.0 3.2 98 310 - -
ldv-memsafety/memset2_false-valid-deref-write.c unknown 75    75    930   29 180    0      error (invalid witness file) .49 .32 10   39 error (invalid witness file) 5.8 3.1 92 300 - -
ldv-memsafety/memset3_false-valid-deref-write.c unknown 270    270    3100   39 260    0      error (invalid witness file) .48 .31 9.3 40 error (invalid witness file) 5.9 3.1 80 300 - -
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c unknown 75    75    960   28 180    0      error (invalid witness file) .48 .31 7.5 40 error (invalid witness file) 5.8 3.1 110 300 - -
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c unknown 270    270    3600   38 260    0      error (invalid witness file) .52 .34 9.7 41 error (invalid witness file) 7.0 3.7 110 310 - -
ldv-memsafety/memsetNonZero_false-valid-deref-write.c unknown 270    270    3400   39 260    0      error (invalid witness file) .47 .32 6.4 40 error (invalid witness file) 5.6 3.0 90 300 - -
ldv-memsafety/memset_false-valid-deref-write.c unknown 270    270    3500   39 220    0      error (invalid witness file) .51 .33 11   39 error (invalid witness file) 5.6 3.0 110 290 - -
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c unknown 900    900    9500   1800 150    0      - - error (invalid witness file) .50 .32 13   40 error (invalid witness file) 5.9 3.1 120 310
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety.c unknown 900    900    6400   690 95    0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.0 3.1 100 300
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 670    660    5500   590 86    0      - - true 8.4  4.4  140   350 true 15   8.5 240 500
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety.c unknown 900    900    8600   800 91    0      - - error (invalid witness file) .56 .36 11   40 error (invalid witness file) 6.2 3.2 130 290
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c unknown 900    900    7000   640 86    0      - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 5.8 3.1 120 300
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety.c true 660    650    5600   620 89    0      - - true 7.6  4.1  100   340 true 12   6.6 170 410
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true 3.7  2.2  36   230 4.0  0      - - true 3.0  1.6  36   240 error 6.4 3.4 110 310
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true 3.7  2.2  36   250 3.4  0      - - true 3.2  1.8  40   240 error 6.9 3.7 130 310
ldv-memsafety/StructInitialization_true-valid-memsafety.c true 3.2  1.8  29   230 3.5  0      - - true 2.9  1.6  53   240 true 6.5 3.5 110 300
ldv-memsafety/memset2_true-valid-memsafety.c true 40    39    530   240 120    0      - - true 3.0  1.7  50   240 true 9.1 5.0 140 350
ldv-memsafety/memset3_true-valid-memsafety.c true 230    220    3400   250 240    0      - - true 3.4  2.0  41   240 true 9.3 5.1 150 360
ldv-memsafety/memsetNonZero2_true-valid-memsafety.c true 40    39    550   250 100    0      - - true 3.0  1.7  68   240 true 9.2 5.0 160 340
ldv-memsafety/memsetNonZero3_true-valid-memsafety.c true 230    220    3200   250 220    0      - - true 3.0  1.7  52   240 true 9.2 5.0 150 340
ldv-memsafety/memsetNonZero_true-valid-memsafety.c true 230    220    3000   250 200    .0041 - - true 3.3  1.8  50   240 true 8.9 4.8 170 350
ldv-memsafety/memset_true-valid-memsafety.c true 230    220    3100   240 200    0      - - true 3.0  1.7  46   250 true 9.1 5.0 180 350
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) .81 .81 10   35 .84 0      true 5.9  3.2  66   310 true 8.4 4.4 130 320 - -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 34    34    470   36 52    0      true 6.5  3.5  97   310 true 8.2 4.4 170 310 - -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 140    140    320   36 61    0      true 5.6  3.1  73   280 true 8.4 4.5 130 330 - -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-deref) 560    560    5500   350 21    0      exception 3.3  1.8  49   240 true 11   5.6 140 340 - -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(valid-deref) 600    600    6200   330 21    0      exception 3.9  2.1  68   260 true 9.1 4.9 160 320 - -
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-deref) 1.7  1.7  23   36 .99 0      false(valid-free) 7.4  3.9  75   280 true 56   49   690 490 - -
ldv-memsafety/memleaks_test12_false-valid-free.i unknown 260    260    3300   210 97    0      error (invalid witness file) .50 .32 4.0 40 error (invalid witness file) 6.7 3.5 150 320 - -
ldv-memsafety/memleaks_test17_2_false-valid-free.i unknown 890    900    8900   310 27    0      error (invalid witness file) .52 .32 11   40 error (invalid witness file) 6.2 3.3 92 330 - -
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-deref) .74 .73 9.1 30 .99 0      true 6.0  3.2  99   280 true 7.9 4.2 150 310 - -
ldv-memsafety/memleaks_test2_false-valid-free.i false(valid-deref) .52 .51 8.0 30 .99 0      false(valid-free) 6.0  3.2  94   270 false(valid-free) 8.8 4.8 150 350 - -
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-deref) .38 .38 4.6 30 .84 0      false(valid-free) 29    19    510   1600 true 7.2 3.8 120 320 - -
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-deref) .57 .56 7.4 30 .99 0      false(valid-free) 6.1  3.3  98   280 true 13   7.1 200 450 - -
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-deref) .55 .55 7.5 30 .99 0      true 6.1  3.2  97   310 true 9.3 5.0 160 360 - -
ldv-memsafety/memleaks_test10_false-valid-memtrack.i false(valid-deref) .75 .75 9.8 31 .99 0      false(valid-memtrack) 7.1  3.7  140   330 timeout 97   89   2100 530 - -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack.i false(valid-deref) 1.2  1.1  14   32 .84 0      false(valid-memtrack) 6.5  3.5  97   300 true 12   6.5 200 400 - -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack.i false(valid-memtrack) .50 .50 6.1 30 .84 0      true 5.7  3.1  92   300 true 7.9 4.2 160 320 - -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(valid-memtrack) 4.3  4.3  53   44 3.4  0      true 6.3  3.4  97   310 true 8.5 4.5 150 320 - -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack.i false(valid-memtrack) .49 .49 5.9 30 .84 0      true 8.3  4.4  59   290 true 10   5.4 150 350 - -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(valid-memtrack) 3.8  3.8  46   44 3.4  0      true 6.3  3.3  94   300 true 19   11   410 570 - -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-memtrack) 77    76    1000   74 93    0      true 7.7  4.0  100   290 true 8.7 4.7 130 340 - -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack.i false(valid-memtrack) .47 .47 6.4 30 .99 0      false(valid-memtrack) 6.3  3.3  100   300 unknown 22   12   230 460 - -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack.i false(valid-memtrack) .47 .47 5.5 30 .99 0      false(valid-memtrack) 6.0  3.2  94   280 unknown 15   7.9 180 350 - -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i unknown 890    900    7400   260 29    0      error (invalid witness file) .54 .35 5.5 42 error (invalid witness file) 6.0 3.2 85 300 - -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 380    380    5200   180 31    0      false(valid-memtrack) 9.8  5.2  110   330 true 11   5.9 150 360 - -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack.i false(valid-memtrack) .50 .50 5.7 30 .84 0      false(valid-memtrack) 7.1  3.8  62   300 true 12   6.4 180 370 - -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack.i false(valid-memtrack) 640    640    6000   160 27    0      false(valid-memtrack) 7.6  4.0  110   310 true 9.7 5.2 180 360 - -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack.i false(valid-memtrack) 10    10    130   37 27    0      false(valid-memtrack) 7.1  3.8  95   280 true 11   5.8 130 380 - -
ldv-memsafety/memleaks_test1_false-valid-memtrack.i false(valid-memtrack) .49 .49 5.2 30 .84 0      false(valid-memtrack) 6.3  3.3  93   300 unknown 14   7.3 150 350 - -
ldv-memsafety/memleaks_test20_false-valid-memtrack.i false(valid-memtrack) .49 .49 5.6 30 .84 0      false(valid-memtrack) 6.4  3.4  110   280 unknown 15   8.2 150 360 - -
ldv-memsafety/memleaks_test21_false-valid-memtrack.i false(valid-memtrack) .48 .48 6.2 30 .84 0      false(valid-memtrack) 6.3  3.3  88   320 unknown 14   7.7 240 340 - -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack.i false(valid-memtrack) 29    29    390   34 61    0      true 6.1  3.3  130   310 true 8.7 4.6 140 330 - -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack.i false(valid-memtrack) 15    15    190   30 56    0      true 6.0  3.2  110   290 true 14   8.1 200 450 - -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack.i false(valid-memtrack) 29    29    390   34 61    0      true 6.6  3.5  100   280 true 7.9 4.2 110 320 - -
ldv-memsafety/memleaks_test4_false-valid-memtrack.i false(valid-memtrack) .53 .52 5.8 30 .84 0      false(valid-memtrack) 6.4  3.4  120   290 unknown 17   9.2 310 350 - -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack.i false(valid-memtrack) .49 .49 5.3 30 .99 0      false(valid-memtrack) 6.7  3.6  64   270 unknown 14   7.4 180 350 - -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack.i false(valid-memtrack) .47 .47 5.7 30 .99 0      true 5.9  3.2  130   300 unknown 16   8.8 230 350 - -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack.i false(valid-memtrack) .50 .50 5.2 30 .99 0      true 6.7  3.6  100   300 true 12   7.0 140 470 - -
ldv-memsafety/memleaks_test6_3_false-valid-memtrack.i false(valid-memtrack) .51 .51 5.2 30 .99 0      false(valid-memtrack) 6.4  3.4  88   320 true 10   5.3 130 340 - -
ldv-memsafety/memleaks_test7_false-valid-memtrack.i false(valid-memtrack) .50 .50 6.1 30 .84 0      false(valid-memtrack) 6.5  3.5  98   320 true 8.0 4.2 160 330 - -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack.i false(valid-memtrack) .46 .46 5.4 30 .99 0      false(valid-memtrack) 6.0  3.2  94   270 unknown 14   7.5 150 350 - -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack.i false(valid-memtrack) .50 .49 6.4 30 .99 .0041 false(valid-memtrack) 6.5  3.5  130   320 unknown 15   7.8 210 350 - -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack.i false(valid-memtrack) .46 .46 6.0 30 .84 0      false(valid-memtrack) 6.0  3.2  100   280 unknown 14   7.7 210 350 - -
ldv-memsafety/memleaks_test10_true-valid-memsafety.i false(valid-deref) .86 .86 10   31 .84 0      - - true 7.1  3.8  120   310 true 230   220   3300 660
ldv-memsafety/memleaks_test11_true-valid-memsafety.i false(valid-deref) 1.7  1.7  22   35 .99 0      - - true 11    5.5  110   440 true 56   49   660 530
ldv-memsafety/memleaks_test12_true-valid-memsafety.i unknown 280    280    3500   210 92    0      - - error (invalid witness file) .58 .37 12   43 error (invalid witness file) 5.8 3.1 97 300
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 31    31    270   360 3.4  0      - - true 6.4  3.4  66   310 true 760   730   9000 970
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 20    20    170   290 3.4  0      - - true 5.8  3.1  63   270 true 170   150   3000 1100
ldv-memsafety/memleaks_test15_true-valid-memsafety.i false(valid-deref) .99 .98 13   35 .99 0      - - true 11    5.8  170   420 true 9.1 4.8 170 320
ldv-memsafety/memleaks_test16_true-valid-memsafety.i true .99 .99 14   30 4.0  0      - - true 4.7  2.6  59   260 true 12   6.6 200 430
ldv-memsafety/memleaks_test17_1_true-valid-memsafety.i unknown 890    900    9200   290 27    0      - - error (invalid witness file) .52 .35 8.9 41 error (invalid witness file) 6.5 3.4 130 300
ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i unknown 890    900    9000   270 19    0      - - error (invalid witness file) .50 .32 7.5 40 error (invalid witness file) 6.1 3.2 110 290
ldv-memsafety/memleaks_test18_true-valid-memsafety.i true 840    840    7000   240 31    0      - - true 7.2  3.9  71   290 timeout 960   930   14000 780
ldv-memsafety/memleaks_test19_true-valid-memsafety.i true 1.1  1.1  12   30 4.0  0      - - true 4.8  2.6  66   260 true 230   200   2600 860
ldv-memsafety/memleaks_test1_true-valid-memsafety.i true .99 .98 12   30 3.4  0      - - true 4.6  2.5  53   260 true 10   5.6 160 360
ldv-memsafety/memleaks_test20_true-valid-memsafety.i true 1.0  1.0  14   30 4.0  0      - - true 5.9  3.2  74   260 true 16   8.9 170 460
ldv-memsafety/memleaks_test21_true-valid-memsafety.i true 1.0  1.0  13   30 4.0  0      - - true 5.8  3.2  61   260 true 12   6.7 200 400
ldv-memsafety/memleaks_test22_1_true-valid-memsafety.i true 28    28    360   33 52    0      - - true 5.2  2.8  96   260 true 320   280   5400 1100
ldv-memsafety/memleaks_test22_2_true-valid-memsafety.i true 37    37    500   36 61    0      - - true 6.2  3.3  43   260 timeout 960   920   14000 3000
ldv-memsafety/memleaks_test22_3_true-valid-memsafety.i true 37    37    410   36 61    0      - - true 6.4  3.4  78   260 timeout 960   920   17000 2600
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i false(valid-deref) 480    480    4800   340 22    0      - - exception 4.2  2.3  40   240 true 12   6.2 160 370
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i false(valid-deref) 200    200    1900   210 25    0      - - exception 3.6  2.0  66   250 true 17   9.6 230 500
ldv-memsafety/memleaks_test2_true-valid-memsafety.i true .98 .98 11   30 3.4  0      - - true 4.8  2.6  86   280 true 10   5.5 170 370
ldv-memsafety/memleaks_test3_true-valid-memsafety.i true .98 .97 13   30 3.5  0      - - true 5.9  3.2  39   290 true 11   6.0 220 360
ldv-memsafety/memleaks_test4_true-valid-memsafety.i true 1.0  1.0  12   30 4.0  0      - - true 4.6  2.5  51   260 true 13   7.3 180 510
ldv-memsafety/memleaks_test5_true-valid-memsafety.i true .99 .98 13   30 4.0  0      - - true 4.8  2.6  66   250 true 11   6.3 160 380
ldv-memsafety/memleaks_test6_true-valid-memsafety.i true 1.1  1.0  13   30 4.0  0      - - true 5.3  2.9  93   260 true 180   170   2100 660
ldv-memsafety/memleaks_test7_true-valid-memsafety.i true 1.1  1.1  13   30 3.4  0      - - true 5.6  3.0  45   260 true 88   79   1000 610
ldv-memsafety/memleaks_test8_true-valid-memsafety.i true 1.0  1.0  12   30 4.0  0      - - true 5.5  2.9  57   260 true 11   6.1 150 370
ldv-memsafety/memleaks_test9_true-valid-memsafety.i true 1.0  .99 12   30 4.0  0      - - true 6.3  3.3  77   290 true 11   6.3 180 380
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i unknown 17    17    200   28 99    0      - - error (invalid witness file) .54 .35 12   42 error (invalid witness file) 5.9 3.1 120 290
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety.i unknown 18    18    210   28 99    0      - - error (invalid witness file) .54 .35 8.3 40 error (invalid witness file) 6.3 3.4 130 320
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety.i unknown 18    18    240   28 99    0      - - error (invalid witness file) .53 .34 13   41 error (invalid witness file) 6.1 3.2 130 300
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety.i unknown 8.9  8.9  110   28 31    0      - - true 3.7  2.0  57   250 unknown 6.4 3.4 120 300
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety.i false(valid-deref) 9.6  9.6  130   28 31    0      - - true 3.6  2.0  59   260 unknown 6.6 3.5 130 300
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i unknown 17    17    200   28 99    0      error (invalid witness file) .59 .37 5.0 41 error (invalid witness file) 5.7 3.0 75 300 - -
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i unknown 18    18    270   29 99    0      error (invalid witness file) .55 .35 13   40 error (invalid witness file) 6.4 3.4 120 310 - -
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i unknown 160    160    450   29 110    0      error (invalid witness file) .54 .35 5.2 43 error (invalid witness file) 6.1 3.2 90 290 - -
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i false(valid-deref) 9.5  9.5  110   28 37    0      true 3.4  2.0  50   250 unknown 6.0 3.2 110 300 - -
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i unknown 19    19    230   28 84    0      error (invalid witness file) .49 .32 8.1 41 error (invalid witness file) 5.8 3.0 110 300 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 890    900    12000   1100 8.0  0      - - error (invalid witness file) .60 .38 8.0 41 error (invalid witness file) 6.0 3.2 110 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 890    900    7800   360 8.0  0      - - error (invalid witness file) .60 .38 10   41 error (invalid witness file) 6.2 3.3 120 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 890    900    12000   850 11    0      - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.3 3.3 120 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 890    900    11000   310 16    0      - - error (invalid witness file) .53 .34 10   41 error (invalid witness file) 5.9 3.2 110 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1.4  1.4  16   30 3.4  0      false(valid-deref) 5.2  2.8  73   270 true 8.8 4.7 170 320 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) .39 .39 4.4 29 .84 0      timeout 96    70    940   4300 true 10   5.3 160 350 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 4.7  4.7  13   29 4.0  0      timeout 94    79    1100   3800 true 9.8 5.2 160 350 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1.7  1.7  20   38 3.4  0      timeout 95    72    880   3700 error 11   5.7 180 310 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 5.6  5.6  20   33 4.0  0      false(valid-memtrack) 6.4  3.4  62   270 true 8.6 4.6 140 320 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1.3  1.3  16   29 3.4  0      false(valid-memtrack) 5.3  2.9  94   270 true 7.8 4.2 100 320 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i unknown 890    900    9200   190 92    0      - - error (invalid witness file) .49 .31 13   39 error (invalid witness file) 6.0 3.2 120 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .47 .46 5.2 29 .84 0      timeout 94    78    1700   4000 true 8.8 4.7 120 350 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 44    44    350   480 13    0      error 4.7  2.5  75   270 true 8.8 4.6 110 330 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .46 .46 4.9 29 .99 0      timeout 94    75    1600   3700 true 8.4 4.5 140 340 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1.0  1.0  13   29 3.4  0      timeout 94    79    910   3900 true 8.3 4.4 150 330 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1.0  1.0  12   29 4.0  0      timeout 94    78    1500   3900 true 7.2 3.9 85 310 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .47 .47 5.1 29 .84 0      false(valid-memtrack) 5.6  3.0  85   270 true 8.7 4.7 150 350 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 890    900    10000   1100 25    0      - - error (invalid witness file) .48 .31 9.9 39 error (invalid witness file) 6.3 3.4 110 300
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 890    900    9900   990 25    0      - - error (invalid witness file) .50 .33 13   41 error (invalid witness file) 6.4 3.4 120 300
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 890    900    11000   940 29    0      - - error (invalid witness file) .47 .31 8.4 39 error (invalid witness file) 6.6 3.5 130 300
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 890    900    9500   990 29    0      error (invalid witness file) .61 .39 8.7 39 error (invalid witness file) 6.4 3.4 110 310 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 890    900    11000   970 25    0      error (invalid witness file) .49 .31 9.2 39 error (invalid witness file) 5.9 3.2 110 290 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 890    900    10000   970 29    0      error (invalid witness file) .58 .38 8.4 41 error (invalid witness file) 6.9 3.6 130 320 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 890    900    10000   1000 27    0      error (invalid witness file) .51 .32 6.7 41 error (invalid witness file) 6.2 3.3 110 290 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 890    900    9400   1000 29    0      error (invalid witness file) .48 .31 9.4 39 error (invalid witness file) 6.8 3.6 140 310 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 890    900    9800   1200 25    0      error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.2 3.3 100 300 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 890    900    9500   1100 25    0      error (invalid witness file) .47 .30 6.7 40 error (invalid witness file) 7.0 3.6 130 310 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 890    900    9900   1100 25    0      error (invalid witness file) .49 .31 4.7 41 error (invalid witness file) 6.0 3.3 120 300 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 900    900    10000   1000 25    0      error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.5 3.4 88 300 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 900    900    3100   1100 29    0      error (invalid witness file) .72 .44 6.6 40 error (invalid witness file) 6.3 3.4 110 300 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 890    900    9600   220 20    0      - - error (invalid witness file) .52 .34 11   41 error (invalid witness file) 6.4 3.4 130 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i unknown 890    900    2800   230 40    0      - - error (invalid witness file) .50 .31 8.9 40 error (invalid witness file) 6.0 3.2 110 290
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 890    900    8900   260 17    0      - - error (invalid witness file) .50 .32 13   39 error (invalid witness file) 6.0 3.2 120 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i unknown 890    900    9100   200 97    0      - - error (invalid witness file) .49 .31 10   40 error (invalid witness file) 6.6 3.5 130 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 890    900    9300   330 20    0      - - error (invalid witness file) .48 .31 9.5 39 error (invalid witness file) 6.0 3.2 98 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 890    900    9000   270 17    0      - - error (invalid witness file) .52 .34 12   41 error (invalid witness file) 6.1 3.2 110 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i unknown 890    900    11000   170 34    0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.4 3.4 130 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i unknown 890    900    10000   150 42    0      - - error (invalid witness file) .56 .36 7.6 40 error (invalid witness file) 5.9 3.2 120 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i unknown 890    900    12000   190 65    0      - - error (invalid witness file) .58 .38 8.3 40 error (invalid witness file) 6.3 3.3 120 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i unknown 890    900    8100   240 17    0      - - error (invalid witness file) .53 .35 8.2 40 error (invalid witness file) 6.3 3.3 120 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i unknown 890    900    8700   340 17    0      - - error (invalid witness file) .50 .33 13   39 error (invalid witness file) 6.3 3.3 130 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i unknown 890    900    10000   540 62    0      - - error (invalid witness file) .56 .35 8.7 39 error (invalid witness file) 6.4 3.4 130 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 890    900    7500   230 20    0      - - error (invalid witness file) .53 .35 11   40 error (invalid witness file) 6.2 3.3 120 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i unknown 890    900    9200   190 100    0      - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 7.5 4.0 140 310
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 890    900    9800   410 20    0      - - error (invalid witness file) .49 .30 6.6 39 error (invalid witness file) 7.0 3.7 130 320
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 890    900    10000   360 17    0      - - error (invalid witness file) .51 .32 10   39 error (invalid witness file) 6.1 3.2 130 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i unknown 890    900    9800   170 39    0      - - error (invalid witness file) .55 .36 12   42 error (invalid witness file) 5.8 3.1 130 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i unknown 900    900    13000   190 52    0      - - error (invalid witness file) .63 .42 7.2 40 error (invalid witness file) 6.0 3.2 100 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i unknown 890    900    9000   200 80    0      - - error (invalid witness file) .50 .32 9.9 40 error (invalid witness file) 6.8 3.5 130 310
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1.5  1.5  19   36 3.5  0      false(valid-deref) 5.5  2.9  67   270 true 9.2 5.0 160 350 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 2.3  2.3  5.5 29 .84 0      timeout 96    76    1800   4000 true 8.6 4.6 110 320 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1.4  1.4  16   30 4.1  0      false(valid-deref) 5.6  3.0  83   270 true 8.2 4.5 120 350 - -
loop-acceleration/array3_false-valid-deref.i unknown 53    53    690   28 260    0      error (invalid witness file) .53 .34 11   40 error (invalid witness file) 5.9 3.2 110 300 - -
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 130    130    1000   790 .86 0      true 12    6.3  170   390 unknown 8.2 4.3 150 310 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 750    760    6400   1100 1.0  0      true 7.2  3.8  110   280 unknown 6.8 3.6 110 300 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 79    54    780   4000 5.0  0      - - true 39    23    340   2300 true 12   6.6 180 460
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 74    52    810   4000 4.4  0      - - true 38    21    450   2400 true 13   6.9 210 460
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 900    840    12000   4800 3.5  0      - - out of memory 250    140    1900   7000 true 10   5.4 150 340
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 270    160    380   4000 3.6  0      - - true 47    29    470   2800 true 9.7 5.2 170 320
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 67    41    670   3900 4.2  0      - - true 44    26    520   2700 true 9.7 5.2 150 330
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 130    86    1200   4300 4.3  0      - - true 74    45    820   3700 true 10   5.4 190 370
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 130    86    1400   4300 4.3  0      - - true 72    44    620   3500 true 10   5.5 170 370
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 39    15    43   460 3.5  0      - - true 9.3  4.9  110   350 true 9.4 4.9 130 340
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 23    9.9  230   1900 4.2  0      - - true 20    10    320   1000 true 9.0 4.9 170 320
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 23    10    220   1800 4.2  0      - - true 26    13    210   1000 true 9.1 4.8 140 320
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900    720    12000   7100 4.0  0      - - timeout 910    810    14000   7000 true 7.5 4.0 120 320
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 910    740    11000   7100 4.0  0      - - timeout 910    780    8900   7000 true 7.4 4.0 140 310
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 910    770    1600   4600 3.4  0      - - out of memory 740    610    12000   7000 true 8.2 4.3 140 330
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900    740    12000   7000 4.0  0      - - out of memory 740    600    9600   7000 true 7.7 4.1 140 320
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 900    860    15000   3700 4.0  0      - - out of memory 660    570    7300   7000 true 7.8 4.2 130 320
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900    750    13000   6900 4.0  0      - - timeout 940    810    12000   7000 true 8.1 4.3 160 320
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 900    860    13000   3200 3.4  0      - - timeout 910    840    12000   6100 true 8.3 4.4 160 320
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900    750    10000   6600 3.4  0      - - timeout 910    840    11000   6100 true 8.1 4.4 140 320
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900    680    10000   8100 3.4  0      - - out of memory 860    760    15000   7000 true 7.2 3.9 150 310
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 910    610    9400   8800 3.4  0      - - timeout 910    800    12000   6800 true 7.5 4.0 150 320
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900    610    9400   8400 4.0  0      - - timeout 910    830    14000   6400 true 7.2 3.9 120 320
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900    690    12000   8300 4.0  0      - - timeout 910    830    13000   6300 true 7.2 3.9 150 310
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900    680    10000   7500 4.0  0      - - timeout 910    810    10000   6800 true 7.2 3.9 160 310
../../sv-benchmarks/c/ verifier status 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 328 130000 130000 1400000 250000 19000 .0082 328 2000 1400 26000 94000   328 1400 800 22000 48000   328 13000 11000 170000 140000   328 8200 7100 120000 73000  
    correct results 129 8600 8200 83000 40000 2500 .0082 62 1800 1200 23000 80000   69 860 460 13000 30000   44 550 310 6100 29000   39 6000 5500 84000 27000  
        correct true 45 4400 4000 42000 34000 1600 .0041 25 0 0 0 0   64 0 0 0 0   44 550 310 6100 29000   39 6000 5500 84000 27000  
        correct false 84 4200 4200 41000 6500 840 .0041 37 1800 1200 23000 80000   5 860 460 13000 30000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 19 720 720 7100 1500 96 0      11 210 130 2600 11000   11 250 190 4300 4600   4 470 330 6500 8900   6 340 300 4800 3000  
        incorrect true 0
        incorrect false 19 720 720 7100 1500 96 0      7 210 130 2600 11000   1 250 190 4300 4600   0 470 330 6500 8900   0 340 300 4800 3000  
score (328 tasks, max score: 517) -130
Run set [sv-comp17.MemSafety-Arrays; sv-comp17.MemSafety-Heap; sv-comp17.MemSafety-LinkedLists; sv-comp17.MemSafety-Other]