Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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:52:43 CET [[ 2017-01-15 00:23:14 CET ]] [[ 2017-01-15 00:35:58 CET ]] [[ 2017-01-15 00:29:47 CET ]] [[ 2017-01-15 00:40:29 CET ]]
Run set sv-comp17.MemSafety-Heap
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.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 48    48    600   70 1.7  0   error (invalid witness file) .51 .34 3.9 40 error (invalid witness file) 6.1 3.2 120 300 - -
memsafety/test-0137_false-valid-deref.i out of memory 0 wit inspect 81    81    750   15000 .99 0   error (invalid witness file) .53 .35 6.7 43 error (invalid witness file) 6.0 3.2 120 290 - -
memsafety/test-0235_false-valid-deref.i timeout 0 wit inspect 900    900    12000   150 .84 0   error (invalid witness file) .52 .33 8.9 40 error (invalid witness file) 6.2 3.3 130 310 - -
memsafety/960521-1_false-valid-free.i false(valid-free) 1 wit inspect 48    48    550   71 1.7  0   error (invalid witness file) .50 .31 8.2 39 error (invalid witness file) 5.7 3.1 120 300 - -
memsafety/test-0158_false-valid-free.i false(valid-free) 1 wit inspect 7.1  7.1  61   3300 1.7  0   error (invalid witness file) .55 .35 9.6 44 error (invalid witness file) 5.7 3.1 100 290 - -
memsafety/test-0232_false-valid-free.i out of memory 0 wit inspect 47    46    590   15000 .99 0   error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.5 3.0 110 280 - -
memsafety/20020406-1_false-valid-memtrack.i out of memory 0 wit inspect 150    140    2000   15000 .99 0   error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.6 3.5 130 310 - -
memsafety/20051113-1.c_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 26    26    340   1000 1.7  0   error (invalid witness file) .51 .34 8.9 39 error (invalid witness file) 6.1 3.3 120 300 - -
memsafety/lockfree-3.1_false-valid-memtrack.i timeout 0 wit inspect 900    900    10000   13000 .99 0   error (invalid witness file) .50 .33 4.2 39 error (invalid witness file) 5.9 3.1 120 300 - -
memsafety/lockfree-3.2_false-valid-memtrack.i timeout 0 wit inspect 900    900    11000   13000 .84 0   error (invalid witness file) .49 .33 5.4 41 error (invalid witness file) 5.9 3.1 110 300 - -
memsafety/lockfree-3.3_false-valid-memtrack.i timeout 0 wit inspect 900    900    9500   13000 .84 0   error (invalid witness file) .48 .30 6.5 39 error (invalid witness file) 6.2 3.3 120 300 - -
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 2.2 24 2.0  0   error (invalid witness file) .51 .32 9.2 39 error (invalid witness file) 5.9 3.2 120 290 - -
memsafety/test-0102_false-valid-memtrack.i timeout 0 wit inspect 900    900    6800   8500 .84 0   error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.2 3.2 120 300 - -
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 .16 2.2 24 2.0  0   error (invalid witness file) .53 .33 9.8 40 error (invalid witness file) 5.2 2.9 120 280 - -
memsafety/test-0220_false-valid-memtrack.i out of memory 0 wit inspect 830    830    7700   15000 .99 0   error (invalid witness file) .49 .31 7.7 40 error (invalid witness file) 5.7 3.1 130 300 - -
memsafety/test-0232_false-valid-memtrack.i out of memory 0 wit inspect 420    420    3400   15000 2.0  0   error (invalid witness file) .55 .35 9.4 40 error (invalid witness file) 6.2 3.3 120 300 - -
memsafety/test-0234_false-valid-memtrack.i timeout 0 wit inspect 900    900    13000   150 .84 0   error (invalid witness file) .53 .35 9.1 41 error (invalid witness file) 6.8 3.6 130 310 - -
memsafety/test-0235_false-valid-memtrack.i timeout 0 wit inspect 900    900    12000   150 .99 0   error (invalid witness file) .50 .33 5.9 39 error (invalid witness file) 6.0 3.1 130 300 - -
memsafety/960521-1_true-valid-memsafety.i true 2 wit inspect 1.7  1.7  21   67 2.0  0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.2 3.2 130 300
memsafety/lockfree-3.0_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   13000 .99 0   - - error (invalid witness file) .49 .34 4.1 39 error (invalid witness file) 6.0 3.2 110 300
memsafety/test-0019_true-valid-memsafety.i true 2 wit inspect .18 .18 1.9 24 2.0  0   - - error (invalid witness file) .51 .35 4.5 41 error (invalid witness file) 5.7 3.0 120 300
memsafety/test-0102_true-valid-memsafety.i timeout 0 wit inspect 900    900    5200   8500 .84 0   - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.7 3.5 140 310
memsafety/test-0134_true-valid-memsafety.i out of memory 0 wit inspect 80    80    730   15000 .84 0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.9 3.2 130 300
memsafety/test-0158_true-valid-memsafety.i true 2 wit inspect .22 .22 2.5 24 2.0  0   - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 6.0 3.2 110 290
memsafety/test-0214_true-valid-memsafety.i out of memory 0 wit inspect 280    280    3300   15000 .99 0   - - error (invalid witness file) .49 .32 14   40 error (invalid witness file) 6.2 3.3 120 310
memsafety/test-0217_true-valid-memsafety.i out of memory 0 wit inspect 52    51    630   15000 .84 0   - - error (invalid witness file) .50 .33 5.8 39 error (invalid witness file) 6.2 3.2 120 300
memsafety/test-0218_true-valid-memsafety.i out of memory 0 wit inspect 52    52    610   15000 .95 0   - - error (invalid witness file) .54 .35 13   42 error (invalid witness file) 7.1 3.8 140 330
memsafety/test-0219_true-valid-memsafety.i out of memory 0 wit inspect 860    860    4500   15000 .99 0   - - error (invalid witness file) .56 .36 8.1 43 error (invalid witness file) 6.6 3.4 120 310
memsafety/test-0232_true-valid-memsafety.i timeout 0 wit inspect 900    900    7900   7300 .99 0   - - error (invalid witness file) .53 .34 14   43 error (invalid witness file) 5.8 3.1 120 290
memsafety/test-0234_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   150 .84 0   - - error (invalid witness file) .50 .32 5.4 40 error (invalid witness file) 6.4 3.4 130 310
memsafety/test-0235_true-valid-memsafety.i timeout 0 wit inspect 900    900    13000   150 .99 0   - - error (invalid witness file) .54 .34 14   40 error (invalid witness file) 6.3 3.4 110 310
memsafety/test-0236_true-valid-memsafety.i timeout 0 wit inspect 900    900    12000   150 .84 0   - - error (invalid witness file) .48 .31 3.9 39 error (invalid witness file) 6.2 3.2 120 300
memsafety/test-0237_true-valid-memsafety.i timeout 0 wit inspect 900    900    13000   150 .99 0   - - error (invalid witness file) .50 .31 4.6 40 error (invalid witness file) 6.9 3.6 130 320
memsafety/test-0504_true-valid-memsafety.i timeout 0 wit inspect 900    900    5100   9200 .84 0   - - error (invalid witness file) .54 .35 4.2 40 error (invalid witness file) 5.8 3.1 120 290
memsafety/test-0513_true-valid-memsafety.i out of memory 0 wit inspect 120    110    1400   15000 .84 0   - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 6.3 3.4 140 310
memsafety/test-0521_true-valid-memsafety.i out of memory 0 wit inspect 10    9.9  140   15000 .99 0   - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 5.7 3.0 120 290
memsafety/test-memleak_nexttime_true-valid-memsafety.i true 2 wit inspect 7.9  7.9  56   3300 2.0  0   - - error (invalid witness file) .49 .31 5.2 39 error (invalid witness file) 6.0 3.1 120 300
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i out of memory 0 wit inspect 80    80    870   15000 .99 0   - - error (invalid witness file) .50 .33 9.4 41 error (invalid witness file) 5.8 3.1 110 290
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i out of memory 0 wit inspect 53    52    550   15000 .99 0   - - error (invalid witness file) .52 .34 6.8 39 error (invalid witness file) 6.3 3.3 120 300
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i out of memory 0 wit inspect 54    53    630   15000 .99 0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.9 3.1 99 300
memsafety-ext/tree_cnstr_true-valid-memsafety.i out of memory 0 wit inspect 95    95    970   15000 .99 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.0 3.2 92 300
memsafety-ext/tree_dsw_true-valid-memsafety.i out of memory 0 wit inspect 97    97    1000   15000 .84 0   - - error (invalid witness file) .50 .32 9.9 40 error (invalid witness file) 6.4 3.3 130 300
memsafety-ext/tree_of_cslls_true-valid-memsafety.i out of memory 0 wit inspect 580    580    4400   15000 .84 0   - - error (invalid witness file) .52 .34 10   40 error (invalid witness file) 6.0 3.2 100 300
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i out of memory 0 wit inspect 120    120    1500   15000 .99 0   - - error (invalid witness file) .51 .33 12   42 error (invalid witness file) 6.5 3.4 150 290
memsafety-ext/tree_stack_true-valid-memsafety.i out of memory 0 wit inspect 93    93    1000   15000 .84 0   - - error (invalid witness file) .50 .34 4.4 39 error (invalid witness file) 6.4 3.4 130 300
memsafety-ext2/split_list_test05_false-valid-deref.i timeout 0 wit inspect 900    900    6300   7300 .84 0   error (invalid witness file) .50 .32 9.8 40 error (invalid witness file) 6.4 3.4 120 310 - -
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i timeout 0 wit inspect 900    900    5000   8900 .99 0   error (invalid witness file) .51 .34 14   40 error (invalid witness file) 6.2 3.3 130 300 - -
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i out of memory 0 wit inspect 750    750    7000   15000 .99 0   error (invalid witness file) .52 .32 9.9 40 error (invalid witness file) 6.0 3.2 130 300 - -
memsafety-ext2/length_test03_false-valid-memtrack.i out of memory 0 wit inspect 550    550    5100   15000 2.0  0   error (invalid witness file) .48 .33 9.3 40 error (invalid witness file) 5.6 3.0 110 290 - -
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i out of memory 0 wit inspect 140    140    1100   15000 .99 0   error (invalid witness file) .51 .33 9.8 41 error (invalid witness file) 6.0 3.2 110 300 - -
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i timeout 0 wit inspect 900    900    4300   8900 .99 0   - - error (invalid witness file) .50 .32 6.4 40 error (invalid witness file) 6.8 3.5 140 300
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i out of memory 0 wit inspect 770    770    4900   15000 .84 0   - - error (invalid witness file) .52 .33 9.5 42 error (invalid witness file) 5.7 3.0 120 290
memsafety-ext2/length_test03_true-valid-memsafety.i timeout 0 wit inspect 900    900    6800   4400 .84 0   - - error (invalid witness file) .51 .34 13   40 error (invalid witness file) 6.4 3.4 120 310
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i out of memory 0 wit inspect 140    140    1100   15000 .99 0   - - error (invalid witness file) .61 .39 13   43 error (invalid witness file) 6.8 3.6 140 310
memsafety-ext2/split_list_test05_true-valid-memsafety.i timeout 0 wit inspect 900    900    6200   7200 .99 0   - - error (invalid witness file) .50 .33 13   39 error (invalid witness file) 5.8 3.1 120 300
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 1 wit inspect 20    20    280   1900 1.7  0   error (invalid witness file) .50 .32 4.3 39 error (invalid witness file) 7.1 3.7 130 320 - -
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 470    470    4700   2700 2.0  0   error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.6 3.5 130 310 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i out of memory 0 wit inspect 460    460    3900   15000 1.8  0   error (invalid witness file) .51 .34 3.5 40 error (invalid witness file) 6.1 3.2 120 300 - -
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) 1 wit inspect 41    41    470   1900 2.0  0   error (invalid witness file) .50 .33 8.5 40 error (invalid witness file) 6.0 3.2 120 300 - -
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) 1 wit inspect .25 .25 2.8 25 2.0  0   error (invalid witness file) .50 .32 7.3 40 error (invalid witness file) 6.0 3.1 130 300 - -
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .20 .20 2.3 25 2.0  0   error (invalid witness file) .50 .32 9.4 41 error (invalid witness file) 5.7 3.1 110 300 - -
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 .16 1.8 24 1.7  0   error (invalid witness file) .50 .33 9.6 40 error (invalid witness file) 5.8 3.1 110 290 - -
list-ext-properties/test-0232_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 34    34    350   1600 2.0  0   error (invalid witness file) .52 .34 8.3 43 error (invalid witness file) 5.8 3.1 120 300 - -
list-ext-properties/960521-1_1_true-valid-memsafety.i true 2 wit inspect 26    26    320   1200 2.0  0   - - error (invalid witness file) .53 .34 13   40 error (invalid witness file) 6.3 3.3 120 310
list-ext-properties/list-ext_1_true-valid-memsafety.i true 2 wit inspect 270    270    2400   2300 2.0  0   - - error (invalid witness file) .52 .36 9.8 40 error (invalid witness file) 6.7 3.5 130 310
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 2 wit inspect 110    110    1400   3500 1.7  0   - - error (invalid witness file) .51 .34 13   40 error (invalid witness file) 6.4 3.4 120 310
list-ext-properties/simple-ext_1_true-valid-memsafety.i true 2 wit inspect 900    900    7600   4700 1.7  0   - - error (invalid witness file) .46 .30 7.2 39 error (invalid witness file) 5.9 3.1 130 290
list-ext-properties/test-0019_1_true-valid-memsafety.i true 2 wit inspect .21 .21 2.1 24 1.7  0   - - error (invalid witness file) .54 .36 12   41 error (invalid witness file) 6.0 3.2 110 300
list-ext-properties/test-0158_1_true-valid-memsafety.i true 2 wit inspect .21 .21 2.5 24 2.0  0   - - error (invalid witness file) .56 .36 13   41 error (invalid witness file) 5.8 3.1 110 290
list-ext-properties/test-0214_1_true-valid-memsafety.i timeout 0 wit inspect 900    900    2000   5400 .99 0   - - error (invalid witness file) .53 .33 13   39 error (invalid witness file) 6.7 3.5 140 310
list-ext-properties/test-0217_1_true-valid-memsafety.i timeout 0 wit inspect 900    900    6800   5100 .99 0   - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.3 3.4 120 300
list-ext-properties/test-0232_1_true-valid-memsafety.i true 2 wit inspect 59    59    680   1600 1.7  0   - - error (invalid witness file) .52 .35 7.8 41 error (invalid witness file) 5.6 3.1 120 290
list-ext-properties/test-0504_1_true-valid-memsafety.i timeout 0 wit inspect 900    900    2400   8000 .99 0   - - error (invalid witness file) .50 .34 7.2 42 error (invalid witness file) 6.0 3.2 120 310
list-ext-properties/test-0513_1_true-valid-memsafety.i out of memory 0 wit inspect 99    99    1200   15000 .99 0   - - error (invalid witness file) .52 .35 9.2 40 error (invalid witness file) 6.8 3.5 130 320
memory-alloca/c.03-alloca_true-valid-memsafety.i true 2 wit inspect 18    18    210   1300 1.7  0   - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.8 3.6 140 310
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 1 wit inspect 440    440    6200   930 2.0  0   error (invalid witness file) .52 .35 10   39 error (invalid witness file) 5.8 3.1 120 290 - -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 440    440    5500   930 2.0  0   error (invalid witness file) .49 .31 6.0 40 error (invalid witness file) 6.2 3.2 120 300 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) 1 wit inspect 4.7  4.7  61   82 1.7  0   error (invalid witness file) .48 .32 8.9 40 error (invalid witness file) 6.0 3.2 130 290 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.6  4.6  63   39 2.0  0   error (invalid witness file) .50 .32 6.0 39 error (invalid witness file) 6.1 3.2 120 300 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 1 wit inspect .79 .79 11   23 2.0  0   error (invalid witness file) .50 .32 7.4 42 error (invalid witness file) 6.0 3.2 120 300 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(valid-deref) 1 wit inspect 3.0  3.0  6.8 23 2.0  0   error (invalid witness file) .50 .31 5.5 39 error (invalid witness file) 6.7 3.5 140 310 - -
ldv-memsafety/memset2_false-valid-deref-write.c false(valid-deref) 1 wit inspect .44 .44 5.6 23 2.0  0   error (invalid witness file) .52 .35 7.5 40 error (invalid witness file) 5.9 3.2 130 300 - -
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.6  1.6  23   23 2.0  0   error (invalid witness file) .55 .35 14   42 error (invalid witness file) 5.7 3.1 120 300 - -
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) 1 wit inspect .44 .45 5.5 23 1.7  0   error (invalid witness file) .48 .32 3.5 39 error (invalid witness file) 5.6 3.0 110 290 - -
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.7  1.7  22   23 1.8  0   error (invalid witness file) .51 .33 6.5 40 error (invalid witness file) 5.9 3.2 110 300 - -
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.7  1.7  23   23 2.0  0   error (invalid witness file) .48 .32 6.3 39 error (invalid witness file) 6.1 3.2 130 300 - -
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.6  1.6  24   23 2.0  0   error (invalid witness file) .51 .35 4.2 39 error (invalid witness file) 5.3 2.9 110 290 - -
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c true 2 wit inspect 8.4  8.4  110   100 2.0  0   - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 5.8 3.1 120 310
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety.c true 2 wit inspect .99 .99 12   23 2.0  0   - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 6.0 3.2 110 290
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 2 wit inspect .63 .63 7.7 23 2.0  0   - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.2 3.3 120 300
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety.c true 2 wit inspect .99 .99 11   23 2.0  0   - - error (invalid witness file) .50 .31 7.3 40 error (invalid witness file) 5.7 3.0 110 300
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 2 wit inspect 4.2  4.2  63   38 2.0  0   - - error (invalid witness file) .59 .37 14   46 error (invalid witness file) 5.6 3.0 110 280
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety.c true 2 wit inspect .68 .68 8.0 23 1.7  0   - - error (invalid witness file) .48 .31 9.7 40 error (invalid witness file) 5.7 3.1 120 300
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true 2 wit inspect .21 .21 2.2 25 2.0  0   - - error (invalid witness file) .53 .34 12   39 error (invalid witness file) 6.4 3.4 120 300
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true 2 wit inspect .20 .20 2.3 25 2.0  0   - - error (invalid witness file) .57 .36 14   42 error (invalid witness file) 6.0 3.2 130 300
ldv-memsafety/StructInitialization_true-valid-memsafety.c true 2 wit inspect .16 .16 1.7 23 2.0  0   - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.0 3.1 110 300
ldv-memsafety/memset2_true-valid-memsafety.c true 2 wit inspect .42 .42 5.5 23 2.0  0   - - error (invalid witness file) .50 .32 9.4 40 error (invalid witness file) 5.9 3.1 110 310
ldv-memsafety/memset3_true-valid-memsafety.c true 2 wit inspect 1.6  1.6  18   23 2.0  0   - - error (invalid witness file) .49 .31 10   39 error (invalid witness file) 5.7 3.1 110 290
ldv-memsafety/memsetNonZero2_true-valid-memsafety.c true 2 wit inspect .41 .41 5.0 23 2.0  0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.2 3.3 120 300
ldv-memsafety/memsetNonZero3_true-valid-memsafety.c true 2 wit inspect 1.6  1.6  22   23 1.7  0   - - error (invalid witness file) .50 .34 7.9 40 error (invalid witness file) 5.7 3.0 110 300
ldv-memsafety/memsetNonZero_true-valid-memsafety.c true 2 wit inspect 1.7  1.6  21   23 2.0  0   - - error (invalid witness file) .57 .36 15   42 error (invalid witness file) 6.1 3.2 130 300
ldv-memsafety/memset_true-valid-memsafety.c true 2 wit inspect 1.6  1.6  19   23 2.0  0   - - error (invalid witness file) .53 .33 11   41 error (invalid witness file) 6.0 3.2 130 300
ldv-memsafety/memleaks_test14_3_false-valid-deref.i out of memory 0 wit inspect 470    470    4400   15000 2.0  0   error (invalid witness file) .49 .32 8.5 40 error (invalid witness file) 6.9 3.6 130 310 - -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 1 wit inspect .40 .40 4.6 26 1.7  0   error (invalid witness file) .51 .35 4.8 42 error (invalid witness file) 5.8 3.1 130 300 - -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 1 wit inspect .42 .42 5.5 26 2.0  0   error (invalid witness file) .50 .33 10   42 error (invalid witness file) 5.5 3.0 110 290 - -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i out of memory 0 wit inspect 600    600    5400   15000 2.0  0   error (invalid witness file) .52 .33 12   41 error (invalid witness file) 5.9 3.1 120 290 - -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i out of memory 0 wit inspect 800    800    6100   15000 2.0  0   error (invalid witness file) .51 .32 7.9 40 error (invalid witness file) 6.6 3.5 140 310 - -
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) 1 wit inspect .76 .76 8.8 28 1.7  0   error (invalid witness file) .51 .33 5.2 41 error (invalid witness file) 6.0 3.2 120 310 - -
ldv-memsafety/memleaks_test12_false-valid-free.i unknown 0 wit inspect 240    240    2800   10000 2.0  0   error (invalid witness file) .49 .34 3.9 40 error (invalid witness file) 6.1 3.2 130 300 - -
ldv-memsafety/memleaks_test17_2_false-valid-free.i false(valid-free) 1 wit inspect 71    71    660   2100 2.0  0   error (invalid witness file) .55 .34 14   41 error (invalid witness file) 6.2 3.3 120 300 - -
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) 1 wit inspect .30 .30 3.1 26 2.0  0   error (invalid witness file) .48 .31 9.6 40 error (invalid witness file) 6.3 3.4 120 300 - -
ldv-memsafety/memleaks_test2_false-valid-free.i false(valid-free) 1 wit inspect .21 .21 2.5 26 2.0  0   error (invalid witness file) .49 .32 8.4 39 error (invalid witness file) 6.1 3.2 140 290 - -
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) 1 wit inspect .21 .20 1.9 26 2.0  0   error (invalid witness file) .49 .32 8.6 40 error (invalid witness file) 6.0 3.2 130 300 - -
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) 1 wit inspect .22 .21 2.7 26 2.0  0   error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.2 3.3 120 300 - -
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) 1 wit inspect .20 .20 2.9 26 2.0  0   error (invalid witness file) .49 .32 7.5 40 error (invalid witness file) 6.5 3.4 130 300 - -
ldv-memsafety/memleaks_test10_false-valid-memtrack.i false(valid-deref) -16 wit inspect .56 .55 6.8 26 2.0  0   error (invalid witness file) .51 .34 6.4 39 error (invalid witness file) 5.7 3.0 110 290 - -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack.i false(valid-deref) -16 wit inspect .61 .61 8.1 26 1.7  0   error (invalid witness file) .51 .33 7.5 39 error (invalid witness file) 6.5 3.4 120 290 - -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .80 .80 2.9 26 2.0  0   error (invalid witness file) .47 .31 7.1 39 error (invalid witness file) 6.5 3.4 130 300 - -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i out of memory 0 wit inspect 490    490    4900   15000 2.0  0   error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.9 3.6 130 320 - -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .23 .23 2.4 26 1.7  0   error (invalid witness file) .48 .32 7.5 40 error (invalid witness file) 5.6 3.0 110 290 - -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i out of memory 0 wit inspect 580    580    6200   15000 2.0  0   error (invalid witness file) .50 .32 6.7 39 error (invalid witness file) 6.2 3.3 130 290 - -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-deref) -16 wit inspect .91 .91 12   32 2.0  0   error (invalid witness file) .49 .33 3.6 40 error (invalid witness file) 6.3 3.3 130 290 - -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .22 .22 2.4 26 1.7  0   error (invalid witness file) .51 .32 4.9 42 error (invalid witness file) 5.7 3.0 110 300 - -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 2.3 26 2.0  0   error (invalid witness file) .51 .32 10   40 error (invalid witness file) 6.7 3.5 130 300 - -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 41    41    480   2100 2.0  0   error (invalid witness file) .50 .33 10   40 error (invalid witness file) 6.2 3.3 120 310 - -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 66    66    900   2000 2.0  0   error (invalid witness file) .48 .32 7.3 40 error (invalid witness file) 6.2 3.2 120 310 - -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 37    37    380   2000 1.7  0   error (invalid witness file) .49 .31 9.2 40 error (invalid witness file) 6.3 3.4 110 300 - -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 59    59    720   2100 1.7  0   error (invalid witness file) .52 .33 13   42 error (invalid witness file) 6.1 3.2 130 300 - -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.4  1.4  17   37 2.0  0   error (invalid witness file) .49 .32 4.1 39 error (invalid witness file) 5.8 3.1 110 290 - -
ldv-memsafety/memleaks_test1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .20 .20 2.1 26 1.7  0   error (invalid witness file) .53 .35 7.8 40 error (invalid witness file) 6.0 3.2 130 300 - -
ldv-memsafety/memleaks_test20_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 2.2 26 1.7  0   error (invalid witness file) .48 .30 8.4 39 error (invalid witness file) 6.0 3.2 130 290 - -
ldv-memsafety/memleaks_test21_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .22 .21 2.6 26 2.0  0   error (invalid witness file) .46 .30 7.2 39 error (invalid witness file) 6.1 3.2 130 290 - -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .36 .36 4.1 26 1.7  0   error (invalid witness file) .47 .31 7.2 40 error (invalid witness file) 5.8 3.1 110 290 - -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .26 .25 2.8 26 1.7  0   error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.0 3.2 110 300 - -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.4  1.4  3.3 26 2.0  0   error (invalid witness file) .56 .36 4.6 40 error (invalid witness file) 6.1 3.2 130 300 - -
ldv-memsafety/memleaks_test4_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .23 .23 2.7 26 1.9  0   error (invalid witness file) .47 .30 3.8 40 error (invalid witness file) 6.4 3.4 130 310 - -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 2.7 26 2.0  0   error (invalid witness file) .50 .34 4.6 40 error (invalid witness file) 6.3 3.3 130 290 - -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 2.1 26 1.7  0   error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.0 3.2 120 300 - -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .22 .22 2.5 26 2.0  0   error (invalid witness file) .51 .32 4.5 41 error (invalid witness file) 6.3 3.3 130 300 - -
ldv-memsafety/memleaks_test6_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .23 .23 2.3 26 2.0  0   error (invalid witness file) .48 .32 5.1 41 error (invalid witness file) 6.1 3.3 120 310 - -
ldv-memsafety/memleaks_test7_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 2.2 26 2.0  0   error (invalid witness file) .50 .34 9.3 40 error (invalid witness file) 6.3 3.3 120 300 - -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 2.1 26 2.0  0   error (invalid witness file) .54 .36 9.9 40 error (invalid witness file) 6.2 3.3 120 300 - -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .20 .20 2.4 26 2.0  0   error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.2 3.3 120 320 - -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 2.3 26 2.0  0   error (invalid witness file) .50 .32 9.6 40 error (invalid witness file) 6.2 3.3 120 300 - -
ldv-memsafety/memleaks_test10_true-valid-memsafety.i false(valid-deref) -16 wit inspect .56 .56 7.6 26 2.0  0   - - error (invalid witness file) .50 .31 8.1 39 error (invalid witness file) 6.4 3.4 130 300
ldv-memsafety/memleaks_test11_true-valid-memsafety.i false(valid-deref) -16 wit inspect .75 .75 11   28 2.0  0   - - error (invalid witness file) .47 .32 9.0 39 error (invalid witness file) 6.6 3.5 110 310
ldv-memsafety/memleaks_test12_true-valid-memsafety.i unknown 0 wit inspect 240    240    2600   10000 2.0  0   - - error (invalid witness file) .55 .36 12   43 error (invalid witness file) 6.3 3.3 120 300
ldv-memsafety/memleaks_test13_true-valid-memsafety.i out of memory 0 wit inspect 450    450    4400   15000 2.0  0   - - error (invalid witness file) .50 .32 7.2 40 error (invalid witness file) 6.1 3.2 110 300
ldv-memsafety/memleaks_test14_true-valid-memsafety.i out of memory 0 wit inspect 530    530    5400   15000 2.0  0   - - error (invalid witness file) .51 .33 10   42 error (invalid witness file) 6.1 3.3 120 290
ldv-memsafety/memleaks_test15_true-valid-memsafety.i false(valid-deref) -16 wit inspect 1.1  1.1  13   31 1.7  0   - - error (invalid witness file) .50 .32 13   40 error (invalid witness file) 6.3 3.3 130 300
ldv-memsafety/memleaks_test16_true-valid-memsafety.i true 2 wit inspect .22 .21 2.1 26 2.0  0   - - error (invalid witness file) .50 .31 11   40 error (invalid witness file) 5.9 3.1 120 290
ldv-memsafety/memleaks_test17_1_true-valid-memsafety.i false(valid-free) -16 wit inspect 82    82    990   2100 2.0  0   - - error (invalid witness file) .49 .31 8.9 39 error (invalid witness file) 6.1 3.3 120 300
ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i timeout 0 wit inspect 900    900    2000   12000 .99 0   - - error (invalid witness file) .51 .35 6.3 40 error (invalid witness file) 6.1 3.3 120 290
ldv-memsafety/memleaks_test18_true-valid-memsafety.i true 2 wit inspect 170    170    1700   2200 2.0  0   - - error (invalid witness file) .51 .35 7.0 39 error (invalid witness file) 5.7 3.0 120 290
ldv-memsafety/memleaks_test19_true-valid-memsafety.i true 2 wit inspect .26 .26 2.6 26 1.7  0   - - error (invalid witness file) .51 .32 10   39 error (invalid witness file) 6.3 3.3 110 310
ldv-memsafety/memleaks_test1_true-valid-memsafety.i true 2 wit inspect .19 .18 2.4 26 1.7  0   - - error (invalid witness file) .50 .32 5.1 39 error (invalid witness file) 7.7 4.0 130 320
ldv-memsafety/memleaks_test20_true-valid-memsafety.i true 2 wit inspect .20 .20 2.1 26 2.0  0   - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.1 3.2 140 300
ldv-memsafety/memleaks_test21_true-valid-memsafety.i true 2 wit inspect .19 .19 2.4 26 1.7  0   - - error (invalid witness file) .47 .31 8.9 40 error (invalid witness file) 6.3 3.3 120 290
ldv-memsafety/memleaks_test22_1_true-valid-memsafety.i true 2 wit inspect .34 .34 3.4 26 2.0  0   - - error (invalid witness file) .49 .32 4.9 40 error (invalid witness file) 6.2 3.3 130 300
ldv-memsafety/memleaks_test22_2_true-valid-memsafety.i true 2 wit inspect .35 .35 4.5 26 2.0  0   - - error (invalid witness file) .57 .36 10   44 error (invalid witness file) 6.2 3.3 120 300
ldv-memsafety/memleaks_test22_3_true-valid-memsafety.i true 2 wit inspect .36 .36 4.8 26 1.7  0   - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.4 3.4 130 310
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i timeout 0 wit inspect 900    900    6100   4300 .99 0   - - error (invalid witness file) .52 .35 9.7 41 error (invalid witness file) 5.8 3.1 120 300
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i timeout 0 wit inspect 900    900    8000   4200 .99 0   - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 5.6 3.0 110 290
ldv-memsafety/memleaks_test2_true-valid-memsafety.i true 2 wit inspect .21 .21 2.6 26 2.0  0   - - error (invalid witness file) .50 .33 13   39 error (invalid witness file) 5.9 3.2 110 300
ldv-memsafety/memleaks_test3_true-valid-memsafety.i true 2 wit inspect .20 .20 2.4 26 1.7  0   - - error (invalid witness file) .48 .31 3.9 39 error (invalid witness file) 5.8 3.1 130 290
ldv-memsafety/memleaks_test4_true-valid-memsafety.i true 2 wit inspect .22 .22 2.6 26 1.7  0   - - error (invalid witness file) .51 .32 7.3 40 error (invalid witness file) 6.2 3.3 120 310
ldv-memsafety/memleaks_test5_true-valid-memsafety.i true 2 wit inspect .19 .19 2.2 26 1.8  0   - - error (invalid witness file) .53 .34 12   41 error (invalid witness file) 7.2 3.8 120 320
ldv-memsafety/memleaks_test6_true-valid-memsafety.i true 2 wit inspect .20 .20 2.8 26 2.0  0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.1 3.2 110 300
ldv-memsafety/memleaks_test7_true-valid-memsafety.i true 2 wit inspect .20 .20 2.5 26 2.0  0   - - error (invalid witness file) .47 .31 7.1 41 error (invalid witness file) 6.2 3.3 120 300
ldv-memsafety/memleaks_test8_true-valid-memsafety.i true 2 wit inspect .21 .21 2.2 26 2.0  0   - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 6.6 3.5 130 330
ldv-memsafety/memleaks_test9_true-valid-memsafety.i true 2 wit inspect .18 .18 2.3 26 1.8  0   - - error (invalid witness file) .53 .35 9.9 41 error (invalid witness file) 6.0 3.2 120 310
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i false(valid-deref) -16 wit inspect .16 .16 2.1 23 2.0  0   - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.4 3.4 120 300
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety.i false(valid-deref) -16 wit inspect .18 .18 1.9 23 2.0  0   - - error (invalid witness file) .50 .33 6.2 39 error (invalid witness file) 5.4 3.0 110 290
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety.i false(valid-deref) -16 wit inspect .19 .19 2.1 23 1.7  0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.0 3.2 110 290
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety.i true 2 wit inspect .57 .57 7.4 23 2.0  0   - - error (invalid witness file) .49 .33 12   40 error (invalid witness file) 6.6 3.5 140 310
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety.i false(valid-deref) -16 wit inspect .89 .89 11   24 1.7  0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.1 3.2 120 300
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i false(valid-deref) 1 wit inspect .16 .16 1.9 23 1.7  0   error (invalid witness file) .49 .30 6.5 39 error (invalid witness file) 6.8 3.6 120 310 - -
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i false(valid-deref) 1 wit inspect .73 .73 1.4 24 1.7  0   error (invalid witness file) .47 .30 5.2 40 error (invalid witness file) 5.9 3.2 110 300 - -
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i unknown 0 wit inspect .58 .58 9.0 23 2.0  0   error (invalid witness file) .51 .34 6.6 40 error (invalid witness file) 6.5 3.4 130 310 - -
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i false(valid-deref) 1 wit inspect 3.7  3.7  8.5 24 2.0  0   error (invalid witness file) .53 .33 12   39 error (invalid witness file) 6.7 3.6 140 320 - -
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i false(valid-deref) -16 wit inspect .19 .19 2.0 23 2.0  0   error (invalid witness file) .50 .33 9.6 39 error (invalid witness file) 6.1 3.2 120 310 - -
../../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 -41 38000 38000 350000 740000 290 0   181 45   30   730 3600   181 550 290 11000 27000   181 47   30   900 3700   181 560 300 11000 27000  
    correct results 106 151 3500 3500 37000 47000 200 0   0 31   20   490 2400   0 370 200 7500 18000   0 23   15   460 1800   0 280 150 5400 14000  
        correct true 45 90 1600 1600 15000 21000 85 0   0 0   0   0 0   0 0 0 0 0   0 23   15   460 1800   0 280 150 5400 14000  
        correct false 61 61 1900 1900 23000 26000 110 0   0 31   20   490 2400   0 370 200 7500 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 12 -192 88 88 1100 2400 23 0   0 2.0 1.3 27 160   0 25 13 470 1200   0 4.0 2.6 79 320   0 49 26 940 2400  
        incorrect true 0
        incorrect false 12 -192 88 88 1100 2400 23 0   0 2.0 1.3 27 160   0 25 13 470 1200   0 4.0 2.6 79 320   0 49 26 940 2400  
score (181 tasks, max score: 272) -41
Run set sv-comp17.MemSafety-Heap