Tool SMACK+Corral 1.7.2
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-14 05:56:27 CET [[ 2017-01-15 04:08:20 CET ]] [[ 2017-01-15 04:18:47 CET ]] [[ 2017-01-15 04:12:29 CET ]] [[ 2017-01-15 04:25:58 CET ]]
Run set sv-comp17.MemSafety-Heap
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.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 timeout 0 wit inspect 880   930   8700 440 3.0 0    error (invalid witness file) .49 .32 7.5 41 error (invalid witness file) 6.2 3.3 130 300 - -
memsafety/test-0137_false-valid-deref.i false(valid-deref) 1 wit inspect 2.8 2.7 33 85 1.3 0    error (invalid witness file) .64 .42 6.6 40 error (invalid witness file) 5.7 3.1 120 290 - -
memsafety/test-0235_false-valid-deref.i false(valid-deref) 1 wit inspect 37   36   430 130 1.5 0    error (invalid witness file) .46 .31 6.4 40 error (invalid witness file) 6.1 3.2 110 300 - -
memsafety/960521-1_false-valid-free.i timeout 0 wit inspect 880   930   11000 430 3.0 0    error (invalid witness file) .51 .32 13   39 error (invalid witness file) 6.4 3.4 140 300 - -
memsafety/test-0158_false-valid-free.i false(valid-free) 1 wit inspect 2.7 2.6 32 77 1.5 0    error (invalid witness file) .50 .31 12   39 error (invalid witness file) 5.9 3.1 84 300 - -
memsafety/test-0232_false-valid-free.i false(valid-free) 1 wit inspect 750   750   6600 280 1.6 0    error (invalid witness file) .51 .34 11   40 error (invalid witness file) 5.6 3.1 110 300 - -
memsafety/20020406-1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.9 7.7 97 95 2.1 0    error (invalid witness file) .49 .34 4.1 40 error (invalid witness file) 5.9 3.2 96 290 - -
memsafety/20051113-1.c_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 5.3 5.3 67 86 1.9 0    error (invalid witness file) .50 .32 4.0 40 error (invalid witness file) 6.9 3.7 130 320 - -
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 840   830   8300 210 2.1 0    error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.0 3.2 110 310 - -
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   11000 200 2.1 0    error (invalid witness file) .48 .32 6.8 39 error (invalid witness file) 6.0 3.2 120 290 - -
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 850   840   8800 200 2.1 0    error (invalid witness file) .46 .30 6.1 40 error (invalid witness file) 6.7 3.5 100 290 - -
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.7 3.7 46 78 1.8 0    error (invalid witness file) .53 .34 10   42 error (invalid witness file) 6.2 3.3 120 300 - -
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   7000 320 2.0 0    error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.2 3.3 120 300 - -
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.5 3.6 42 76 1.7 0    error (invalid witness file) .50 .33 4.8 40 error (invalid witness file) 5.7 3.1 110 290 - -
memsafety/test-0220_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   7200 350 1.9 0    error (invalid witness file) .53 .34 12   40 error (invalid witness file) 7.1 3.7 140 320 - -
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   7000 330 1.9 0    error (invalid witness file) .47 .32 7.0 39 error (invalid witness file) 7.9 4.2 81 310 - -
memsafety/test-0234_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   6800 370 2.1 0    error (invalid witness file) .52 .33 14   39 error (invalid witness file) 6.2 3.3 130 300 - -
memsafety/test-0235_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   7300 430 2.2 0    error (invalid witness file) .52 .33 11   39 error (invalid witness file) 5.8 3.1 120 290 - -
memsafety/960521-1_true-valid-memsafety.i timeout 0 wit inspect 900   930   10000 220 1.9 0    - - error (invalid witness file) .48 .32 10   39 error (invalid witness file) 5.9 3.2 120 300
memsafety/lockfree-3.0_true-valid-memsafety.i true 2 wit inspect 880   880   10000 200 2.1 0    - - error (invalid witness file) .51 .31 12   40 error (invalid witness file) 6.4 3.4 140 300
memsafety/test-0019_true-valid-memsafety.i true 2 wit inspect 3.4 3.4 45 70 1.8 0    - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 6.2 3.3 120 300
memsafety/test-0102_true-valid-memsafety.i timeout 0 wit inspect 880   930   9000 340 2.0 0    - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 7.2 3.8 130 320
memsafety/test-0134_true-valid-memsafety.i timeout 0 wit inspect 880   930   6800 360 2.1 0    - - error (invalid witness file) .54 .35 4.0 39 error (invalid witness file) 6.0 3.2 120 300
memsafety/test-0158_true-valid-memsafety.i true 2 wit inspect 3.2 3.2 46 70 1.7 0    - - error (invalid witness file) .52 .33 13   39 error (invalid witness file) 5.6 3.0 120 290
memsafety/test-0214_true-valid-memsafety.i timeout 0 wit inspect 880   930   10000 230 2.1 0    - - error (invalid witness file) .49 .31 10   39 error (invalid witness file) 6.0 3.2 110 290
memsafety/test-0217_true-valid-memsafety.i timeout 0 wit inspect 880   930   7800 280 2.2 0    - - error (invalid witness file) .49 .32 6.8 40 error (invalid witness file) 6.9 3.6 130 320
memsafety/test-0218_true-valid-memsafety.i timeout 0 wit inspect 880   930   7900 280 2.2 0    - - error (invalid witness file) .48 .33 6.9 39 error (invalid witness file) 5.8 3.1 110 300
memsafety/test-0219_true-valid-memsafety.i timeout 0 wit inspect 880   930   7500 360 1.9 0    - - error (invalid witness file) .52 .32 9.9 39 error (invalid witness file) 6.1 3.2 120 300
memsafety/test-0232_true-valid-memsafety.i true 2 wit inspect 880   880   9200 310 1.9 0    - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.2 3.3 130 300
memsafety/test-0234_true-valid-memsafety.i timeout 0 wit inspect 880   930   7400 380 2.1 0    - - error (invalid witness file) .55 .37 8.6 41 error (invalid witness file) 6.3 3.3 110 300
memsafety/test-0235_true-valid-memsafety.i timeout 0 wit inspect 880   930   8900 410 2.2 0    - - error (invalid witness file) .59 .37 8.1 41 error (invalid witness file) 6.2 3.3 120 300
memsafety/test-0236_true-valid-memsafety.i timeout 0 wit inspect 880   930   8400 440 2.1 0    - - error (invalid witness file) .51 .33 10   41 error (invalid witness file) 5.8 3.1 120 290
memsafety/test-0237_true-valid-memsafety.i timeout 0 wit inspect 880   930   8000 390 2.2 0    - - error (invalid witness file) .51 .33 4.7 41 error (invalid witness file) 6.5 3.4 120 320
memsafety/test-0504_true-valid-memsafety.i timeout 0 wit inspect 880   930   7900 380 1.9 0    - - error (invalid witness file) .51 .33 6.1 39 error (invalid witness file) 6.1 3.2 110 290
memsafety/test-0513_true-valid-memsafety.i timeout 0 wit inspect 880   930   8600 440 2.0 0    - - error (invalid witness file) .52 .33 10   41 error (invalid witness file) 6.0 3.2 130 300
memsafety/test-0521_true-valid-memsafety.i timeout 0 wit inspect 880   930   7600 370 2.4 0    - - error (invalid witness file) .53 .36 12   42 error (invalid witness file) 5.6 3.0 110 300
memsafety/test-memleak_nexttime_true-valid-memsafety.i true 2 wit inspect 3.3 3.4 47 69 1.8 0    - - error (invalid witness file) .47 .31 7.8 40 error (invalid witness file) 6.7 3.5 94 300
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i true 2 wit inspect 880   880   10000 230 1.9 0    - - error (invalid witness file) .50 .33 8.1 41 error (invalid witness file) 6.1 3.2 110 300
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i timeout 0 wit inspect 880   930   8400 280 2.0 0    - - error (invalid witness file) .49 .32 6.5 39 error (invalid witness file) 5.8 3.1 120 290
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i timeout 0 wit inspect 880   930   6900 280 2.1 0    - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.0 3.2 130 300
memsafety-ext/tree_cnstr_true-valid-memsafety.i timeout 0 wit inspect 880   930   9000 290 2.0 0    - - error (invalid witness file) .49 .31 9.7 39 error (invalid witness file) 6.0 3.1 110 300
memsafety-ext/tree_dsw_true-valid-memsafety.i timeout 0 wit inspect 880   930   9200 270 2.1 0    - - error (invalid witness file) .54 .35 4.4 40 error (invalid witness file) 6.3 3.3 120 300
memsafety-ext/tree_of_cslls_true-valid-memsafety.i timeout 0 wit inspect 880   930   7200 360 2.2 0    - - error (invalid witness file) .47 .30 3.8 43 error (invalid witness file) 6.3 3.4 120 300
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i timeout 0 wit inspect 880   930   7500 300 2.1 0    - - error (invalid witness file) .50 .32 6.4 40 error (invalid witness file) 6.0 3.2 110 310
memsafety-ext/tree_stack_true-valid-memsafety.i timeout 0 wit inspect 880   930   7300 280 2.0 0    - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 6.2 3.3 120 300
memsafety-ext2/split_list_test05_false-valid-deref.i timeout 0 wit inspect 880   930   8400 430 2.6 0    error (invalid witness file) .51 .34 4.6 40 error (invalid witness file) 6.0 3.2 99 300 - -
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 840   830   6800 450 2.4 0    error (invalid witness file) .49 .34 4.2 41 error (invalid witness file) 6.2 3.3 110 300 - -
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   10000 380 2.2 0    error (invalid witness file) .53 .33 12   39 error (invalid witness file) 5.8 3.1 110 300 - -
memsafety-ext2/length_test03_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   8200 320 2.0 0    error (invalid witness file) .51 .34 6.4 42 error (invalid witness file) 6.0 3.2 120 300 - -
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   7100 410 2.2 0    error (invalid witness file) .53 .33 12   39 error (invalid witness file) 6.1 3.2 120 300 - -
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i timeout 0 wit inspect 880   930   7400 440 2.4 0    - - error (invalid witness file) .48 .31 8.8 40 error (invalid witness file) 5.9 3.1 120 300
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i timeout 0 wit inspect 880   930   10000 440 2.2 0    - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.1 3.2 96 300
memsafety-ext2/length_test03_true-valid-memsafety.i true 2 wit inspect 880   880   8400 320 2.0 0    - - error (invalid witness file) .50 .32 6.1 40 error (invalid witness file) 6.0 3.1 130 300
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i timeout 0 wit inspect 880   930   8400 420 2.2 0    - - error (invalid witness file) .52 .34 6.8 41 error (invalid witness file) 6.1 3.2 120 300
memsafety-ext2/split_list_test05_true-valid-memsafety.i timeout 0 wit inspect 880   930   7600 320 2.6 0    - - error (invalid witness file) .51 .32 13   40 error (invalid witness file) 6.2 3.3 130 310
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 1 wit inspect 2.5 2.5 31 83 1.3 0    error (invalid witness file) .50 .31 7.0 40 error (invalid witness file) 6.4 3.3 120 300 - -
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 880   930   7500 290 2.0 0    error (invalid witness file) .54 .35 12   39 error (invalid witness file) 6.8 3.6 110 300 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 2.3 2.3 27 91 1.3 0    error (invalid witness file) .52 .36 3.8 39 error (invalid witness file) 5.9 3.1 120 300 - -
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) 1 wit inspect 640   640   7000 330 1.6 0    error (invalid witness file) .50 .33 7.0 40 error (invalid witness file) 6.5 3.5 140 300 - -
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) 1 wit inspect 2.8 2.8 37 73 1.5 0    error (invalid witness file) .49 .32 7.2 39 error (invalid witness file) 7.5 4.0 85 300 - -
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.9 3.9 49 84 1.8 0    error (invalid witness file) .49 .32 6.3 39 error (invalid witness file) 6.3 3.4 140 300 - -
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.7 3.8 46 80 1.8 0    error (invalid witness file) .50 .32 7.9 39 error (invalid witness file) 5.8 3.0 100 290 - -
list-ext-properties/test-0232_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   8000 350 1.9 0    error (invalid witness file) .48 .31 10   40 error (invalid witness file) 7.5 3.9 140 320 - -
list-ext-properties/960521-1_1_true-valid-memsafety.i true 2 wit inspect 830   820   9500 320 2.0 0    - - error (invalid witness file) .47 .32 7.8 39 error (invalid witness file) 6.2 3.3 120 300
list-ext-properties/list-ext_1_true-valid-memsafety.i true 2 wit inspect 880   880   8100 350 2.0 0    - - error (invalid witness file) .49 .32 7.1 40 error (invalid witness file) 6.2 3.3 110 300
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 2 wit inspect 880   880   8400 240 2.0 0    - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.1 3.3 130 300
list-ext-properties/simple-ext_1_true-valid-memsafety.i true 2 wit inspect 880   880   11000 290 1.9 0    - - error (invalid witness file) .49 .33 6.8 39 error (invalid witness file) 6.1 3.2 100 300
list-ext-properties/test-0019_1_true-valid-memsafety.i true 2 wit inspect 3.6 3.5 41 74 1.8 0    - - error (invalid witness file) .52 .34 3.6 39 error (invalid witness file) 6.1 3.2 120 300
list-ext-properties/test-0158_1_true-valid-memsafety.i true 2 wit inspect 3.3 3.4 41 66 1.8 0    - - error (invalid witness file) .52 .34 4.0 40 error (invalid witness file) 6.1 3.3 110 310
list-ext-properties/test-0214_1_true-valid-memsafety.i timeout 0 wit inspect 880   930   6900 270 2.2 0    - - error (invalid witness file) .52 .34 3.6 40 error (invalid witness file) 5.4 3.0 94 290
list-ext-properties/test-0217_1_true-valid-memsafety.i timeout 0 wit inspect 880   930   8700 360 2.2 0    - - error (invalid witness file) .50 .32 10   40 error (invalid witness file) 6.1 3.2 120 300
list-ext-properties/test-0232_1_true-valid-memsafety.i true 2 wit inspect 880   880   8100 340 1.9 0    - - error (invalid witness file) .48 .32 7.2 40 error (invalid witness file) 6.3 3.3 130 300
list-ext-properties/test-0504_1_true-valid-memsafety.i timeout 0 wit inspect 880   930   7300 380 2.0 0    - - error (invalid witness file) .50 .34 3.5 40 error (invalid witness file) 7.1 3.7 98 330
list-ext-properties/test-0513_1_true-valid-memsafety.i true 2 wit inspect 370   370   3100 310 2.1 0    - - error (invalid witness file) .55 .34 13   43 error (invalid witness file) 6.2 3.3 130 290
memory-alloca/c.03-alloca_true-valid-memsafety.i true 2 wit inspect 4.1 4.1 47 81 1.9 0    - - error (invalid witness file) .51 .32 9.9 40 error (invalid witness file) 5.9 3.1 120 300
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 1 wit inspect 3.9 3.8 50 83 1.2 0    error (invalid witness file) .56 .36 12   40 error (invalid witness file) 5.9 3.2 110 300 - -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 3.5 3.3 45 84 1.2 0    error (invalid witness file) .51 .34 7.1 40 error (invalid witness file) 5.7 3.1 95 300 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) 1 wit inspect 3.2 3.1 39 82 1.2 0    error (invalid witness file) .50 .32 8.5 40 error (invalid witness file) 6.0 3.2 120 300 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.1 3.9 63 95 2.0 0    error (invalid witness file) .54 .35 13   41 error (invalid witness file) 5.9 3.1 110 300 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c timeout 0 wit inspect 750   930   7500 480 2.2 0    error (invalid witness file) .65 .41 5.7 39 error (invalid witness file) 6.1 3.2 100 290 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c timeout 0 wit inspect 750   930   6900 420 2.2 0    error (invalid witness file) .48 .30 6.4 39 error (invalid witness file) 5.5 2.9 110 290 - -
ldv-memsafety/memset2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.7 1.7 23 73 1.1 0    error (invalid witness file) .64 .41 8.1 40 error (invalid witness file) 5.5 2.9 110 290 - -
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.6 1.7 23 73 1.1 0    error (invalid witness file) .50 .32 10   39 error (invalid witness file) 5.8 3.1 130 300 - -
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.6 1.7 21 82 1.1 0    error (invalid witness file) .51 .33 13   41 error (invalid witness file) 5.4 3.0 100 290 - -
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.6 1.7 22 82 1.1 0    error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.5 3.0 95 290 - -
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.6 1.7 21 73 1.1 0    error (invalid witness file) .53 .35 3.9 40 error (invalid witness file) 7.3 3.8 100 310 - -
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.6 1.7 20 76 1.1 0    error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.2 3.3 120 300 - -
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c true 2 wit inspect 760   760   7400 340 1.8 0    - - error (invalid witness file) .49 .31 8.8 39 error (invalid witness file) 6.5 3.4 120 310
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety.c true 2 wit inspect 750   750   6700 560 2.2 0    - - error (invalid witness file) .52 .34 9.4 41 error (invalid witness file) 5.2 2.9 80 300
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c timeout 0 wit inspect 750   930   10000 400 2.2 0    - - error (invalid witness file) .52 .34 13   41 error (invalid witness file) 5.9 3.2 120 300
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety.c true 2 wit inspect 750   750   6500 540 2.2 0    - - error (invalid witness file) .53 .33 11   40 error (invalid witness file) 6.2 3.3 130 300
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 2 wit inspect 760   760   7800 330 3.2 0    - - error (invalid witness file) .52 .34 11   39 error (invalid witness file) 5.5 2.9 110 300
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety.c timeout 0 wit inspect 750   930   8300 460 2.2 0    - - error (invalid witness file) .50 .32 9.8 40 error (invalid witness file) 6.3 3.3 120 300
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true 2 wit inspect 3.1 3.3 38 71 1.8 0    - - error (invalid witness file) .54 .34 12   41 error (invalid witness file) 6.0 3.1 120 300
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true 2 wit inspect 3.2 3.3 41 67 1.8 0    - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 5.9 3.1 120 300
ldv-memsafety/StructInitialization_true-valid-memsafety.c true 2 wit inspect 3.0 3.3 33 70 1.7 0    - - error (invalid witness file) .52 .34 13   39 error (invalid witness file) 6.0 3.2 120 300
ldv-memsafety/memset2_true-valid-memsafety.c true 2 wit inspect 3.1 3.3 34 73 1.7 0    - - error (invalid witness file) .50 .32 9.7 41 error (invalid witness file) 6.2 3.3 110 290
ldv-memsafety/memset3_true-valid-memsafety.c true 2 wit inspect 3.1 3.3 36 69 1.7 0    - - error (invalid witness file) .54 .34 13   41 error (invalid witness file) 5.6 3.0 110 290
ldv-memsafety/memsetNonZero2_true-valid-memsafety.c true 2 wit inspect 3.0 3.2 38 67 1.7 0    - - error (invalid witness file) .51 .34 9.8 39 error (invalid witness file) 6.9 3.6 120 310
ldv-memsafety/memsetNonZero3_true-valid-memsafety.c true 2 wit inspect 3.1 3.3 37 68 1.7 0    - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 5.6 3.0 110 300
ldv-memsafety/memsetNonZero_true-valid-memsafety.c true 2 wit inspect 3.1 3.3 37 71 1.7 0    - - error (invalid witness file) .51 .32 9.3 40 error (invalid witness file) 6.1 3.2 110 290
ldv-memsafety/memset_true-valid-memsafety.c true 2 wit inspect 3.0 3.2 33 71 1.7 0    - - error (invalid witness file) .52 .34 13   41 error (invalid witness file) 6.0 3.2 120 290
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) 1 wit inspect 2.7 2.6 35 93 1.3 0    error (invalid witness file) .50 .33 5.8 39 error (invalid witness file) 6.3 3.4 120 300 - -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 1 wit inspect 2.7 2.7 34 82 1.3 0    error (invalid witness file) .55 .36 14   41 error (invalid witness file) 6.2 3.3 130 300 - -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 1 wit inspect 2.8 2.7 31 83 1.3 0    error (invalid witness file) .51 .33 14   40 error (invalid witness file) 6.3 3.3 130 300 - -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-deref) 1 wit inspect 3.8 3.7 47 93 1.5 0    error (invalid witness file) .52 .35 6.6 41 error (invalid witness file) 6.2 3.3 130 300 - -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(valid-deref) 1 wit inspect 3.4 3.4 43 89 1.5 0    error (invalid witness file) .51 .32 11   39 error (invalid witness file) 5.8 3.1 110 300 - -
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) 1 wit inspect 3.6 3.5 45 82 1.6 .12 error (invalid witness file) .56 .36 8.4 42 error (invalid witness file) 6.2 3.3 110 300 - -
ldv-memsafety/memleaks_test12_false-valid-free.i false(valid-free) 1 wit inspect 20   19   270 110 2.1 0    error (invalid witness file) .52 .34 5.6 39 error (invalid witness file) 6.5 3.4 130 300 - -
ldv-memsafety/memleaks_test17_2_false-valid-free.i false(valid-free) 1 wit inspect 40   39   560 140 1.7 0    error (invalid witness file) .49 .32 9.1 41 error (invalid witness file) 6.1 3.3 110 300 - -
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) 1 wit inspect 3.3 3.3 39 80 1.6 0    error (invalid witness file) .53 .34 14   40 error (invalid witness file) 6.2 3.3 130 300 - -
ldv-memsafety/memleaks_test2_false-valid-free.i false(valid-free) 1 wit inspect 2.6 2.7 40 82 1.5 0    error (invalid witness file) .48 .30 6.4 40 error (invalid witness file) 6.3 3.3 100 300 - -
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) 1 wit inspect 2.6 2.8 34 83 1.5 0    error (invalid witness file) .51 .33 9.1 40 error (invalid witness file) 5.6 3.0 110 280 - -
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) 1 wit inspect 2.9 2.9 36 76 1.6 0    error (invalid witness file) .56 .37 4.5 42 error (invalid witness file) 5.5 3.0 110 290 - -
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) 1 wit inspect 2.9 3.0 38 78 1.5 0    error (invalid witness file) .59 .39 5.1 42 error (invalid witness file) 6.3 3.3 130 310 - -
ldv-memsafety/memleaks_test10_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 4.4 4.5 54 74 1.9 0    error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.0 3.2 110 300 - -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 4.7 4.6 67 85 2.0 0    error (invalid witness file) .51 .33 6.9 40 error (invalid witness file) 6.8 3.6 120 300 - -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.9 4.0 42 81 1.9 0    error (invalid witness file) .48 .31 8.3 39 error (invalid witness file) 6.4 3.4 130 300 - -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 5.3 5.2 62 89 2.0 0    error (invalid witness file) .54 .35 14   41 error (invalid witness file) 5.9 3.1 120 300 - -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.9 4.0 48 82 1.9 0    error (invalid witness file) .53 .35 12   39 error (invalid witness file) 5.8 3.1 120 300 - -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 5.2 5.1 55 87 2.0 0    error (invalid witness file) .48 .32 6.8 40 error (invalid witness file) 6.5 3.4 120 290 - -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 9.3 9.1 110 87 2.1 0    error (invalid witness file) .48 .31 9.7 39 error (invalid witness file) 6.2 3.3 120 300 - -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.6 3.7 43 78 1.8 0    error (invalid witness file) .51 .33 7.9 39 error (invalid witness file) 5.8 3.1 110 290 - -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.6 3.7 47 78 1.8 0    error (invalid witness file) .50 .33 6.6 40 error (invalid witness file) 6.1 3.2 120 300 - -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 95   95   1100 150 2.0 0    error (invalid witness file) .53 .34 14   41 error (invalid witness file) 6.1 3.3 97 300 - -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 45   44   520 130 2.0 0    error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.2 3.3 130 300 - -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 32   32   490 120 2.0 0    error (invalid witness file) .49 .32 6.5 41 error (invalid witness file) 7.8 4.1 160 320 - -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 27   26   350 110 2.0 0    error (invalid witness file) .51 .33 6.7 41 error (invalid witness file) 5.8 3.1 120 300 - -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 5.9 5.8 63 80 1.9 0    error (invalid witness file) .50 .31 8.4 39 error (invalid witness file) 5.7 3.1 110 290 - -
ldv-memsafety/memleaks_test1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.5 3.6 54 80 1.8 0    error (invalid witness file) .63 .41 8.3 40 error (invalid witness file) 6.4 3.4 120 300 - -
ldv-memsafety/memleaks_test20_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.7 3.7 46 78 1.8 0    error (invalid witness file) .50 .32 7.3 40 error (invalid witness file) 6.9 3.6 110 320 - -
ldv-memsafety/memleaks_test21_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.6 3.8 48 80 1.8 0    error (invalid witness file) .48 .31 8.5 40 error (invalid witness file) 5.8 3.1 100 290 - -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 4.7 4.6 60 77 2.0 0    error (invalid witness file) .63 .41 7.9 39 error (invalid witness file) 5.7 3.0 94 290 - -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.9 3.9 48 86 1.9 0    error (invalid witness file) .49 .32 4.0 41 error (invalid witness file) 5.6 3.0 110 290 - -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 4.8 4.8 56 80 2.0 0    error (invalid witness file) .63 .39 12   42 error (invalid witness file) 6.1 3.3 130 300 - -
ldv-memsafety/memleaks_test4_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.6 3.7 45 84 1.8 0    error (invalid witness file) .49 .31 5.8 39 error (invalid witness file) 6.2 3.3 100 300 - -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.5 3.7 47 73 1.8 0    error (invalid witness file) .52 .33 11   39 error (invalid witness file) 6.4 3.4 130 300 - -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.6 3.8 44 78 1.8 0    error (invalid witness file) .51 .33 10   40 error (invalid witness file) 7.2 3.8 92 300 - -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 4.0 4.0 48 86 1.9 0    error (invalid witness file) .53 .34 13   40 error (invalid witness file) 7.2 3.7 120 320 - -
ldv-memsafety/memleaks_test6_3_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.9 3.8 45 80 1.9 0    error (invalid witness file) .49 .31 5.4 40 error (invalid witness file) 6.2 3.3 100 300 - -
ldv-memsafety/memleaks_test7_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.8 3.7 49 78 1.9 0    error (invalid witness file) .52 .35 9.0 40 error (invalid witness file) 6.5 3.4 110 300 - -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.7 3.7 48 73 1.8 0    error (invalid witness file) .57 .37 14   42 error (invalid witness file) 5.9 3.1 84 300 - -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.7 3.8 40 84 1.8 0    error (invalid witness file) .53 .34 12   39 error (invalid witness file) 6.2 3.3 130 310 - -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.6 3.7 43 81 1.8 0    error (invalid witness file) .50 .32 4.0 40 error (invalid witness file) 6.4 3.4 130 300 - -
ldv-memsafety/memleaks_test10_true-valid-memsafety.i true 2 wit inspect 4.3 4.3 49 73 1.9 0    - - error (invalid witness file) .54 .34 13   42 error (invalid witness file) 6.8 3.5 120 300
ldv-memsafety/memleaks_test11_true-valid-memsafety.i true 2 wit inspect 4.2 4.2 54 73 2.0 0    - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.1 3.2 130 300
ldv-memsafety/memleaks_test12_true-valid-memsafety.i true 2 wit inspect 330   330   3300 210 2.5 0    - - error (invalid witness file) .49 .32 8.8 39 error (invalid witness file) 6.5 3.4 140 300
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 2 wit inspect 5.0 5.1 69 91 2.0 0    - - error (invalid witness file) .50 .31 4.1 40 error (invalid witness file) 7.2 3.8 120 320
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 2 wit inspect 4.8 4.8 54 80 2.0 0    - - error (invalid witness file) .49 .32 7.1 40 error (invalid witness file) 5.5 3.0 110 280
ldv-memsafety/memleaks_test15_true-valid-memsafety.i true 2 wit inspect 8.6 8.5 100 87 2.2 0    - - error (invalid witness file) .59 .36 9.7 44 error (invalid witness file) 6.0 3.2 120 290
ldv-memsafety/memleaks_test16_true-valid-memsafety.i true 2 wit inspect 3.2 3.3 42 68 1.9 0    - - error (invalid witness file) .49 .33 8.3 41 error (invalid witness file) 5.6 3.0 120 290
ldv-memsafety/memleaks_test17_1_true-valid-memsafety.i true 2 wit inspect 110   110   1400 150 2.0 0    - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.0 3.2 120 300
ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i true 2 wit inspect 880   880   11000 310 2.0 0    - - error (invalid witness file) .49 .32 4.4 40 error (invalid witness file) 6.4 3.4 130 300
ldv-memsafety/memleaks_test18_true-valid-memsafety.i true 2 wit inspect 43   43   580 110 2.0 0    - - error (invalid witness file) .51 .33 12   42 error (invalid witness file) 6.2 3.3 100 300
ldv-memsafety/memleaks_test19_true-valid-memsafety.i true 2 wit inspect 4.0 4.0 55 70 1.9 0    - - error (invalid witness file) .47 .32 3.8 39 error (invalid witness file) 6.1 3.2 120 300
ldv-memsafety/memleaks_test1_true-valid-memsafety.i true 2 wit inspect 3.2 3.2 36 70 1.8 0    - - error (invalid witness file) .49 .33 5.8 41 error (invalid witness file) 6.3 3.3 120 300
ldv-memsafety/memleaks_test20_true-valid-memsafety.i true 2 wit inspect 3.4 3.4 47 72 1.9 0    - - error (invalid witness file) .49 .31 5.5 39 error (invalid witness file) 6.4 3.4 130 300
ldv-memsafety/memleaks_test21_true-valid-memsafety.i true 2 wit inspect 3.2 3.3 37 68 1.9 0    - - error (invalid witness file) .48 .31 8.4 40 error (invalid witness file) 5.9 3.2 130 300
ldv-memsafety/memleaks_test22_1_true-valid-memsafety.i true 2 wit inspect 4.2 4.2 55 73 2.0 0    - - error (invalid witness file) .52 .34 8.2 42 error (invalid witness file) 6.8 3.5 110 310
ldv-memsafety/memleaks_test22_2_true-valid-memsafety.i true 2 wit inspect 5.0 5.0 62 76 2.0 0    - - error (invalid witness file) .54 .34 11   41 error (invalid witness file) 6.2 3.3 120 310
ldv-memsafety/memleaks_test22_3_true-valid-memsafety.i true 2 wit inspect 5.2 5.1 58 78 2.0 0    - - error (invalid witness file) .49 .33 13   40 error (invalid witness file) 6.1 3.2 120 300
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i true 2 wit inspect 880   880   8400 330 2.3 0    - - error (invalid witness file) .53 .34 8.9 40 error (invalid witness file) 5.7 3.1 110 290
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i timeout 0 wit inspect 880   930   7100 290 2.3 0    - - error (invalid witness file) .51 .33 13   39 error (invalid witness file) 5.9 3.2 110 300
ldv-memsafety/memleaks_test2_true-valid-memsafety.i true 2 wit inspect 3.2 3.3 44 73 1.8 0    - - error (invalid witness file) .53 .33 9.0 42 error (invalid witness file) 6.4 3.4 120 310
ldv-memsafety/memleaks_test3_true-valid-memsafety.i true 2 wit inspect 3.2 3.3 44 69 1.8 0    - - error (invalid witness file) .49 .30 7.9 39 error (invalid witness file) 6.2 3.3 130 300
ldv-memsafety/memleaks_test4_true-valid-memsafety.i true 2 wit inspect 3.2 3.2 49 70 1.8 0    - - error (invalid witness file) .52 .34 11   41 error (invalid witness file) 5.9 3.2 110 300
ldv-memsafety/memleaks_test5_true-valid-memsafety.i true 2 wit inspect 3.2 3.3 42 69 1.8 0    - - error (invalid witness file) .54 .35 11   43 error (invalid witness file) 5.8 3.1 120 300
ldv-memsafety/memleaks_test6_true-valid-memsafety.i true 2 wit inspect 3.5 3.6 41 73 1.9 0    - - error (invalid witness file) .51 .32 9.0 41 error (invalid witness file) 6.5 3.4 120 310
ldv-memsafety/memleaks_test7_true-valid-memsafety.i true 2 wit inspect 3.5 3.6 42 75 1.9 0    - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.2 3.3 110 300
ldv-memsafety/memleaks_test8_true-valid-memsafety.i true 2 wit inspect 3.3 3.4 40 70 1.8 0    - - error (invalid witness file) .50 .33 10   40 error (invalid witness file) 6.0 3.2 120 300
ldv-memsafety/memleaks_test9_true-valid-memsafety.i true 2 wit inspect 3.4 3.4 41 70 1.9 0    - - error (invalid witness file) .55 .35 14   41 error (invalid witness file) 6.3 3.3 120 300
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i true 2 wit inspect 3.5 3.5 40 75 1.8 0    - - error (invalid witness file) .47 .32 5.1 40 error (invalid witness file) 5.9 3.1 120 300
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety.i true 2 wit inspect 3.7 3.7 52 75 1.9 0    - - error (invalid witness file) .48 .31 8.1 39 error (invalid witness file) 6.2 3.3 120 300
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety.i true 2 wit inspect 3.9 4.0 54 69 1.9 0    - - error (invalid witness file) .59 .36 14   43 error (invalid witness file) 6.0 3.2 100 290
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety.i true 2 wit inspect 3.8 3.7 50 73 1.9 0    - - error (invalid witness file) .49 .31 5.5 41 error (invalid witness file) 6.1 3.3 120 300
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety.i true 2 wit inspect 4.3 4.4 54 72 1.9 0    - - error (invalid witness file) .50 .34 3.5 40 error (invalid witness file) 6.2 3.3 120 300
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.9 26 77 1.2 0    error (invalid witness file) .51 .34 6.5 39 error (invalid witness file) 5.3 2.9 93 290 - -
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.8 25 78 1.2 0    error (invalid witness file) .50 .31 9.6 39 error (invalid witness file) 6.3 3.3 130 300 - -
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i false(valid-deref) 1 wit inspect 1.7 1.7 22 70 1.2 0    error (invalid witness file) .48 .33 4.1 39 error (invalid witness file) 6.0 3.2 110 290 - -
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i false(valid-deref) 1 wit inspect 1.8 1.7 23 70 1.3 0    error (invalid witness file) .48 .30 3.6 39 error (invalid witness file) 6.3 3.3 120 310 - -
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i false(valid-free) 1 wit inspect 3.3 3.3 43 81 1.5 0    error (invalid witness file) .47 .29 6.0 39 error (invalid witness file) 5.8 3.1 120 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 204 59000 61000 570000 33000 340 .12 181 46 30 770 3600   181 560 300 10000 27000   181 46 30 830 3700   181 560 300 11000 27000  
    correct results 144 204 26000 26000 260000 20000 260 .12 0 43 28 720 3400   0 520 280 9600 25000   0 31 20 560 2400   0 370 200 7100 18000  
        correct true 60 120 14000 14000 140000 8800 120 0    0 0 0 0 0   0 0 0 0 0   0 31 20 560 2400   0 370 200 7100 18000  
        correct false 84 84 13000 13000 120000 11000 140 .12 0 43 28 720 3400   0 520 280 9600 25000   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) 204
Run set sv-comp17.MemSafety-Heap