Tool CBMC 5.6
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-11 10:20:18 CET [[ 2017-01-14 21:14:41 CET ]] [[ 2017-01-14 21:35:33 CET ]] [[ 2017-01-14 21:19:46 CET ]] [[ 2017-01-14 21:37:38 CET ]]
Run set sv-comp17.MemSafety-Heap
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.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 false(valid-deref) 1 wit inspect 2.7  2.7  28    51 1.6    11     error 12    6.1  230   570 out of memory 89   55   1400 7000 - -
memsafety/test-0137_false-valid-deref.i error (1) 0 wit inspect .21 .21 2.3  20 .0082 0     error (invalid witness file) .48 .32 11   40 error (invalid witness file) 5.9 3.1 130 290 - -
memsafety/test-0235_false-valid-deref.i error (1) 0 wit inspect 1.0  1.1  12    33 .0082 8.2   error (invalid witness file) .57 .35 13   40 error (invalid witness file) 6.8 3.6 100 300 - -
memsafety/960521-1_false-valid-free.i false(valid-free) 1 wit inspect 2.7  2.7  30    40 2.0    0     error 11    5.8  180   550 timeout 90   55   1700 7000 - -
memsafety/test-0158_false-valid-free.i false(valid-free) 1 wit inspect .20 .20 1.5  20 .0082 0     true 4.5  2.4  73   270 false(valid-free) 12   6.7 190 370 - -
memsafety/test-0232_false-valid-free.i false(valid-free) 1 wit inspect .21 .21 2.2  21 .0082 0     error 4.5  2.5  75   260 false(valid-free) 26   15   540 650 - -
memsafety/20020406-1_false-valid-memtrack.i error (134) 0 wit inspect 46    46    550    13000 2.4    .26  error (invalid witness file) .49 .31 7.3 39 error (invalid witness file) 6.3 3.3 130 300 - -
memsafety/20051113-1.c_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.3  3.3  44    85 .76   0     exception 3.5  1.9  52   210 true 9.4 5.0 180 340 - -
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.6  3.6  49    150 .22   0     assertion 6.1  3.3  58   270 true 8.8 4.7 170 360 - -
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 2.0  23 .0082 0     assertion 4.7  2.6  83   270 true 8.5 4.5 140 330 - -
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.8  3.8  43    160 .22   8.2   assertion 5.8  3.1  67   260 true 9.5 5.0 180 360 - -
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 1.7  20 .0082 0     error 4.2  2.3  81   250 true 9.0 4.7 180 330 - -
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .27 .26 3.1  23 .0082 .35  error 5.1  2.8  90   270 true 8.7 4.7 160 330 - -
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 1.7  22 .0082 2.4   true 4.1  2.3  87   260 true 7.6 4.0 150 320 - -
memsafety/test-0220_false-valid-memtrack.i error (1) 0 wit inspect .20 .20 2.2  21 .0082 0     error (invalid witness file) .49 .31 9.0 39 error (invalid witness file) 6.4 3.4 140 300 - -
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .18 .18 2.7  20 .0082 0     error 5.3  2.9  76   260 true 9.2 4.9 180 330 - -
memsafety/test-0234_false-valid-memtrack.i error (1) 0 wit inspect .67 .67 6.8  21 .0082 .23  error (invalid witness file) .51 .32 5.5 40 error (invalid witness file) 7.2 3.8 77 300 - -
memsafety/test-0235_false-valid-memtrack.i error (1) 0 wit inspect .77 .76 8.7  22 .0082 0     error (invalid witness file) .51 .33 12   39 error (invalid witness file) 5.2 2.8 78 290 - -
memsafety/960521-1_true-valid-memsafety.i out of memory 0 wit inspect 140    140    1900    15000 1.6    0     - - error (invalid witness file) .47 .31 5.4 39 error (invalid witness file) 6.8 3.6 85 300
memsafety/lockfree-3.0_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6200    2100 1.5    .10  - - error (invalid witness file) .66 .43 12   41 error (invalid witness file) 6.3 3.3 97 300
memsafety/test-0019_true-valid-memsafety.i true 2 wit inspect .35 .35 3.0  20 .016  0     - - true 3.9  2.2  72   250 true 20   12   260 550
memsafety/test-0102_true-valid-memsafety.i error (1) 0 wit inspect 16    16    230    270 1.6    0     - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 5.8 3.1 120 300
memsafety/test-0134_true-valid-memsafety.i error (1) 0 wit inspect .21 .21 2.3  20 .0082 0     - - error (invalid witness file) .50 .32 8.9 41 error (invalid witness file) 7.1 3.8 100 300
memsafety/test-0158_true-valid-memsafety.i true 2 wit inspect .33 .32 3.5  20 .016  .16  - - true 3.7  2.1  73   250 true 12   6.7 180 380
memsafety/test-0214_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5400    1800 .025  0     - - error (invalid witness file) .49 .32 9.4 40 error (invalid witness file) 6.5 3.4 110 310
memsafety/test-0217_true-valid-memsafety.i error (1) 0 wit inspect 42    42    560    13000 .025  .10  - - error (invalid witness file) .60 .38 8.8 44 error (invalid witness file) 6.0 3.2 110 310
memsafety/test-0218_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5300    4100 .025  0     - - error (invalid witness file) .51 .34 10   40 error (invalid witness file) 6.9 3.6 110 320
memsafety/test-0219_true-valid-memsafety.i error (1) 0 wit inspect .22 .21 2.0  20 .0082 0     - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 7.4 3.9 76 290
memsafety/test-0232_true-valid-memsafety.i error (1) 0 wit inspect 29    29    370    190 1.2    12     - - error (invalid witness file) .48 .31 8.2 39 error (invalid witness file) 6.4 3.4 85 300
memsafety/test-0234_true-valid-memsafety.i error (1) 0 wit inspect .74 .74 7.4  22 .0082 .033 - - error (invalid witness file) .51 .34 4.9 39 error (invalid witness file) 6.0 3.2 120 290
memsafety/test-0235_true-valid-memsafety.i error (1) 0 wit inspect .97 .97 11    26 .0082 0     - - error (invalid witness file) .49 .33 7.0 40 error (invalid witness file) 5.7 3.0 120 300
memsafety/test-0236_true-valid-memsafety.i error (1) 0 wit inspect .82 .81 8.5  23 .0082 0     - - error (invalid witness file) .51 .35 6.2 41 error (invalid witness file) 5.6 3.0 96 290
memsafety/test-0237_true-valid-memsafety.i error (1) 0 wit inspect .80 .80 11    23 .0082 .029 - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 7.2 3.8 100 310
memsafety/test-0504_true-valid-memsafety.i error (1) 0 wit inspect 310    310    3900    670 2.7    2.2   - - error (invalid witness file) .47 .31 6.8 40 error (invalid witness file) 5.9 3.1 110 300
memsafety/test-0513_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5600    1900 1.4    0     - - error (invalid witness file) .62 .37 8.5 40 error (invalid witness file) 6.4 3.4 110 300
memsafety/test-0521_true-valid-memsafety.i error (134) 0 wit inspect 150    150    1800    14000 4.3    .074 - - error (invalid witness file) .52 .32 13   39 error (invalid witness file) 5.1 2.8 97 290
memsafety/test-memleak_nexttime_true-valid-memsafety.i error (1) 0 wit inspect .18 .18 1.9  21 .0082 0     - - error (invalid witness file) .50 .32 8.7 40 error (invalid witness file) 6.8 3.5 89 300
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i error (1) 0 wit inspect 78    78    960    300 1.6    .10  - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 5.9 3.2 120 300
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i error (42) 0 wit inspect 850    850    8000    420 .51   .10  - - error (invalid witness file) .54 .34 10   40 error (invalid witness file) 7.0 3.7 85 300
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i error (42) 0 wit inspect 850    850    8300    630 .76   .19  - - error (invalid witness file) .51 .33 8.4 40 error (invalid witness file) 6.8 3.5 95 300
memsafety-ext/tree_cnstr_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4900    2100 1.1    .10  - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.3 3.3 110 300
memsafety-ext/tree_dsw_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4100    1700 .68   .10  - - error (invalid witness file) .55 .34 11   43 error (invalid witness file) 8.2 4.3 95 310
memsafety-ext/tree_of_cslls_true-valid-memsafety.i error (42) 0 wit inspect 850    850    8100    1000 .025  .10  - - error (invalid witness file) .55 .35 9.6 40 error (invalid witness file) 6.2 3.3 110 290
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5800    2000 .76   0     - - error (invalid witness file) .51 .34 4.6 39 error (invalid witness file) 6.5 3.4 90 300
memsafety-ext/tree_stack_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4900    1400 .63   0     - - error (invalid witness file) .51 .33 8.7 41 error (invalid witness file) 5.5 2.9 110 290
memsafety-ext2/split_list_test05_false-valid-deref.i out of memory 0 wit inspect 310    310    4100    15000 .0082 0     error (invalid witness file) .51 .33 10   40 error (invalid witness file) 6.2 3.3 130 300 - -
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 17    17    190    630 8.7    0     error 15    7.7  250   620 true 43   24   680 3400 - -
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.9  1.9  25    110 .45   0     error 7.9  4.2  150   310 true 14   7.5 280 760 - -
memsafety-ext2/length_test03_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.4  1.4  16    34 .36   0     assertion 6.1  3.2  110   280 true 10   5.3 150 420 - -
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 16    16    200    280 2.8    0     error 5.9  3.1  96   290 true 12   6.1 240 520 - -
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i error (42) 0 wit inspect 850    850    10000    2500 9.0    0     - - error (invalid witness file) .50 .31 7.1 42 error (invalid witness file) 6.1 3.2 99 300
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i error (1) 0 wit inspect 52    52    600    480 2.4    .10  - - error (invalid witness file) .69 .44 7.8 42 error (invalid witness file) 6.2 3.3 110 300
memsafety-ext2/length_test03_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4200    2000 2.0    0     - - error (invalid witness file) .59 .39 8.9 40 error (invalid witness file) 7.0 3.7 87 300
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i error (1) 0 wit inspect 200    200    2100    800 8.6    0     - - error (invalid witness file) .50 .33 7.1 40 error (invalid witness file) 7.8 4.1 73 310
memsafety-ext2/split_list_test05_true-valid-memsafety.i out of memory 0 wit inspect 210    210    2500    15000 .0082 0     - - error (invalid witness file) .48 .32 7.4 40 error (invalid witness file) 7.5 3.9 59 300
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 1 wit inspect .20 .20 1.8  20 .0082 0     error 5.4  2.9  71   270 false(valid-deref) 11   5.7 210 370 - -
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 100    100    1100    390 2.2    0     assertion 6.5  3.4  65   290 false(valid-free) 61   32   1100 1700 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .26 .26 1.9  21 .0082 0     assertion 4.4  2.4  83   260 false(valid-free) 9.0 4.8 180 330 - -
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) 1 wit inspect .20 .20 2.1  20 .0082 .16  error 4.5  2.5  82   260 false(valid-free) 10   5.6 150 360 - -
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) 1 wit inspect .18 .17 1.8  20 .0082 0     true 4.2  2.3  84   260 false(valid-free) 13   6.8 200 370 - -
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 1.6  20 .0082 0     error 5.1  2.7  88   260 true 9.5 5.0 130 320 - -
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .20 1.5  20 .0082 0     true 4.8  2.7  100   270 true 6.7 3.6 130 320 - -
list-ext-properties/test-0232_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .23 .22 2.1  20 .0082 0     error 5.0  2.7  110   270 true 9.0 4.8 190 330 - -
list-ext-properties/960521-1_1_true-valid-memsafety.i true 2 wit inspect 56    56    730    850 .50   0     - - true 10    5.3  100   420 timeout 960   900   18000 1200
list-ext-properties/list-ext_1_true-valid-memsafety.i true 2 wit inspect 110    110    1200    290 1.7    .10  - - true 22    12    260   950 timeout 960   870   29000 1600
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 2 wit inspect 45    45    650    150 1.8    .16  - - timeout 910    860    17000   4800 timeout 960   870   31000 1600
list-ext-properties/simple-ext_1_true-valid-memsafety.i true 2 wit inspect 48    48    550    270 1.9    0     - - true 19    9.7  110   650 timeout 960   890   31000 1700
list-ext-properties/test-0019_1_true-valid-memsafety.i true 2 wit inspect .33 .33 3.2  20 .016  0     - - true 5.5  3.0  66   250 true 50   32   850 740
list-ext-properties/test-0158_1_true-valid-memsafety.i true 2 wit inspect .33 .33 2.9  20 .016  0     - - true 3.9  2.1  85   250 true 11   6.1 250 380
list-ext-properties/test-0214_1_true-valid-memsafety.i true 2 wit inspect 430    430    3300    460 2.6    0     - - timeout 910    830    17000   5900 timeout 960   900   30000 2300
list-ext-properties/test-0217_1_true-valid-memsafety.i true 2 wit inspect 400    400    3400    390 3.5    0     - - timeout 950    870    15000   5400 timeout 960   870   26000 2800
list-ext-properties/test-0232_1_true-valid-memsafety.i true 2 wit inspect 6.1  6.1  88    62 .77   0     - - true 8.1  4.3  85   390 timeout 960   900   15000 1100
list-ext-properties/test-0504_1_true-valid-memsafety.i true 2 wit inspect 4.6  4.6  64    87 .46   .10  - - true 420    380    8800   4800 timeout 960   900   23000 1500
list-ext-properties/test-0513_1_true-valid-memsafety.i true 2 wit inspect 10    10    110    290 1.5    .16  - - true 7.0  3.7  100   280 timeout 960   870   23000 1900
memory-alloca/c.03-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6900    2100 11      0     - - error (invalid witness file) .51 .33 6.9 41 error (invalid witness file) 6.2 3.3 98 300
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 1 wit inspect .15 .15 .97 18 .0041 .16  error 3.6  2.0  55   260 false(valid-deref) 9.0 4.8 170 350 - -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) 1 wit inspect .15 .14 .92 18 .0041 .16  error 3.8  2.1  64   260 false(valid-deref) 11   6.0 230 360 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) 1 wit inspect .14 .13 .94 18 .0041 0     error 3.7  2.1  55   260 false(valid-deref) 7.8 4.2 140 320 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) 1 wit inspect .12 .12 .90 18 .0041 .19  error 3.3  1.9  47   270 false(valid-deref) 7.7 4.2 160 320 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 1 wit inspect 1.7  1.7  17    26 1.8    .16  error 14    7.1  190   620 timeout 98   61   1500 5600 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.7  1.7  19    26 1.8    0     error 11    5.5  160   600 timeout 96   65   1600 4600 - -
ldv-memsafety/memset2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 2.0  1.9  22    19 .22   0     error 3.1  1.7  55   250 false(valid-deref) 7.9 4.2 170 330 - -
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 2.1  2.1  20    19 .23   0     error 3.3  1.9  72   250 false(valid-deref) 7.4 4.1 150 340 - -
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 2.0  2.0  21    19 .23   .40  error 3.2  1.8  52   260 false(valid-deref) 8.1 4.4 170 320 - -
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 2.1  2.1  21    19 .23   0     error 3.3  1.9  68   260 false(valid-deref) 8.0 4.4 160 350 - -
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 1 wit inspect 2.1  2.1  21    18 .23   0     error 4.0  2.2  58   270 false(valid-deref) 7.4 4.0 140 330 - -
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 1 wit inspect 2.1  2.1  20    19 .23   0     error 3.8  2.1  52   260 false(valid-deref) 7.9 4.2 170 330 - -
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c error (42) 0 wit inspect 850    850    4300    5500 49      0     - - error (invalid witness file) .49 .31 9.5 39 error (invalid witness file) 6.7 3.6 85 300
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety.c true 2 wit inspect 2.0  2.0  25    19 2.2    0     - - true 10    5.3  69   450 true 21   13   510 550
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 2 wit inspect 1.7  1.7  19    19 1.2    0     - - true 9.5  5.0  180   420 true 25   14   340 500
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety.c true 2 wit inspect 2.0  2.0  25    19 2.2    0     - - true 11    5.7  220   460 true 29   18   310 560
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 2 wit inspect 6.1  6.1  80    67 6.6    0     - - true 36    19    480   1300 true 170   150   3100 930
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety.c true 2 wit inspect 1.7  1.7  20    19 1.3    0     - - true 9.0  4.8  97   340 true 21   12   250 500
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true 2 wit inspect .18 .18 2.1  17 .0082 .16  - - true 3.1  1.8  64   240 error 6.7 3.6 84 290
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true 2 wit inspect .19 .19 1.6  17 .0082 0     - - true 3.0  1.7  57   240 error 6.2 3.3 110 300
ldv-memsafety/StructInitialization_true-valid-memsafety.c true 2 wit inspect .19 .19 1.9  17 .0082 0     - - true 2.9  1.6  40   240 unknown 6.4 3.4 100 300
ldv-memsafety/memset2_true-valid-memsafety.c true 2 wit inspect 2.2  2.2  24    19 .23   0     - - true 3.2  1.8  39   240 true 9.8 5.3 160 350
ldv-memsafety/memset3_true-valid-memsafety.c true 2 wit inspect 2.2  2.2  22    19 .24   0     - - true 3.2  1.8  62   240 true 9.4 5.1 180 350
ldv-memsafety/memsetNonZero2_true-valid-memsafety.c true 2 wit inspect 2.2  2.2  22    19 .23   0     - - true 3.0  1.7  39   240 true 9.8 5.2 200 340
ldv-memsafety/memsetNonZero3_true-valid-memsafety.c true 2 wit inspect 2.3  2.3  19    21 .24   2.3   - - true 3.5  1.9  44   240 true 9.2 5.1 150 350
ldv-memsafety/memsetNonZero_true-valid-memsafety.c true 2 wit inspect 2.2  2.2  24    19 .24   .19  - - true 3.0  1.7  43   240 true 11   5.8 140 350
ldv-memsafety/memset_true-valid-memsafety.c true 2 wit inspect 2.1  2.1  28    19 .24   0     - - true 3.1  1.7  58   240 true 11   6.2 120 350
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) 1 wit inspect .26 .25 2.3  26 .0082 0     error 5.7  3.0  85   310 true 14   7.7 260 380 - -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 1 wit inspect 1.5  1.5  15    28 .25   0     error 6.2  3.3  94   320 true 11   5.9 220 500 - -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 1 wit inspect 1.5  1.5  19    27 .25   .23  error 5.9  3.1  120   300 true 13   6.8 180 500 - -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-deref) 1 wit inspect 10    10    120    220 .0082 0     exception 4.3  2.3  63   270 true 14   7.4 290 380 - -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(valid-deref) 1 wit inspect 10    10    110    220 .0082 0     exception 4.3  2.4  64   250 true 16   8.6 250 390 - -
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) 1 wit inspect .25 .24 2.8  27 .0082 0     error 6.6  3.5  120   310 true 36   26   1100 590 - -
ldv-memsafety/memleaks_test12_false-valid-free.i error (1) 0 wit inspect .37 .36 3.9  36 .0082 0     error (invalid witness file) .48 .32 8.6 39 error (invalid witness file) 6.2 3.2 110 300 - -
ldv-memsafety/memleaks_test17_2_false-valid-free.i false(valid-free) 1 wit inspect 1.6  1.6  17    53 .21   0     error 6.5  3.4  120   310 out of memory 67   40   1400 7000 - -
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) 1 wit inspect .21 .22 2.0  23 .0082 2.3   error 7.1  3.8  63   320 false(valid-free) 15   8.1 320 420 - -
ldv-memsafety/memleaks_test2_false-valid-free.i false(valid-free) 1 wit inspect .21 .21 1.6  23 .0082 2.3   error 5.3  2.8  96   280 true 9.5 5.1 210 350 - -
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) 1 wit inspect .22 .21 1.7  21 .0082 0     error 6.2  3.3  87   310 false(valid-free) 7.8 4.2 140 320 - -
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) 1 wit inspect .23 .22 1.8  21 .0082 0     error 5.7  3.1  110   320 false(valid-free) 11   6.2 240 370 - -
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) 1 wit inspect .20 .19 2.0  20 .0082 0     error 5.7  3.1  98   320 false(valid-free) 12   6.1 220 360 - -
ldv-memsafety/memleaks_test10_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .25 .25 2.3  22 .0082 0     error 5.6  3.0  84   300 true 10   5.3 220 340 - -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .26 .26 2.5  25 .0082 0     error 5.7  3.1  110   300 true 9.7 5.1 160 330 - -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .20 .19 2.0  21 .0082 0     error 7.0  3.8  64   310 true 9.8 5.2 110 320 - -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .29 .33 2.6  35 .0082 11     error 5.8  3.1  120   310 true 10   5.5 140 320 - -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .22 .23 1.9  23 .0082 2.4   error 5.6  3.0  100   310 true 8.0 4.2 160 330 - -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .23 .23 3.0  24 .0082 0     error 6.7  3.6  85   310 true 8.8 4.7 160 350 - -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 2.8  21 .0082 0     error 6.7  3.6  97   310 true 8.6 4.6 160 330 - -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .23 .23 1.7  21 .0082 0     error 5.9  3.2  60   270 true 7.8 4.2 160 320 - -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 1.8  20 .0082 0     error 6.7  3.6  52   290 true 7.6 4.0 160 310 - -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.2  2.1  21    67 .29   0     error 6.7  3.5  130   290 true 10   5.3 210 470 - -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.9  1.9  20    55 .23   0     error 5.8  3.1  120   280 true 9.5 5.0 170 390 - -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .24 .23 2.3  24 .0082 0     error 5.6  3.0  95   310 true 8.3 4.4 170 330 - -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.5  1.5  15    42 .16   0     error 6.5  3.5  120   320 true 9.4 5.0 150 320 - -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.0  1.0  12    27 .14   .25  error 6.6  3.5  130   330 true 8.4 4.5 180 330 - -
ldv-memsafety/memleaks_test1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 1.8  20 .0082 0     error 5.6  3.0  100   310 true 7.4 3.9 150 320 - -
ldv-memsafety/memleaks_test20_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 1.7  21 .0082 0     error 5.2  2.8  88   290 true 7.6 4.0 150 320 - -
ldv-memsafety/memleaks_test21_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .22 .22 1.7  21 .0082 0     error 5.1  2.7  68   300 true 7.3 3.9 150 320 - -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.5  1.5  14    25 .22   0     error 6.7  3.6  85   310 true 11   5.7 200 490 - -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.4  1.4  15    24 .17   .13  error 6.0  3.2  110   300 true 11   5.7 210 470 - -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.5  1.5  14    27 .22   0     error 6.1  3.3  100   300 true 11   5.9 200 510 - -
ldv-memsafety/memleaks_test4_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .20 .20 1.7  21 .0082 .16  error 5.4  2.9  98   290 true 7.5 4.0 140 320 - -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 1.7  21 .0082 0     error 4.7  2.6  90   270 true 7.0 3.8 140 320 - -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .20 .19 1.7  21 .0082 0     error 5.0  2.7  70   270 true 8.3 4.4 160 340 - -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .24 .23 1.7  21 .0082 0     error 5.4  2.9  98   310 true 9.8 5.2 100 330 - -
ldv-memsafety/memleaks_test6_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 1.9  21 .0082 0     error 5.4  2.9  74   290 true 8.0 4.2 160 320 - -
ldv-memsafety/memleaks_test7_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .23 .27 2.4  33 .0082 13     error 5.7  3.1  90   320 true 8.3 4.4 150 330 - -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 1.6  21 .0082 .16  error 6.1  3.3  120   320 true 7.3 3.9 150 330 - -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 2.0  21 .0082 0     error 4.9  2.6  97   270 true 7.7 4.1 150 320 - -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .20 .20 2.2  21 .0082 0     error 5.9  3.1  82   310 true 8.4 4.5 120 330 - -
ldv-memsafety/memleaks_test10_true-valid-memsafety.i true 2 wit inspect .44 .44 5.1  23 .016  0     - - true 5.2  2.8  81   260 timeout 960   930   32000 860
ldv-memsafety/memleaks_test11_true-valid-memsafety.i true 2 wit inspect .49 .48 4.4  26 .016  .16  - - true 5.5  3.0  76   260 timeout 960   910   33000 930
ldv-memsafety/memleaks_test12_true-valid-memsafety.i error (1) 0 wit inspect .36 .35 4.7  36 .0082 0     - - error (invalid witness file) .52 .34 9.2 39 error (invalid witness file) 6.7 3.6 86 300
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 2 wit inspect .47 .51 4.6  38 .016  12     - - true 5.2  2.8  110   260 true 810   780   17000 1100
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 2 wit inspect .44 .43 6.1  26 .016  0     - - true 5.9  3.1  80   260 true 200   170   3900 1100
ldv-memsafety/memleaks_test15_true-valid-memsafety.i error (1) 0 wit inspect .24 .23 2.4  23 .0082 0     - - error (invalid witness file) .48 .30 6.9 39 error (invalid witness file) 7.2 3.8 120 310
ldv-memsafety/memleaks_test16_true-valid-memsafety.i true 2 wit inspect .38 .38 3.4  21 .016  0     - - true 5.4  2.9  110   260 true 16   8.6 170 430
ldv-memsafety/memleaks_test17_1_true-valid-memsafety.i true 2 wit inspect 3.2  3.2  37    66 .35   .10  - - true 8.5  4.5  86   290 timeout 960   930   19000 1900
ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i error (134) 0 wit inspect 580    580    4500    14000 .40   .10  - - error (invalid witness file) .54 .33 10   39 error (invalid witness file) 6.9 3.6 89 300
ldv-memsafety/memleaks_test18_true-valid-memsafety.i true 2 wit inspect 2.1  2.1  19    41 .21   .13  - - true 7.0  3.7  140   280 timeout 960   920   25000 970
ldv-memsafety/memleaks_test19_true-valid-memsafety.i true 2 wit inspect .40 .40 3.5  21 .016  0     - - true 5.0  2.7  67   250 true 230   200   5500 830
ldv-memsafety/memleaks_test1_true-valid-memsafety.i true 2 wit inspect .36 .36 3.8  21 .016  .19  - - true 4.6  2.5  86   260 true 11   6.0 190 370
ldv-memsafety/memleaks_test20_true-valid-memsafety.i true 2 wit inspect .36 .36 3.4  21 .016  0     - - true 5.0  2.7  50   260 true 15   8.5 260 460
ldv-memsafety/memleaks_test21_true-valid-memsafety.i true 2 wit inspect .40 .43 3.7  33 .016  13     - - true 5.2  2.8  110   260 true 14   8.0 190 430
ldv-memsafety/memleaks_test22_1_true-valid-memsafety.i true 2 wit inspect 1.7  1.7  19    26 .21   0     - - true 5.3  2.8  94   260 true 330   290   8000 1000
ldv-memsafety/memleaks_test22_2_true-valid-memsafety.i true 2 wit inspect 1.9  1.9  17    28 .27   0     - - true 6.1  3.2  88   290 timeout 960   910   21000 2600
ldv-memsafety/memleaks_test22_3_true-valid-memsafety.i true 2 wit inspect 1.8  1.8  16    28 .27   0     - - true 5.5  3.0  89   260 timeout 960   900   18000 2300
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5900    10000 8.6    0     - - error (invalid witness file) .55 .35 11   41 error (invalid witness file) 7.5 4.0 87 310
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6900    10000 8.0    .10  - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 5.7 3.0 110 300
ldv-memsafety/memleaks_test2_true-valid-memsafety.i true 2 wit inspect .38 .37 3.3  21 .016  0     - - true 5.2  2.8  51   260 true 13   6.9 150 360
ldv-memsafety/memleaks_test3_true-valid-memsafety.i true 2 wit inspect .38 .37 3.3  21 .016  0     - - true 4.8  2.6  75   260 true 11   6.3 220 360
ldv-memsafety/memleaks_test4_true-valid-memsafety.i true 2 wit inspect .38 .38 3.3  21 .016  .19  - - true 4.9  2.6  63   260 true 17   9.7 200 490
ldv-memsafety/memleaks_test5_true-valid-memsafety.i true 2 wit inspect .36 .36 4.3  21 .016  0     - - true 4.5  2.5  53   250 true 13   7.1 210 420
ldv-memsafety/memleaks_test6_true-valid-memsafety.i true 2 wit inspect .37 .36 3.1  21 .016  0     - - true 5.4  2.9  43   290 true 170   160   4500 660
ldv-memsafety/memleaks_test7_true-valid-memsafety.i true 2 wit inspect .36 .36 3.7  21 .016  0     - - true 4.8  2.6  89   260 true 86   76   2800 600
ldv-memsafety/memleaks_test8_true-valid-memsafety.i true 2 wit inspect .40 .39 3.3  21 .016  0     - - true 4.9  2.6  62   290 true 13   7.2 160 370
ldv-memsafety/memleaks_test9_true-valid-memsafety.i true 2 wit inspect .39 .39 3.0  21 .016  0     - - true 4.7  2.5  100   260 true 13   7.2 180 380
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i true 2 wit inspect .36 .35 2.8  18 .016  0     - - true 3.2  1.8  53   240 unknown 8.3 4.4 90 320
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety.i true 2 wit inspect .63 .62 6.0  19 .053  0     - - true 3.4  1.9  70   250 unknown 6.6 3.5 130 310
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety.i true 2 wit inspect .71 .71 5.3  21 .057  .23  - - true 3.2  1.8  33   240 unknown 7.8 4.1 81 300
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety.i true 2 wit inspect .93 .93 9.5  19 .098  0     - - true 3.1  1.7  40   240 unknown 7.4 3.9 75 300
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety.i true 2 wit inspect 1.0  1.0  9.1  19 .11   0     - - true 3.2  1.8  52   240 unknown 7.1 3.7 150 320
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i false(valid-deref) 1 wit inspect .18 .17 1.8  18 .0082 0     error 3.2  1.8  75   250 unknown 6.0 3.2 130 300 - -
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i false(valid-deref) 1 wit inspect .50 .49 4.4  19 .037  0     error 3.2  1.8  71   250 unknown 7.5 3.9 130 320 - -
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i false(valid-deref) 1 wit inspect .86 .85 7.6  19 .082  0     assertion 3.3  1.8  69   260 unknown 6.5 3.5 130 300 - -
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i false(valid-deref) 1 wit inspect .78 .77 11    19 .086  0     assertion 4.2  2.3  51   250 unknown 6.7 3.6 120 310 - -
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i false(valid-free) 1 wit inspect .49 .48 5.1  19 .041  0     error 3.3  1.9  67   250 unknown 6.4 3.4 120 320 - -
../../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 190 18000 18000 140000 160000 180 110 181 470 250 7600 25000   181 1300 760 25000 66000   181 3500 3100 63000 38000   181 17000 16000 430000 55000  
    correct results 136 190 1400 1400 13000 7900 58 83 4 460 250 7600 25000   72 1300 730 24000 64000   51 3500 3100 63000 37000   31 17000 16000 430000 44000  
        correct true 54 108 1200 1200 11000 3900 32 29 4 0 0 0 0   51 0 0 0 0   51 3500 3100 63000 37000   31 17000 16000 430000 44000  
        correct false 82 82 220 220 2400 4000 27 54 0 460 250 7600 25000   21 1300 730 24000 64000   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 (181 tasks, max score: 272) 190
Run set sv-comp17.MemSafety-Heap