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