Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-13 04:51:53 CET [[ 2017-01-15 00:05:22 CET ]] [[ 2017-01-15 00:31:32 CET ]] [[ 2017-01-15 00:11:25 CET ]] [[ 2017-01-15 00:39:18 CET ]]
Run set sv-comp17.MemSafety-Heap
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
memsafety/960521-1_false-valid-deref.i unknown 0 wit inspect 440    440    1000   75 300    0      error (invalid witness file) .66 .42 8.4 41 error (invalid witness file) 5.7 3.0 93 290 - -
memsafety/test-0137_false-valid-deref.i false(valid-deref) 1 wit inspect .51 .50 6.9 29 .99 0      timeout 98    53    760   5300 true 8.3 4.5 130 320 - -
memsafety/test-0235_false-valid-deref.i unknown 0 wit inspect 600    600    6600   510 310    0      error (invalid witness file) .54 .34 11   42 error (invalid witness file) 5.6 3.0 69 300 - -
memsafety/960521-1_false-valid-free.i unknown 0 wit inspect 110    110    1500   77 260    0      error (invalid witness file) .58 .37 14   42 error (invalid witness file) 5.9 3.1 110 290 - -
memsafety/test-0158_false-valid-free.i false(valid-deref) -16 wit inspect 16    16    110   490 .99 0      true 4.3  2.4  73   270 true 10   5.4 140 350 - -
memsafety/test-0232_false-valid-free.i false(valid-deref) -16 wit inspect 1.4  1.4  16   29 3.5  0      true 5.4  3.0  54   260 true 7.5 4.0 130 310 - -
memsafety/20020406-1_false-valid-memtrack.i unknown 0 wit inspect 890    900    6600   4800 30    0      error (invalid witness file) .50 .32 13   40 error (invalid witness file) 6.0 3.2 110 300 - -
memsafety/20051113-1.c_false-valid-memtrack.i unknown 0 wit inspect 530    530    6600   170 300    0      error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.0 3.2 120 300 - -
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.3  7.3  88   40 19    0      false(valid-memtrack) 6.8  3.6  110   280 true 8.5 4.5 150 330 - -
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.2  1.1  14   29 3.4  0      false(valid-memtrack) 5.6  3.0  91   270 true 8.2 4.4 150 320 - -
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 42    42    530   83 31    0      false(valid-memtrack) 7.4  3.9  120   290 true 8.1 4.3 160 320 - -
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .54 .53 6.7 29 .84 0      false(valid-memtrack) 5.1  2.8  110   270 true 10   5.6 170 360 - -
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 11    11    130   110 3.6  0      timeout 94    51    770   4600 true 7.9 4.2 120 310 - -
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.7  1.7  3.4 29 .84 0      false(valid-memtrack) 33    24    640   2200 true 7.8 4.3 160 350 - -
memsafety/test-0220_false-valid-memtrack.i unknown 0 wit inspect 900    900    4500   8300 20    0      error (invalid witness file) .55 .36 11   39 error (invalid witness file) 6.3 3.4 130 310 - -
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.2  2.2  4.4 29 .84 0      timeout 93    50    1000   3800 true 7.8 4.2 170 320 - -
memsafety/test-0234_false-valid-memtrack.i unknown 0 wit inspect 630    630    5300   520 270    0      error (invalid witness file) .56 .37 6.3 39 error (invalid witness file) 6.1 3.3 130 300 - -
memsafety/test-0235_false-valid-memtrack.i unknown 0 wit inspect 600    600    5400   510 310    0      error (invalid witness file) .48 .31 8.8 40 error (invalid witness file) 6.1 3.2 100 300 - -
memsafety/960521-1_true-valid-memsafety.i unknown 0 wit inspect 440    440    1600   72 300    0      - - error (invalid witness file) .54 .35 8.7 39 error (invalid witness file) 5.7 3.0 120 280
memsafety/lockfree-3.0_true-valid-memsafety.i unknown 0 wit inspect 890    900    9800   200 47    0      - - error (invalid witness file) .58 .38 8.9 40 error (invalid witness file) 5.9 3.2 120 300
memsafety/test-0019_true-valid-memsafety.i true 2 wit inspect .88 .87 8.9 29 4.0  0      - - true 4.7  2.6  47   250 true 16   9.2 200 540
memsafety/test-0102_true-valid-memsafety.i unknown 0 wit inspect 890    900    8500   550 4.2  0      - - error (invalid witness file) .50 .33 10   40 error (invalid witness file) 6.1 3.2 120 300
memsafety/test-0134_true-valid-memsafety.i unknown 0 wit inspect 890    900    12000   290 14    0      - - error (invalid witness file) .49 .30 11   40 error (invalid witness file) 6.0 3.2 120 300
memsafety/test-0158_true-valid-memsafety.i true 2 wit inspect 3.5  3.5  13   29 4.0  0      - - true 4.1  2.3  48   250 true 11   6.1 170 390
memsafety/test-0214_true-valid-memsafety.i unknown 0 wit inspect 890    900    7800   2000 5.0  0      - - error (invalid witness file) .48 .30 9.2 40 error (invalid witness file) 7.0 3.6 140 310
memsafety/test-0217_true-valid-memsafety.i unknown 0 wit inspect 890    900    6000   1900 1.7  0      - - error (invalid witness file) .64 .40 8.2 41 error (invalid witness file) 5.9 3.1 130 290
memsafety/test-0218_true-valid-memsafety.i unknown 0 wit inspect 890    900    5800   1900 2.0  0      - - error (invalid witness file) .51 .33 11   42 error (invalid witness file) 6.3 3.3 130 300
memsafety/test-0219_true-valid-memsafety.i unknown 0 wit inspect 900    900    5600   8500 20    0      - - error (invalid witness file) .51 .33 8.1 40 error (invalid witness file) 6.0 3.2 110 300
memsafety/test-0232_true-valid-memsafety.i unknown 0 wit inspect 890    900    9500   260 77    0      - - error (invalid witness file) .54 .35 11   39 error (invalid witness file) 6.2 3.3 130 300
memsafety/test-0234_true-valid-memsafety.i unknown 0 wit inspect 590    590    6500   510 310    0      - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.1 3.2 120 300
memsafety/test-0235_true-valid-memsafety.i unknown 0 wit inspect 590    590    6400   510 310    0      - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.4 3.4 130 300
memsafety/test-0236_true-valid-memsafety.i unknown 0 wit inspect 690    690    5700   510 300    0      - - error (invalid witness file) .64 .41 7.1 40 error (invalid witness file) 6.1 3.2 110 290
memsafety/test-0237_true-valid-memsafety.i unknown 0 wit inspect 660    650    5600   510 310    0      - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 6.0 3.2 140 300
memsafety/test-0504_true-valid-memsafety.i unknown 0 wit inspect 890    900    9800   380 11    0      - - error (invalid witness file) .51 .32 9.0 40 error (invalid witness file) 6.0 3.2 120 300
memsafety/test-0513_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   250 15    0      - - error (invalid witness file) .50 .33 12   42 error (invalid witness file) 6.3 3.3 110 310
memsafety/test-0521_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   750 9.3  0      - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.4 3.4 120 300
memsafety/test-memleak_nexttime_true-valid-memsafety.i unknown 0 wit inspect 890    900    6900   630 11    0      - - error (invalid witness file) .51 .34 13   40 error (invalid witness file) 6.2 3.3 120 310
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i unknown 0 wit inspect 890    900    12000   220 23    0      - - error (invalid witness file) .50 .32 9.3 39 error (invalid witness file) 6.9 3.6 110 300
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i unknown 0 wit inspect 890    900    9900   93 19    0      - - error (invalid witness file) .57 .37 7.4 40 error (invalid witness file) 5.8 3.1 110 300
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i unknown 0 wit inspect 890    900    12000   110 16    0      - - error (invalid witness file) .58 .35 7.6 40 error (invalid witness file) 7.0 3.7 140 320
memsafety-ext/tree_cnstr_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   160 13    0      - - error (invalid witness file) .58 .37 7.8 40 error (invalid witness file) 6.1 3.3 100 300
memsafety-ext/tree_dsw_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   340 10    0      - - error (invalid witness file) .47 .31 9.6 41 error (invalid witness file) 6.1 3.2 110 310
memsafety-ext/tree_of_cslls_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   520 8.0  0      - - error (invalid witness file) .51 .33 8.2 40 error (invalid witness file) 6.0 3.2 120 300
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i unknown 0 wit inspect 890    900    12000   270 11    0      - - error (invalid witness file) .64 .41 8.4 40 error (invalid witness file) 5.8 3.1 120 290
memsafety-ext/tree_stack_true-valid-memsafety.i unknown 0 wit inspect 890    900    12000   330 13    0      - - error (invalid witness file) .58 .36 8.5 39 error (invalid witness file) 6.4 3.4 130 310
memsafety-ext2/split_list_test05_false-valid-deref.i unknown 0 wit inspect 900    900    10000   15000 2.0  0      error (invalid witness file) .51 .33 3.8 40 error (invalid witness file) 6.9 3.6 130 300 - -
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i unknown 0 wit inspect 890    900    6800   550 22    0      error (invalid witness file) .53 .35 5.9 40 error (invalid witness file) 5.9 3.1 89 300 - -
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i unknown 0 wit inspect 890    900    7200   490 8.4  0      error (invalid witness file) .47 .31 3.7 40 error (invalid witness file) 5.9 3.2 110 310 - -
memsafety-ext2/length_test03_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 10    10    130   48 19    0      timeout 93    50    620   3800 true 8.3 4.5 160 320 - -
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i false(valid-deref) -16 wit inspect .82 .83 9.6 29 .99 0      timeout 97    59    940   4700 true 8.8 4.6 110 330 - -
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i unknown 0 wit inspect 890    900    7100   640 26    0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.3 3.3 120 300
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i unknown 0 wit inspect 890    900    6600   500 6.7  0      - - error (invalid witness file) .49 .32 13   40 error (invalid witness file) 7.4 3.9 130 320
memsafety-ext2/length_test03_true-valid-memsafety.i unknown 0 wit inspect 890    900    9200   190 62    0      - - error (invalid witness file) .61 .39 10   40 error (invalid witness file) 5.3 2.9 100 290
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i false(valid-deref) -16 wit inspect .79 .79 11   29 .99 0      - - out of memory 430    300    5900   7000 true 7.9 4.3 130 320
memsafety-ext2/split_list_test05_true-valid-memsafety.i unknown 0 wit inspect 900    900    10000   15000 2.0  0      - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.2 3.3 120 300
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 1 wit inspect 1.5  1.5  19   29 3.5  0      false(valid-deref) 5.7  3.0  78   270 true 8.7 4.7 160 350 - -
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 1.3  1.3  19   30 4.0  0      false(valid-deref) 5.5  2.9  89   260 true 8.5 4.6 110 330 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 1.3  1.3  15   29 4.0  0      false(valid-deref) 5.0  2.7  74   260 true 8.5 4.6 130 350 - -
list-ext-properties/960521-1_1_false-valid-free.i unknown 0 wit inspect 1.5  1.5  21   29 4.1  0      false(valid-free) 5.7  3.1  96   260 true 8.4 4.6 160 350 - -
list-ext-properties/test-0158_1_false-valid-free.i false(valid-deref) -16 wit inspect .57 .56 6.6 29 .84 0      false(valid-free) 33    20    290   1900 true 9.5 5.0 200 360 - -
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .52 .52 5.9 29 .99 0      false(valid-memtrack) 5.0  2.7  73   270 true 20   12   240 580 - -
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .47 .46 5.8 29 .84 0      false(valid-memtrack) 28    17    290   1700 true 8.1 4.4 130 350 - -
list-ext-properties/test-0232_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .57 .57 6.7 29 .99 0      false(valid-memtrack) 8.8  4.6  140   300 true 8.0 4.3 130 330 - -
list-ext-properties/960521-1_1_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   110 55    0      - - error (invalid witness file) .53 .35 7.4 40 error (invalid witness file) 6.6 3.4 120 310
list-ext-properties/list-ext_1_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   220 29    0      - - error (invalid witness file) .49 .31 9.8 39 error (invalid witness file) 6.9 3.6 120 310
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i unknown 0 wit inspect 890    900    9600   200 41    0      - - error (invalid witness file) .61 .39 11   44 error (invalid witness file) 6.0 3.2 130 300
list-ext-properties/simple-ext_1_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   190 59    0      - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.4 3.4 130 290
list-ext-properties/test-0019_1_true-valid-memsafety.i true 2 wit inspect .84 .83 10   29 3.4  0      - - true 3.8  2.1  59   260 true 39   26   480 820
list-ext-properties/test-0158_1_true-valid-memsafety.i true 2 wit inspect 1.1  1.1  12   29 4.0  0      - - true 3.6  2.0  44   250 true 11   6.1 170 380
list-ext-properties/test-0214_1_true-valid-memsafety.i unknown 0 wit inspect 890    900    2700   870 2.5  0      - - error (invalid witness file) .58 .37 6.6 40 error (invalid witness file) 5.5 2.9 120 290
list-ext-properties/test-0217_1_true-valid-memsafety.i unknown 0 wit inspect 890    900    5300   1100 3.4  0      - - error (invalid witness file) .56 .35 10   42 error (invalid witness file) 6.3 3.3 110 310
list-ext-properties/test-0232_1_true-valid-memsafety.i true 2 wit inspect 190    190    2100   150 55    0      - - true 9.3  4.9  80   290 timeout 960   910   9700 1100
list-ext-properties/test-0504_1_true-valid-memsafety.i unknown 0 wit inspect 890    900    8100   440 11    0      - - error (invalid witness file) .61 .38 7.9 39 error (invalid witness file) 6.0 3.2 120 300
list-ext-properties/test-0513_1_true-valid-memsafety.i unknown 0 wit inspect 890    900    8900   2600 16    0      - - true 7.3  3.9  120   280 timeout 960   870   17000 1700
memory-alloca/c.03-alloca_true-valid-memsafety.i unknown 0 wit inspect 160    150    1800   71 260    0      - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.5 3.4 130 300
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 1 wit inspect .39 .39 4.7 28 1.0  0      true 3.7  2.0  61   270 true 8.6 4.6 110 330 - -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c unknown 0 wit inspect .36 .35 4.2 28 1.0  0      true 3.5  1.9  54   260 true 9.2 4.9 130 350 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c unknown 0 wit inspect .36 .36 4.0 27 .84 0      true 3.6  2.0  74   250 true 8.8 4.8 120 350 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c unknown 0 wit inspect .37 .36 4.3 27 .84 0      true 3.3  1.9  41   260 true 8.8 4.7 120 340 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 1 wit inspect 610    610    5600   570 100    0      true 11    5.7  140   420 true 27   14   280 900 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c unknown 0 wit inspect 900    900    1900   430 76    0      error (invalid witness file) .55 .35 6.6 39 error (invalid witness file) 6.0 3.2 98 310 - -
ldv-memsafety/memset2_false-valid-deref-write.c unknown 0 wit inspect 75    75    930   29 180    0      error (invalid witness file) .49 .32 10   39 error (invalid witness file) 5.8 3.1 92 300 - -
ldv-memsafety/memset3_false-valid-deref-write.c unknown 0 wit inspect 270    270    3100   39 260    0      error (invalid witness file) .48 .31 9.3 40 error (invalid witness file) 5.9 3.1 80 300 - -
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c unknown 0 wit inspect 75    75    960   28 180    0      error (invalid witness file) .48 .31 7.5 40 error (invalid witness file) 5.8 3.1 110 300 - -
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c unknown 0 wit inspect 270    270    3600   38 260    0      error (invalid witness file) .52 .34 9.7 41 error (invalid witness file) 7.0 3.7 110 310 - -
ldv-memsafety/memsetNonZero_false-valid-deref-write.c unknown 0 wit inspect 270    270    3400   39 260    0      error (invalid witness file) .47 .32 6.4 40 error (invalid witness file) 5.6 3.0 90 300 - -
ldv-memsafety/memset_false-valid-deref-write.c unknown 0 wit inspect 270    270    3500   39 220    0      error (invalid witness file) .51 .33 11   39 error (invalid witness file) 5.6 3.0 110 290 - -
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c unknown 0 wit inspect 900    900    9500   1800 150    0      - - error (invalid witness file) .50 .32 13   40 error (invalid witness file) 5.9 3.1 120 310
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety.c unknown 0 wit inspect 900    900    6400   690 95    0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.0 3.1 100 300
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 2 wit inspect 670    660    5500   590 86    0      - - true 8.4  4.4  140   350 true 15   8.5 240 500
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety.c unknown 0 wit inspect 900    900    8600   800 91    0      - - error (invalid witness file) .56 .36 11   40 error (invalid witness file) 6.2 3.2 130 290
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c unknown 0 wit inspect 900    900    7000   640 86    0      - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 5.8 3.1 120 300
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety.c true 2 wit inspect 660    650    5600   620 89    0      - - true 7.6  4.1  100   340 true 12   6.6 170 410
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true 2 wit inspect 3.7  2.2  36   230 4.0  0      - - true 3.0  1.6  36   240 error 6.4 3.4 110 310
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true 2 wit inspect 3.7  2.2  36   250 3.4  0      - - true 3.2  1.8  40   240 error 6.9 3.7 130 310
ldv-memsafety/StructInitialization_true-valid-memsafety.c true 2 wit inspect 3.2  1.8  29   230 3.5  0      - - true 2.9  1.6  53   240 true 6.5 3.5 110 300
ldv-memsafety/memset2_true-valid-memsafety.c true 2 wit inspect 40    39    530   240 120    0      - - true 3.0  1.7  50   240 true 9.1 5.0 140 350
ldv-memsafety/memset3_true-valid-memsafety.c true 2 wit inspect 230    220    3400   250 240    0      - - true 3.4  2.0  41   240 true 9.3 5.1 150 360
ldv-memsafety/memsetNonZero2_true-valid-memsafety.c true 2 wit inspect 40    39    550   250 100    0      - - true 3.0  1.7  68   240 true 9.2 5.0 160 340
ldv-memsafety/memsetNonZero3_true-valid-memsafety.c true 2 wit inspect 230    220    3200   250 220    0      - - true 3.0  1.7  52   240 true 9.2 5.0 150 340
ldv-memsafety/memsetNonZero_true-valid-memsafety.c true 2 wit inspect 230    220    3000   250 200    .0041 - - true 3.3  1.8  50   240 true 8.9 4.8 170 350
ldv-memsafety/memset_true-valid-memsafety.c true 2 wit inspect 230    220    3100   240 200    0      - - true 3.0  1.7  46   250 true 9.1 5.0 180 350
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) 1 wit inspect .81 .81 10   35 .84 0      true 5.9  3.2  66   310 true 8.4 4.4 130 320 - -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 1 wit inspect 34    34    470   36 52    0      true 6.5  3.5  97   310 true 8.2 4.4 170 310 - -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 1 wit inspect 140    140    320   36 61    0      true 5.6  3.1  73   280 true 8.4 4.5 130 330 - -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-deref) 1 wit inspect 560    560    5500   350 21    0      exception 3.3  1.8  49   240 true 11   5.6 140 340 - -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(valid-deref) 1 wit inspect 600    600    6200   330 21    0      exception 3.9  2.1  68   260 true 9.1 4.9 160 320 - -
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-deref) -16 wit inspect 1.7  1.7  23   36 .99 0      false(valid-free) 7.4  3.9  75   280 true 56   49   690 490 - -
ldv-memsafety/memleaks_test12_false-valid-free.i unknown 0 wit inspect 260    260    3300   210 97    0      error (invalid witness file) .50 .32 4.0 40 error (invalid witness file) 6.7 3.5 150 320 - -
ldv-memsafety/memleaks_test17_2_false-valid-free.i unknown 0 wit inspect 890    900    8900   310 27    0      error (invalid witness file) .52 .32 11   40 error (invalid witness file) 6.2 3.3 92 330 - -
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-deref) -16 wit inspect .74 .73 9.1 30 .99 0      true 6.0  3.2  99   280 true 7.9 4.2 150 310 - -
ldv-memsafety/memleaks_test2_false-valid-free.i false(valid-deref) -16 wit inspect .52 .51 8.0 30 .99 0      false(valid-free) 6.0  3.2  94   270 false(valid-free) 8.8 4.8 150 350 - -
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-deref) -16 wit inspect .38 .38 4.6 30 .84 0      false(valid-free) 29    19    510   1600 true 7.2 3.8 120 320 - -
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-deref) -16 wit inspect .57 .56 7.4 30 .99 0      false(valid-free) 6.1  3.3  98   280 true 13   7.1 200 450 - -
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-deref) -16 wit inspect .55 .55 7.5 30 .99 0      true 6.1  3.2  97   310 true 9.3 5.0 160 360 - -
ldv-memsafety/memleaks_test10_false-valid-memtrack.i false(valid-deref) -16 wit inspect .75 .75 9.8 31 .99 0      false(valid-memtrack) 7.1  3.7  140   330 timeout 97   89   2100 530 - -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack.i false(valid-deref) -16 wit inspect 1.2  1.1  14   32 .84 0      false(valid-memtrack) 6.5  3.5  97   300 true 12   6.5 200 400 - -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .50 .50 6.1 30 .84 0      true 5.7  3.1  92   300 true 7.9 4.2 160 320 - -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 4.3  4.3  53   44 3.4  0      true 6.3  3.4  97   310 true 8.5 4.5 150 320 - -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .49 .49 5.9 30 .84 0      true 8.3  4.4  59   290 true 10   5.4 150 350 - -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.8  3.8  46   44 3.4  0      true 6.3  3.3  94   300 true 19   11   410 570 - -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 77    76    1000   74 93    0      true 7.7  4.0  100   290 true 8.7 4.7 130 340 - -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .47 .47 6.4 30 .99 0      false(valid-memtrack) 6.3  3.3  100   300 unknown 22   12   230 460 - -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .47 .47 5.5 30 .99 0      false(valid-memtrack) 6.0  3.2  94   280 unknown 15   7.9 180 350 - -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i unknown 0 wit inspect 890    900    7400   260 29    0      error (invalid witness file) .54 .35 5.5 42 error (invalid witness file) 6.0 3.2 85 300 - -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 380    380    5200   180 31    0      false(valid-memtrack) 9.8  5.2  110   330 true 11   5.9 150 360 - -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .50 .50 5.7 30 .84 0      false(valid-memtrack) 7.1  3.8  62   300 true 12   6.4 180 370 - -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 640    640    6000   160 27    0      false(valid-memtrack) 7.6  4.0  110   310 true 9.7 5.2 180 360 - -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 10    10    130   37 27    0      false(valid-memtrack) 7.1  3.8  95   280 true 11   5.8 130 380 - -
ldv-memsafety/memleaks_test1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .49 .49 5.2 30 .84 0      false(valid-memtrack) 6.3  3.3  93   300 unknown 14   7.3 150 350 - -
ldv-memsafety/memleaks_test20_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .49 .49 5.6 30 .84 0      false(valid-memtrack) 6.4  3.4  110   280 unknown 15   8.2 150 360 - -
ldv-memsafety/memleaks_test21_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .48 .48 6.2 30 .84 0      false(valid-memtrack) 6.3  3.3  88   320 unknown 14   7.7 240 340 - -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 29    29    390   34 61    0      true 6.1  3.3  130   310 true 8.7 4.6 140 330 - -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 15    15    190   30 56    0      true 6.0  3.2  110   290 true 14   8.1 200 450 - -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 29    29    390   34 61    0      true 6.6  3.5  100   280 true 7.9 4.2 110 320 - -
ldv-memsafety/memleaks_test4_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .53 .52 5.8 30 .84 0      false(valid-memtrack) 6.4  3.4  120   290 unknown 17   9.2 310 350 - -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .49 .49 5.3 30 .99 0      false(valid-memtrack) 6.7  3.6  64   270 unknown 14   7.4 180 350 - -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .47 .47 5.7 30 .99 0      true 5.9  3.2  130   300 unknown 16   8.8 230 350 - -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .50 .50 5.2 30 .99 0      true 6.7  3.6  100   300 true 12   7.0 140 470 - -
ldv-memsafety/memleaks_test6_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .51 .51 5.2 30 .99 0      false(valid-memtrack) 6.4  3.4  88   320 true 10   5.3 130 340 - -
ldv-memsafety/memleaks_test7_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .50 .50 6.1 30 .84 0      false(valid-memtrack) 6.5  3.5  98   320 true 8.0 4.2 160 330 - -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .46 .46 5.4 30 .99 0      false(valid-memtrack) 6.0  3.2  94   270 unknown 14   7.5 150 350 - -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .50 .49 6.4 30 .99 .0041 false(valid-memtrack) 6.5  3.5  130   320 unknown 15   7.8 210 350 - -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .46 .46 6.0 30 .84 0      false(valid-memtrack) 6.0  3.2  100   280 unknown 14   7.7 210 350 - -
ldv-memsafety/memleaks_test10_true-valid-memsafety.i false(valid-deref) -16 wit inspect .86 .86 10   31 .84 0      - - true 7.1  3.8  120   310 true 230   220   3300 660
ldv-memsafety/memleaks_test11_true-valid-memsafety.i false(valid-deref) -16 wit inspect 1.7  1.7  22   35 .99 0      - - true 11    5.5  110   440 true 56   49   660 530
ldv-memsafety/memleaks_test12_true-valid-memsafety.i unknown 0 wit inspect 280    280    3500   210 92    0      - - error (invalid witness file) .58 .37 12   43 error (invalid witness file) 5.8 3.1 97 300
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 2 wit inspect 31    31    270   360 3.4  0      - - true 6.4  3.4  66   310 true 760   730   9000 970
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 2 wit inspect 20    20    170   290 3.4  0      - - true 5.8  3.1  63   270 true 170   150   3000 1100
ldv-memsafety/memleaks_test15_true-valid-memsafety.i false(valid-deref) -16 wit inspect .99 .98 13   35 .99 0      - - true 11    5.8  170   420 true 9.1 4.8 170 320
ldv-memsafety/memleaks_test16_true-valid-memsafety.i true 2 wit inspect .99 .99 14   30 4.0  0      - - true 4.7  2.6  59   260 true 12   6.6 200 430
ldv-memsafety/memleaks_test17_1_true-valid-memsafety.i unknown 0 wit inspect 890    900    9200   290 27    0      - - error (invalid witness file) .52 .35 8.9 41 error (invalid witness file) 6.5 3.4 130 300
ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i unknown 0 wit inspect 890    900    9000   270 19    0      - - error (invalid witness file) .50 .32 7.5 40 error (invalid witness file) 6.1 3.2 110 290
ldv-memsafety/memleaks_test18_true-valid-memsafety.i true 2 wit inspect 840    840    7000   240 31    0      - - true 7.2  3.9  71   290 timeout 960   930   14000 780
ldv-memsafety/memleaks_test19_true-valid-memsafety.i true 2 wit inspect 1.1  1.1  12   30 4.0  0      - - true 4.8  2.6  66   260 true 230   200   2600 860
ldv-memsafety/memleaks_test1_true-valid-memsafety.i true 2 wit inspect .99 .98 12   30 3.4  0      - - true 4.6  2.5  53   260 true 10   5.6 160 360
ldv-memsafety/memleaks_test20_true-valid-memsafety.i true 2 wit inspect 1.0  1.0  14   30 4.0  0      - - true 5.9  3.2  74   260 true 16   8.9 170 460
ldv-memsafety/memleaks_test21_true-valid-memsafety.i true 2 wit inspect 1.0  1.0  13   30 4.0  0      - - true 5.8  3.2  61   260 true 12   6.7 200 400
ldv-memsafety/memleaks_test22_1_true-valid-memsafety.i true 2 wit inspect 28    28    360   33 52    0      - - true 5.2  2.8  96   260 true 320   280   5400 1100
ldv-memsafety/memleaks_test22_2_true-valid-memsafety.i true 2 wit inspect 37    37    500   36 61    0      - - true 6.2  3.3  43   260 timeout 960   920   14000 3000
ldv-memsafety/memleaks_test22_3_true-valid-memsafety.i true 2 wit inspect 37    37    410   36 61    0      - - true 6.4  3.4  78   260 timeout 960   920   17000 2600
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i false(valid-deref) -16 wit inspect 480    480    4800   340 22    0      - - exception 4.2  2.3  40   240 true 12   6.2 160 370
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i false(valid-deref) -16 wit inspect 200    200    1900   210 25    0      - - exception 3.6  2.0  66   250 true 17   9.6 230 500
ldv-memsafety/memleaks_test2_true-valid-memsafety.i true 2 wit inspect .98 .98 11   30 3.4  0      - - true 4.8  2.6  86   280 true 10   5.5 170 370
ldv-memsafety/memleaks_test3_true-valid-memsafety.i true 2 wit inspect .98 .97 13   30 3.5  0      - - true 5.9  3.2  39   290 true 11   6.0 220 360
ldv-memsafety/memleaks_test4_true-valid-memsafety.i true 2 wit inspect 1.0  1.0  12   30 4.0  0      - - true 4.6  2.5  51   260 true 13   7.3 180 510
ldv-memsafety/memleaks_test5_true-valid-memsafety.i true 2 wit inspect .99 .98 13   30 4.0  0      - - true 4.8  2.6  66   250 true 11   6.3 160 380
ldv-memsafety/memleaks_test6_true-valid-memsafety.i true 2 wit inspect 1.1  1.0  13   30 4.0  0      - - true 5.3  2.9  93   260 true 180   170   2100 660
ldv-memsafety/memleaks_test7_true-valid-memsafety.i true 2 wit inspect 1.1  1.1  13   30 3.4  0      - - true 5.6  3.0  45   260 true 88   79   1000 610
ldv-memsafety/memleaks_test8_true-valid-memsafety.i true 2 wit inspect 1.0  1.0  12   30 4.0  0      - - true 5.5  2.9  57   260 true 11   6.1 150 370
ldv-memsafety/memleaks_test9_true-valid-memsafety.i true 2 wit inspect 1.0  .99 12   30 4.0  0      - - true 6.3  3.3  77   290 true 11   6.3 180 380
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i unknown 0 wit inspect 17    17    200   28 99    0      - - error (invalid witness file) .54 .35 12   42 error (invalid witness file) 5.9 3.1 120 290
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety.i unknown 0 wit inspect 18    18    210   28 99    0      - - error (invalid witness file) .54 .35 8.3 40 error (invalid witness file) 6.3 3.4 130 320
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety.i unknown 0 wit inspect 18    18    240   28 99    0      - - error (invalid witness file) .53 .34 13   41 error (invalid witness file) 6.1 3.2 130 300
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety.i unknown 0 wit inspect 8.9  8.9  110   28 31    0      - - true 3.7  2.0  57   250 unknown 6.4 3.4 120 300
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety.i false(valid-deref) -16 wit inspect 9.6  9.6  130   28 31    0      - - true 3.6  2.0  59   260 unknown 6.6 3.5 130 300
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i unknown 0 wit inspect 17    17    200   28 99    0      error (invalid witness file) .59 .37 5.0 41 error (invalid witness file) 5.7 3.0 75 300 - -
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i unknown 0 wit inspect 18    18    270   29 99    0      error (invalid witness file) .55 .35 13   40 error (invalid witness file) 6.4 3.4 120 310 - -
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i unknown 0 wit inspect 160    160    450   29 110    0      error (invalid witness file) .54 .35 5.2 43 error (invalid witness file) 6.1 3.2 90 290 - -
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i false(valid-deref) 1 wit inspect 9.5  9.5  110   28 37    0      true 3.4  2.0  50   250 unknown 6.0 3.2 110 300 - -
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i unknown 0 wit inspect 19    19    230   28 84    0      error (invalid witness file) .49 .32 8.1 41 error (invalid witness file) 5.8 3.0 110 300 - -
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 181 -185 57000 57000 550000 91000 9600 .0082 181 950 530 11000 47000   181 980 590 16000 32000   181 680 440 9300 21000   181 7500 6800 110000 42000  
    correct results 84 119 6800 6700 69000 8200 2400 .0082 43 710 390 8200 34000   37 550 300 8200 18000   35 180 95 2200 9300   29 5900 5500 82000 23000  
        correct true 35 70 3500 3500 36000 5000 1600 .0041 16 0 0 0 0   37 0 0 0 0   35 180 95 2200 9300   29 5900 5500 82000 23000  
        correct false 49 49 3200 3200 33000 3200 770 .0041 27 710 390 8200 34000   0 550 300 8200 18000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 19 -304 720 720 7100 1500 96 0      11 210 130 2600 11000   11 250 190 4300 4600   4 470 330 6500 8900   6 340 300 4800 3000  
        incorrect true 0
        incorrect false 19 -304 720 720 7100 1500 96 0      7 210 130 2600 11000   1 250 190 4300 4600   0 470 330 6500 8900   0 340 300 4800 3000  
score (181 tasks, max score: 272) -185
Run set sv-comp17.MemSafety-Heap