Tool DepthK 3.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-memsafety.MemSafety-Heap cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
memsafety/960521-1_false-valid-deref.i 0 74    73    63 970   3000    .037  0 .62 .37 40 0   0   0 .021 .023 5.7 0    0   0 .96 .62 48 0     0    0 .0042 .0049 .40 0     0      -
memsafety/test-0137_false-valid-deref.i 1 .20 .20 34 2.2 1.0  0      1 6.0  3.3  250 0   0   0 12     6.7   290   .71 0   0 92    75    2200 0     0    1 .67   .67   20    .11  .025  -
memsafety/test-0235_false-valid-deref.i 1 .64 .63 42 10   1.0  0      1 19    10    910 0   0   -32 11     5.9   320   .62 0   0 92    76    2200 0     0    1 .70   .70   21    .11  0      -
memsafety/960521-1_false-valid-free.i 0 74    73    62 1000   3000    .037  0 .69 .42 40 0   0   0 .021 .022 5.8 0    0   0 .93 .60 48 0     0    0 .0024 .0030 .40 0     0      -
memsafety/test-0158_false-valid-free.i -16 .21 .21 34 2.7 1.0  0      -32 5.2  2.8  250 0   0   1 9.1   5.0   320   .62 0   0 3.9  2.3  250 0     0    1 .68   .68   20    .070 .78   -
memsafety/test-0232_false-valid-free.i -16 .63 .62 36 7.2 31    0      1 5.0  2.7  250 0   0   0 97     87     1300   1.5  0   0 96    84    1900 0     0    -32 .67   .67   20    .082 0      -
memsafety/20020406-1_false-valid-memtrack.i 0 5.6  5.6  66 84   31    0      0 5.2  2.8  260 0   0   -32 11     6.3   370   .66 0   0 4.9  2.7  280 0     0    -32 .71   .70   21    .12  0      -
memsafety/20051113-1.c_false-valid-memtrack.i 0 1.4  1.3  36 21   92    0      -32 5.0  2.7  250 0   0   -32 8.8   4.9   310   .62 0   0 4.3  2.4  250 0     0    -32 .66   .69   21    .082 0      -
memsafety/lockfree-3.1_false-valid-memtrack.i 0 4.8  4.7  44 61   180    .0041 0 96    72    2200 0   0   -32 8.5   4.6   310   .66 0   0 92    71    2200 0     0    -32 .66   .67   20    .086 0      -
memsafety/lockfree-3.2_false-valid-memtrack.i 0 .50 .50 35 6.2 31    0      0 98    72    2400 0   0   -32 8.4   4.7   310   .66 0   0 92    71    2400 0     0    -32 .68   .68   20    .090 .29   -
memsafety/lockfree-3.3_false-valid-memtrack.i 0 18    18    68 220   300    .0041 0 98    72    2200 0   0   -32 8.8   4.9   310   .66 0   0 92    69    2200 0     0    -32 .66   .66   20    .090 0      -
memsafety/test-0019_false-valid-memtrack_true-termination.i 0 .16 .16 34 1.9 1.0  0      0 2.9  1.6  200 0   0   -32 7.6   4.3   310   .66 0   0 3.1  1.8  200 0     0    -32 .64   .64   20    .074 .13   -
memsafety/test-0102_false-valid-memtrack.i 0 4.1  4.0  63 56   31    0      0 98    63    3100 0   0   0 12     7.1   290   .75 0   0 92    76    2200 0     0    -16 .67   .67   20    .098 0      -
memsafety/test-0158_false-valid-memtrack_true-termination.i 0 .15 .14 34 1.6 1.0  0      -32 4.2  2.3  250 0   0   -32 8.2   4.6   310   .62 0   0 4.4  2.5  250 0     0    -32 .64   .64   20    .066 0      -
memsafety/test-0220_false-valid-memtrack.i 0 20    20    120 240   31    0      0 97    62    2900 0   0   -32 8.6   5.1   320   .66 0   0 92    75    2300 0     0    -16 .67   .66   20    .090 0      -
memsafety/test-0232_false-valid-memtrack.i 0 .17 .16 34 1.8 .85 0      0 94    81    1600 0   0   -32 8.9   5.3   310   .66 0   0 97    87    1700 .91  0    -32 .65   .67   20    .082 .13   -
memsafety/test-0234_false-valid-memtrack.i 0 .49 .48 41 6.1 1.0  0      0 97    71    2300 0   0   -32 10     5.6   330   .66 0   0 92    77    2200 0     0    -16 .69   .69   21    .11  1.1    -
memsafety/test-0235_false-valid-memtrack.i 0 .53 .53 41 5.7 .85 0      0 97    73    2300 0   0   -32 9.8   5.8   320   .62 0   0 92    76    2200 0     0    -16 .70   .69   21    .11  0      -
memsafety/960521-1_true-valid-memsafety.i 0 72    72    64 1100   3000    .041  - - - - 0 .021 .022 5.6 0    0  
memsafety/lockfree-3.0_true-valid-memsafety.i 0 900    900    390 11000   730    .0041 - - - - 0 .021 .022 5.6 0    0  
memsafety/test-0019_true-valid-memsafety_true-termination.i 2 .42 .42 35 5.2 31    0      - - - - 2 21     14     640   .66 0  
memsafety/test-0102_true-valid-memsafety.i 0 900    900    770 9200   92    0      - - - - 0 .020 .021 5.6 0    0  
memsafety/test-0134_true-valid-memsafety.i 0 900    900    1300 9200   180    0      - - - - 0 .022 .024 5.7 0    0  
memsafety/test-0158_true-valid-memsafety_true-termination.i 2 .49 .48 35 6.0 31    0      - - - - 2 11     6.0   340   .66 0  
memsafety/test-0214_true-valid-memsafety_false-termination.i 0 900    900    6100 7300   130    0      - - - - 0 .021 .022 5.6 0    0  
memsafety/test-0217_true-valid-memsafety_false-termination.i 0 310    310    15000 3100   81    0      - - - - 0 .027 .028 5.6 0    0  
memsafety/test-0218_true-valid-memsafety_false-termination.i 0 260    260    15000 3300   92    0      - - - - 0 .028 .028 5.6 0    0  
memsafety/test-0219_true-valid-memsafety.i 0 900    900    1600 10000   72    0      - - - - 0 .020 .023 5.6 0    0  
memsafety/test-0232_true-valid-memsafety.i 0 900    900    300 11000   810    0      - - - - 0 .022 .024 5.6 0    0  
memsafety/test-0234_true-valid-memsafety.i 0 900    900    10000 7900   11    0      - - - - 0 .021 .022 5.6 0    0  
memsafety/test-0235_true-valid-memsafety.i 0 900    900    11000 5700   11    0      - - - - 0 .022 .023 5.6 0    0  
memsafety/test-0236_true-valid-memsafety.i 0 900    900    15000 10000   21    0      - - - - 0 .020 .021 5.6 0    0  
memsafety/test-0237_true-valid-memsafety.i 0 800    800    15000 8800   39    0      - - - - 0 .021 .022 5.6 0    0  
memsafety/test-0504_true-valid-memsafety.i 0 900    900    570 14000   150    0      - - - - 0 .024 .025 5.6 0    0  
memsafety/test-0513_true-valid-memsafety.i 0 890    900    670 11000   230    0      - - - - 0 .021 .023 5.6 0    0  
memsafety/test-0521_true-valid-memsafety.i 0 890    900    1000 9600   150    0      - - - - 0 .022 .022 5.6 0    0  
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i 2 1.8  1.8  39 24   120    0      - - - - 0 960     880     900   .63 0  
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i 0 900    900    240 13000   370    .0041 - - - - 0 .021 .022 5.7 0    0  
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i 0 900    900    160 13000   240    0      - - - - 0 .023 .023 5.6 0    0  
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i 0 900    900    190 12000   210    0      - - - - 0 .020 .021 5.6 0    0  
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i 0 900    900    660 10000   180    0      - - - - 0 .022 .023 5.6 0    0  
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i 0 900    900    500 9900   270    0      - - - - 0 .022 .022 5.6 0    0  
memsafety-ext/tree_of_cslls_true-valid-memsafety.i 0 900    900    650 10000   120    0      - - - - 0 .026 .026 5.5 0    0  
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i 0 900    900    400 11000   240    0      - - - - 0 .022 .022 5.6 0    0  
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i 0 900    900    430 11000   240    0      - - - - 0 .021 .023 5.7 0    0  
memsafety-ext2/split_list_test05_false-valid-deref.i 0 160    160    15000 1900   1.0  0      0 .62 .39 41 0   0   0 .023 .024 5.6 0    0   0 .91 .59 47 0     0    0 .0019 .0025 .65 0     0      -
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i 0 900    900    1500 12000   290    0      0 .61 .37 42 0   0   0 .024 .025 5.6 0    0   0 .98 .65 48 0     0    0 .0025 .0037 .53 0     0      -
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i 0 900    900    2200 10000   72    0      0 .59 .37 41 0   0   0 .023 .024 5.6 0    0   0 .95 .62 48 0     0    0 .0015 .0021 .53 0     0      -
memsafety-ext2/length_test03_false-valid-memtrack.i 0 12    12    56 130   180    0      0 96    72    2400 0   0   -32 8.8   5.1   320   .62 0   0 97    87    1500 .56  0    -16 .71   .71   21    .098 0      -
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i 0 900    900    360 10000   240    0      0 .66 .41 41 0   0   0 .023 .024 5.6 0    0   0 .96 .63 48 0     0    0 .0057 .0076 .53 0     0      -
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i 0 900    900    1300 9200   330    0      - - - - 0 .038 .040 5.5 0    0  
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i 0 900    900    1800 10000   72    0      - - - - 0 .021 .022 5.6 0    0  
memsafety-ext2/length_test03_true-valid-memsafety.i 0 900    900    370 13000   950    0      - - - - 0 .022 .025 5.6 0    0  
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i 0 890    900    450 12000   240    0      - - - - 0 .021 .022 5.7 0    0  
memsafety-ext2/split_list_test05_true-valid-memsafety.i 0 150    150    15000 1700   .86 0      - - - - 0 .020 .020 5.6 0    0  
list-ext-properties/960521-1_1_false-valid-deref.i 1 .58 .57 36 8.3 31    0      -32 20    10    1100 0   0   -32 9.1   5.1   320   .62 0   0 15    130    790 .016 0    1 .65   .67   20    .078 0      -
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 .82 .81 36 10   26    0      1 16    8.9  690 0   0   -32 8.9   5.0   320   .66 0   0 6.4  3.7  280 0     0    1 .66   .66   20    .082 0      -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 1 .58 .57 35 8.9 31    0      1 5.2  2.8  270 0   0   -16 9.9   5.6   330   .62 0   0 92    68    2700 0     0    1 .67   .67   20    .082 .025  -
list-ext-properties/960521-1_1_false-valid-free.i 0 .59 .58 35 7.5 31    0      -32 20    11    1100 0   0   -32 10     6.0   320   .62 0   0 16    8.2  1100 0     0    1 .65   .65   20    .078 .041  -
list-ext-properties/test-0158_1_false-valid-free.i -16 .19 .19 34 2.8 .85 0      -32 5.5  3.0  250 0   0   1 9.5   5.8   320   .66 0   0 4.1  2.3  250 0     0    1 .65   .65   20    .074 .025  -
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i 0 .16 .16 34 1.8 1.0  0      0 3.6  2.0  200 0   0   -32 8.4   4.9   300   .62 0   0 3.3  1.9  200 0     0    -32 .64   .64   20    .074 0      -
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i 0 .15 .15 34 1.6 1.0  0      -32 4.8  2.7  250 0   0   -32 8.1   5.0   300   .62 0   0 4.0  2.3  250 0     0    -32 .67   .67   20    .074 0      -
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i 0 .16 .16 34 1.9 .85 0      -32 9.1  4.8  410 0   0   -32 9.0   5.0   310   .66 0   0 7.8  4.2  420 0     0    -32 .65   .65   20    .082 0      -
list-ext-properties/960521-1_1_true-valid-memsafety.i 2 30    30    51 460   910    .0082 - - - - 0 960     950     810   .63 0  
list-ext-properties/list-ext_1_true-valid-memsafety.i 2 400    400    220 5400   570    0      - - - - 0 960     850     2300   .68 0  
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i 2 130    130    95 1800   610    .0041 - - - - 0 960     850     2200   .68 0  
list-ext-properties/simple-ext_1_true-valid-memsafety.i 2 520    520    160 6100   950    .0041 - - - - 0 960     890     2300   .70 0  
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i 2 .44 .43 35 5.4 31    0      - - - - 2 40     27     720   .62 0  
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i 2 .53 .53 35 6.7 31    0      - - - - 2 11     6.1   350   .62 0  
list-ext-properties/test-0214_1_true-valid-memsafety.i 0 210    210    310 2700   1000    0      - - - - 0 .023 .025 5.7 0    0  
list-ext-properties/test-0217_1_true-valid-memsafety.i 0 190    190    240 2700   1000    0      - - - - 0 .022 .023 5.6 0    0  
list-ext-properties/test-0232_1_true-valid-memsafety_true-termination.i 2 250    250    230 3100   580    0      - - - - 0 960     930     1200   .63 0  
list-ext-properties/test-0504_1_true-valid-memsafety.i 0 900    900    2200 8200   140    0      - - - - 0 960     910     990   .63 0  
list-ext-properties/test-0513_1_true-valid-memsafety.i 2 93    93    1800 1400   150    0      - - - - 0 960     870     2100   .70 0  
memory-alloca/c.03-alloca_true-valid-memsafety.i 0 280    280    70 4000   3000    .012  - - - - 0 .021 .023 5.6 0    0  
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c 1 .18 .18 33 2.0 .85 0      1 4.4  2.5  250 0   0   -32 10     5.8   340   .62 0   1 3.7  2.3  240 0     .14 0 96      96      20    .086 0      -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c 0 .15 .14 33 1.6 .85 0      1 3.4  1.9  240 0   0   1 7.4   4.6   310   .62 0   1 3.8  2.2  250 0     0    0 96      96      20    .074 .012  -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c 0 .15 .15 33 2.5 1.0  0      1 3.4  1.9  240 0   0   1 7.9   4.9   300   .66 0   1 3.5  2.1  240 0     0    -32 .59   .59   20    .061 .0041 -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c 0 .14 .14 33 1.6 1.0  0      1 3.9  2.1  250 0   0   1 7.4   4.7   310   .56 0   1 4.8  2.8  250 0     0    -32 .62   .62   20    .061 0      -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c 1 87    87    220 1000   980    0      1 13    7.0  440 0   0   -32 11     6.8   400   .62 0   1 11    5.9  420 0     3.9  1 .59   .59   20    .061 0      -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c 0 92    91    220 1100   980    0      1 12    6.1  580 0   0   -32 11     6.6   380   .62 0   1 10    5.4  480 0     0    1 .63   .63   20    .061 0      -
ldv-memsafety/memset2_false-valid-deref-write.c 1 11    11    37 140   1200    .020  -32 3.4  1.9  240 0   0   -32 6.9   4.3   300   .62 0   0 3.3  1.9  240 0     0    1 .59   .59   20    .049 1.8    -
ldv-memsafety/memset3_false-valid-deref-write.c 1 46    46    40 660   2400    .045  -32 3.4  1.9  240 0   0   -32 6.8   4.3   300   .62 0   0 3.3  1.9  250 0     0    1 .62   .62   20    .049 0      -
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c 1 11    11    38 160   1200    .025  -32 4.0  2.3  240 0   0   -32 6.9   3.8   300   .62 0   0 3.6  2.0  250 0     0    1 .59   .60   20    .049 2.9    -
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c 1 46    46    40 670   2400    .041  -32 4.1  2.3  240 0   0   -32 6.9   4.2   300   .62 0   0 3.4  1.9  240 0     0    1 .62   .64   20    .049 0      -
ldv-memsafety/memsetNonZero_false-valid-deref-write.c 1 46    46    40 660   2400    .045  -32 4.4  2.4  250 0   0   -32 6.8   4.3   310   .66 0   0 3.5  2.0  250 0     0    1 .60   .60   20    .049 0      -
ldv-memsafety/memset_false-valid-deref-write.c 1 46    46    40 670   2100    .041  -32 3.3  1.9  240 0   0   -32 7.2   4.3   300   .66 0   0 3.5  2.0  250 0     0    1 .61   .60   20    .049 0      -
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c 0 900    900    970 9600   450    .0041 - - - - 0 .020 .020 5.6 0    0  
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c 0 41    41    140 490   980    .0082 - - - - 2 27     20     470   .62 0  
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c 0 79    79    190 1000   950    .0041 - - - - 2 26     16     570   .66 0  
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c 0 41    41    140 520   980    .0041 - - - - 2 22     13     470   .62 0  
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c 0 900    900    1000 11000   2500    .0041 - - - - 0 .021 .022 5.7 0    0  
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c 0 89    88    210 1100   980    0      - - - - 2 23     14     500   .62 0  
ldv-memsafety/StructInitialization1_true-valid-memsafety.c 0 .88 .64 66 8.7 31    0      - - - - 2 12     6.7   350   .66 0  
ldv-memsafety/StructInitialization2_true-valid-memsafety.c 0 .89 .63 65 11   31    0      - - - - 2 11     6.4   350   .66 0  
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c 0 .83 .57 67 8.3 31    0      - - - - 2 8.6   5.1   310   .66 0  
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c 0 .82 .55 67 8.8 26    0      - - - - 2 11     6.6   340   .62 0  
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c 0 .82 .55 66 8.4 31    0      - - - - 2 9.8   6.1   340   .66 0  
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c 0 11    11    69 180   1200    .025  - - - - 2 13     7.7   340   .62 0  
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c 0 46    45    67 670   2400    .045  - - - - 2 11     6.4   340   .66 0  
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c 0 46    45    69 470   2400    .045  - - - - 2 10     6.5   340   .62 0  
ldv-memsafety/memset_true-valid-memsafety_true-termination.c 0 .79 .55 66 12   26    0      - - - - 2 12     7.4   330   .66 0  
ldv-memsafety/memleaks_test14_3_false-valid-deref.i 0 .21 .21 35 2.3 .85 0      -32 4.9  2.7  250 0   0   0 12     7.6   280   .71 0   0 4.9  2.7  280 0     0    0 .57   .57   21    .025 0      -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i 0 .27 .27 35 3.3 1.0  0      -32 5.5  3.0  260 0   0   -32 10     6.2   340   .66 0   0 4.8  2.7  260 0     0    0 .57   .58   21    .025 0      -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i 0 .26 .25 35 3.1 1.0  0      -32 5.4  2.9  260 0   0   -32 10     6.1   340   .62 0   0 4.7  2.7  260 0     0    0 .65   .68   20    .025 0      -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i 0 2.4  2.4  55 31   1.0  0      -32 7.9  4.1  270 0   0   -32 19     11     410   .68 0   0 5.5  3.0  270 0     0    0 .59   .60   20    .029 0      -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i 0 2.4  2.4  54 29   .85 0      -32 6.7  3.6  270 0   0   -32 11     6.5   390   .66 0   0 5.4  3.0  260 0     0    0 .60   .62   20    .029 0      -
ldv-memsafety/memleaks_test11_1_false-valid-free.i -16 .52 .51 38 6.2 .85 0      -32 5.5  2.9  260 0   0   -32 11     6.2   350   .66 0   0 5.6  3.1  260 0     0    0 .60   .59   20    .025 0      -
ldv-memsafety/memleaks_test12_false-valid-free.i 0 570    570    1900 7100   1100    0      0 .67 .39 41 0   0   0 .020 .020 5.6 0    0   0 .93 .59 48 0     0    0 .0049 .0081 .53 0     0      -
ldv-memsafety/memleaks_test17_2_false-valid-free.i -16 30    30    130 350   300    .0041 -32 9.1  4.8  350 0   0   0 98     71     6600   1.6  0   0 6.3  3.5  330 0     0    0 .57   .57   21    .025 0      -
ldv-memsafety/memleaks_test19_false-valid-free.i -16 .20 .20 35 2.0 .85 0      1 6.2  3.3  250 0   0   -32 10     5.9   350   .62 0   0 5.2  3.0  280 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test1_false-valid-free.i -16 .17 .17 35 2.0 1.0  0      1 5.3  2.9  250 0   0   1 12     6.6   370   .62 0   0 5.1  3.0  280 0     0    0 .58   .58   20    .025 .033  -
ldv-memsafety/memleaks_test3_false-valid-free.i -16 .18 .18 35 1.7 1.0  0      1 4.5  2.5  250 0   0   1 10     6.1   340   .62 0   0 4.7  2.7  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test6_2_false-valid-free.i -16 .17 .17 35 1.9 1.0  0      1 5.3  2.8  260 0   0   1 13     7.2   440   .62 0   0 4.9  2.8  270 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test8_2_false-valid-free.i -16 .20 .19 35 1.9 1.0  0      1 6.0  3.2  250 0   0   1 13     7.8   410   .62 0   0 4.6  2.7  260 0     0    0 .63   .65   20    .025 0      -
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i 0 .39 .39 37 5.6 .85 0      -32 5.8  3.1  260 0   0   -32 10     6.1   350   .62 0   0 4.9  2.7  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i 0 .40 .40 37 5.1 1.0  0      -32 5.7  3.0  260 0   0   -32 10     5.7   350   .62 0   0 4.9  2.7  260 0     0    0 .57   .57   20    .025 .033  -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i 0 .17 .17 35 1.9 1.0  0      -32 6.0  3.2  260 0   0   -32 9.8   5.5   330   .62 0   0 4.6  2.6  250 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i 0 1.2  1.2  41 14   26    0      -32 6.1  3.3  250 0   0   -32 11     6.4   370   .62 0   0 4.7  2.6  260 0     0    0 .61   .60   20    .025 0      -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i 0 .16 .16 35 2.0 1.0  0      -32 6.0  3.3  260 0   0   0 12     7.0   290   .68 0   0 4.5  2.5  260 0     0    0 .60   .60   20    .025 0      -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i 0 1.1  1.1  42 16   31    0      0 3.2  1.8  200 0   0   0 12     7.4   290   .75 0   0 3.5  2.0  200 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i 0 .54 .54 43 6.8 1.0  0      -32 5.5  3.0  260 0   0   -32 11     5.9   370   .62 0   0 5.0  2.7  280 0     0    0 .61   .61   21    .029 .033  -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i 0 .16 .16 34 1.8 1.0  0      -32 4.8  2.6  250 0   0   -32 11     5.9   350   .62 0   0 4.5  2.6  250 0     0    0 .62   .62   20    .025 0      -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i 0 .16 .16 35 1.9 1.0  0      -32 5.3  2.9  250 0   0   -32 10     5.6   340   .62 0   0 4.4  2.5  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i 0 24    24    130 360   260    .0041 -32 7.1  3.8  320 0   0   -32 12     6.9   370   .62 0   0 6.8  3.7  290 0     0    0 .57   .57   21    .025 0      -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i 0 31    31    90 470   300    0      -32 7.7  4.1  300 0   0   -32 10     5.8   360   .66 0   0 6.3  3.4  270 0     0    0 .62   .62   21    .025 0      -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i 0 .18 .18 35 2.0 1.0  0      -32 8.7  4.5  410 0   0   -32 11     5.9   330   .62 0   0 9.6  5.1  410 0     0    0 .60   .60   20    .025 0      -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i 0 89    89    88 1200   260    0      -32 11    5.7  440 0   0   -32 11     6.0   350   .66 0   0 14    7.1  480 0     0    0 .57   .57   21    .025 0      -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i 0 24    24    49 350   300    .0041 0 95    69    2200 0   0   -32 11     6.2   360   .66 0   0 93    66    2200 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i 0 .16 .16 35 2.0 1.0  0      -32 4.5  2.4  260 0   0   -32 11     5.9   350   .66 0   0 4.2  2.4  250 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i 0 .17 .16 35 1.9 1.0  0      -32 4.7  2.6  250 0   0   -32 10     6.0   340   .62 0   0 4.4  2.5  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i 0 .16 .16 35 1.8 1.0  0      -32 4.5  2.5  250 0   0   -32 11     6.1   350   .66 0   0 4.3  2.4  260 0     0    0 .65   .66   20    .025 0      -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i 0 .22 .22 35 2.5 1.0  0      -32 5.3  2.9  260 0   0   -32 9.5   5.7   340   .62 0   0 4.9  2.7  280 0     0    0 .57   .57   21    .025 0      -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i 0 .17 .17 34 1.8 1.0  0      -32 5.9  3.2  260 0   0   -32 10     6.0   340   .62 0   0 4.5  2.5  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i 0 .22 .22 35 3.1 1.0  0      -32 6.5  3.5  260 0   0   -32 11     6.0   370   .62 0   0 4.8  2.7  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i 0 .17 .17 35 1.9 1.0  0      -32 4.9  2.7  260 0   0   -32 10     6.2   340   .62 0   0 4.6  2.6  260 0     0    0 .58   .60   20    .025 0      -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i 0 .16 .16 34 2.0 1.0  0      -32 4.9  2.7  250 0   0   -32 12     6.4   360   .62 0   0 4.3  2.4  260 0     0    0 .60   .60   20    .025 0      -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i 0 .18 .18 35 1.7 1.0  0      -32 4.8  2.6  250 0   0   -32 11     6.2   340   .62 0   0 4.3  2.4  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i 0 .16 .16 35 2.4 1.0  0      -32 6.2  3.3  260 0   0   -32 11     6.3   340   .62 0   0 4.7  2.6  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i 0 .19 .19 35 1.8 1.0  0      -32 6.2  3.3  260 0   0   -32 10     5.6   350   .62 0   0 4.4  2.5  260 0     0    0 .60   .60   20    .025 0      -
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i 0 .17 .17 35 2.0 1.0  0      -32 4.9  2.7  260 0   0   -32 11     6.5   350   .62 0   0 4.7  2.7  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i 0 .16 .16 35 1.9 1.0  0      -32 4.5  2.5  250 0   0   -32 10     6.1   340   .62 0   0 4.5  2.5  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i 0 .16 .16 35 1.8 1.0  0      -32 4.7  2.6  250 0   0   -32 10     6.0   340   .62 0   0 4.8  2.7  250 0     0    0 .59   .59   20    .025 0      -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i 0 .18 .17 35 2.0 1.0  0      -32 4.8  2.6  250 0   0   -32 9.6   5.8   330   .62 0   0 4.2  2.4  250 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i 2 1.8  1.8  39 27   26    0      - - - - 0 960     920     900   .70 0  
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i 2 1.8  1.8  40 24   31    0      - - - - 0 960     900     810   .69 0  
ldv-memsafety/memleaks_test12_true-valid-memsafety.i 0 560    560    1900 8000   1100    0      - - - - 0 .021 .022 5.6 0    0  
ldv-memsafety/memleaks_test13_true-valid-memsafety.i 2 14    14    290 160   31    0      - - - - 2 96     67     1100   .62 0  
ldv-memsafety/memleaks_test14_true-valid-memsafety.i 2 20    20    290 250   31    0      - - - - 0 12     7.0   290   .75 0  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i 2 7.1  7.0  49 80   31    0      - - - - 0 960     920     1300   .64 0  
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i 2 .42 .41 36 5.2 31    0      - - - - 2 20     11     520   .62 0  
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i 2 76    76    170 1100   300    .0041 - - - - 0 960     900     2200   .70 0  
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i 0 900    900    280 11000   370    0      - - - - 0 .021 .023 5.7 0    0  
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i 2 95    95    120 1400   300    0      - - - - 0 960     930     850   .63 0  
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i 2 .54 .53 36 6.8 31    0      - - - - 0 960     910     860   .69 0  
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i 2 .42 .42 36 4.8 31    0      - - - - 2 13     7.7   440   .62 0  
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i 2 .43 .42 36 5.2 31    0      - - - - 2 19     11     530   .66 0  
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i 2 .43 .42 36 5.3 31    0      - - - - 2 16     9.2   480   .66 0  
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i 2 .60 .59 36 8.3 31    0      - - - - 0 960     900     2600   .69 0  
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i 2 .73 .72 36 9.5 31    0      - - - - 0 960     890     2500   .68 0  
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i 2 .74 .74 36 9.9 31    0      - - - - 0 960     920     4000   .64 0  
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i 0 900    900    650 10000   120    0      - - - - 0 .021 .021 5.6 0    0  
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i 0 900    900    920 11000   120    0      - - - - 0 .021 .022 5.6 0    0  
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i 2 .42 .41 36 6.2 30    0      - - - - 2 13     8.0   460   .62 0  
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i 2 .48 .47 36 5.8 31    0      - - - - 2 33     24     540   .62 0  
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i 2 .43 .42 36 5.1 31    0      - - - - 2 15     8.9   530   .66 0  
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i 2 .44 .44 36 5.2 31    0      - - - - 2 24     14     570   .62 0  
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i 2 .45 .44 36 5.5 31    0      - - - - 2 23     13     500   .62 0  
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i 2 .43 .42 36 5.1 31    0      - - - - 2 14     8.0   460   .66 0  
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i 2 .43 .42 36 5.2 27    0      - - - - 2 16     9.1   470   .66 0  
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i 0 .84 .58 67 9.0 31    0      - - - - 0 11     6.6   290   .70 0  
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i 0 1.3  1.1  67 14   92    0      - - - - 0 9.6   6.0   280   .75 0  
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i 0 1.6  1.4  67 19   120    0      - - - - 0 11     6.2   290   .73 0  
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i 0 2.3  2.3  36 26   210    0      - - - - 0 10     5.6   290   .66 0  
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i 0 2.9  2.6  67 34   210    .0041 - - - - 0 9.9   5.8   280   .74 0  
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i 1 .15 .15 33 1.6 .85 0      1 4.7  2.5  240 0   0   0 10     5.6   290   .73 0   1 3.8  2.2  250 0     .54 1 .60   .62   20    .053 0      -
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i 0 1.2  1.2  35 15   120    0      -32 4.2  2.3  250 0   0   0 10     5.5   280   .70 0   0 3.6  2.1  250 0     0    -32 .59   .59   20    .053 0      -
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i 0 3.3  3.3  37 38   330    .0041 -32 3.5  1.9  240 0   0   0 10     5.9   280   .70 0   0 3.4  2.0  240 0     0    -32 .59   .59   20    .061 0      -
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i 1 2.5  2.4  36 28   240    .0041 -32 4.3  2.4  240 0   0   0 10     5.8   280   .67 0   0 3.5  2.0  240 0     0    1 .64   .64   20    .061 .0041 -
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i -16 1.2  1.2  36 14   100    .0041 1 4.6  2.5  240 0   0   0 10     6.0   280   .74 0   0 4.0  2.3  280 0     0    1 .60   .60   20    .053 0      -
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 180 -95 36000 36000 150000 430000 60000 .55   90 -1614 1400 960 46000 0   0   90 -1959 1000   630   35000 55    0   90 7 1700 1400 50000 1.5 4.6 90 -573 240   240   1700 4.2  7.4  90 58 17000 16000 44000 34 0  
    correct results 48 81 1900 1900 5100 25000 18000 .24   18 18 130 69 6100 0   0   9 9 90   53   3100 5.6  0   7 7 41 23 2100 0   4.6 19 19 12   12   390 1.3  5.7  29 58 580 370 14000 19 0  
        correct true 33 66 1600 1600 4300 21000 5200 .020  0 0 0 0 29 58 580 370 14000 19 0  
        correct false 15 15 300 300 740 4000 13000 .22   18 18 130 69 6100 0   0   9 9 90   53   3100 5.6  0   7 7 41 23 2100 0   4.6 19 19 12   12   390 1.3  5.7  0
    correct-unconfimed results 52 0 250 250 2300 3400 2600 .020  0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 52 0 250 250 2300 3400 2600 .020  0 0 0 0 0
    incorrect results 11 -176 34 34 480 390 450 .0082 51 -1632 310 170 15000 0   0   62 -1968 610   350   21000 39    0   0 21 -592 14   14   430 1.7  1.6  0
        incorrect true 0 51 -1632 310 170 15000 0   0   61 -1952 600   350   21000 39    0   0 16 -512 10   10   330 1.2  .55 0
        incorrect false 11 -176 34 34 480 390 450 .0082 0 1 -16 9.9 5.6 330 .62 0   0 5 -80 3.4 3.4 100 .51 1.1  0
score (180 tasks, max score: 270) -95 -1614 -1959 7 -573 58
Run set depthk.sv-comp19_prop-memsafety.MemSafety-Heap cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Heap