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