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