Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [apollon004; apollon069; apollon137; apollon154] 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-06 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap
Options -s kinduction -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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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 1 5.3   5.3   110 82    1.0  0   -32 15    7.9  860 0   0     -32 28     18     1900   .62 0   0 16    8.5  1000 0     0    1 .69   .69   22    .070 0      -
memsafety/test-0137_false-valid-deref.i 1 .13  .13  27 1.6  1.0  0   1 5.7  3.1  260 0   0     0 13     7.7   290   .71 0   0 92    76    2200 0     0    1 .67   .67   20    .11  0      -
memsafety/test-0235_false-valid-deref.i 1 .56  .56  33 7.9  .85 0   1 26    14    830 0   0     -32 10     5.8   330   .62 0   0 92    76    2200 0     0    1 .69   .69   21    .11  0      -
memsafety/960521-1_false-valid-free.i 1 5.3   5.2   110 69    1.0  0   -32 17    8.7  860 0   0     -32 59     46     4700   .62 0   0 17    9.0  930 0     0    1 .67   .66   22    .070 0      -
memsafety/test-0158_false-valid-free.i 1 .14  .14  27 1.6  .85 0   -32 4.6  2.6  250 0   0     1 11     6.5   330   .62 0   0 4.1  2.3  250 0     0    1 .65   .65   20    .070 0      -
memsafety/test-0232_false-valid-free.i 1 .30  .30  28 4.2  1.0  0   1 4.9  2.7  260 0   0     0 97     86     1000   2.0  0   0 92    80    2000 0     0    -32 .67   .67   20    .082 .025  -
memsafety/20020406-1_false-valid-memtrack.i 0 4.3   4.3   93 55    1.0  0   0 5.3  2.8  260 0   0     -32 13     7.2   360   .62 0   0 4.8  2.6  260 0     0    -32 .70   .70   20    .12  0      -
memsafety/20051113-1.c_false-valid-memtrack.i 0 .40  .40  27 5.3  1.0  0   -32 5.1  2.7  250 0   0     -32 9.5   5.3   310   .62 0   0 4.5  2.5  250 0     0    -32 .65   .65   21    .082 0      -
memsafety/lockfree-3.1_false-valid-memtrack.i 0 1.0   1.0   34 13    .85 0   0 96    75    2100 0   0     -32 8.2   4.6   310   .62 0   0 92    69    2200 0     0    -32 .66   .66   20    .090 0      -
memsafety/lockfree-3.2_false-valid-memtrack.i 0 .16  .16  27 1.6  1.0  0   0 98    73    2300 0   0     -32 8.7   4.8   310   .62 0   0 92    66    2600 0     0    -32 .65   .65   20    .090 0      -
memsafety/lockfree-3.3_false-valid-memtrack.i 0 4.9   4.9   74 59    1.0  0   0 96    73    2200 0   0     -32 8.9   5.2   310   .62 0   0 93    70    2200 0     0    -32 .66   .65   20    .090 0      -
memsafety/test-0019_false-valid-memtrack_true-termination.i 0 .13  .13  26 1.2  .85 0   0 2.9  1.6  200 0   0     -32 8.0   4.4   310   .62 0   0 3.3  1.8  200 0     0    -32 .64   .64   20    .074 0      -
memsafety/test-0102_false-valid-memtrack.i 0 49     49     190 560    .85 0   0 98    63    2800 0   0     0 12     6.5   290   .68 0   0 92    77    2200 0     0    -16 .72   .73   21    .098 .43   -
memsafety/test-0158_false-valid-memtrack_true-termination.i 0 .088 .088 27 1.1  1.0  0   -32 4.7  2.5  250 0   0     -32 7.6   4.2   300   .62 0   0 3.9  2.2  250 0     0    -32 .66   .66   20    .066 .025  -
memsafety/test-0220_false-valid-memtrack.i 0 68     68     460 730    1.0  0   0 98    67    3000 0   0     -32 8.5   5.3   320   .62 0   0 92    74    2300 0     0    -16 .67   .68   21    .090 0      -
memsafety/test-0232_false-valid-memtrack.i 0 .11  .11  26 1.2  .85 0   0 94    83    1700 0   0     -32 8.6   4.8   310   .62 0   0 97    86    1600 .88  0    -32 .65   .65   20    .082 0      -
memsafety/test-0234_false-valid-memtrack.i 0 .42  .42  33 5.3  .85 0   0 98    70    2300 0   0     -32 11     6.7   340   .62 0   0 92    75    2200 0     0    -16 .68   .68   21    .11  .033  -
memsafety/test-0235_false-valid-memtrack.i 0 .43  .43  33 5.6  1.0  0   0 97    73    2300 0   0     -32 10     6.2   330   .62 0   0 92    77    2200 0     0    -16 .69   .69   20    .11  0      -
memsafety/960521-1_true-valid-memsafety.i 0 900     900     13000 10000    .86 0   - - - - 0 .032 .032 5.5 0    0  
memsafety/lockfree-3.0_true-valid-memsafety.i 0 900     900     710 12000    .86 0   - - - - 0 .020 .021 5.6 0    0  
memsafety/test-0019_true-valid-memsafety_true-termination.i 2 .12  .12  26 1.8  .85 0   - - - - 2 24     15     640   .66 0  
memsafety/test-0102_true-valid-memsafety.i 0 900     900     2400 12000    .86 0   - - - - 0 .027 .028 5.6 0    0  
memsafety/test-0134_true-valid-memsafety.i 0 900     900     2600 9800    1.0  0   - - - - 0 .027 .028 5.6 0    0  
memsafety/test-0158_true-valid-memsafety_true-termination.i 2 .16  .16  26 2.0  .85 0   - - - - 2 14     7.9   340   .66 0  
memsafety/test-0214_true-valid-memsafety_false-termination.i 0 .36  .36  32 4.6  1.0  0   - - - - 0 .027 .028 5.6 0    0  
memsafety/test-0217_true-valid-memsafety_false-termination.i 0 .87  .87  82 10    1.0  0   - - - - 0 .021 .021 5.6 0    0  
memsafety/test-0218_true-valid-memsafety_false-termination.i 0 .45  .45  48 6.0  .85 0   - - - - 0 .021 .022 5.6 0    0  
memsafety/test-0219_true-valid-memsafety.i 0 900     900     2900 9700    .86 0   - - - - 0 .026 .026 5.6 0    0  
memsafety/test-0232_true-valid-memsafety.i 0 900     900     660 10000    .86 0   - - - - 0 .021 .022 5.6 0    0  
memsafety/test-0234_true-valid-memsafety.i 0 200     200     15000 2000    1.0  0   - - - - 0 .032 .032 5.6 0    0  
memsafety/test-0235_true-valid-memsafety.i 0 210     210     15000 2400    1.0  0   - - - - 0 .023 .024 5.6 0    0  
memsafety/test-0236_true-valid-memsafety.i 0 210     210     15000 2400    1.0  0   - - - - 0 .022 .023 5.6 0    0  
memsafety/test-0237_true-valid-memsafety.i 0 210     210     15000 3100    1.0  0   - - - - 0 .026 .027 5.6 0    0  
memsafety/test-0504_true-valid-memsafety.i 0 900     900     620 11000    1.0  0   - - - - 0 .024 .025 5.7 0    0  
memsafety/test-0513_true-valid-memsafety.i 0 900     900     930 11000    .86 0   - - - - 0 .027 .028 5.6 0    0  
memsafety/test-0521_true-valid-memsafety.i 0 900     900     1900 12000    1.0  0   - - - - 0 .025 .026 5.7 0    0  
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i 2 .65  .65  29 8.0  1.0  0   - - - - 0 960     870     820   .64 0  
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i 0 900     900     400 11000    1.0  0   - - - - 0 .021 .021 5.6 0    0  
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i 0 900     900     190 13000    .86 0   - - - - 0 .021 .023 5.7 0    0  
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i 0 900     900     250 11000    1.0  0   - - - - 0 .025 .025 5.6 0    0  
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i 0 900     900     800 11000    1.0  0   - - - - 0 .023 .024 5.6 0    0  
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i 0 900     900     1500 11000    1.0  0   - - - - 0 .024 .025 5.6 0    0  
memsafety-ext/tree_of_cslls_true-valid-memsafety.i 0 900     900     690 11000    1.0  0   - - - - 0 .026 .028 5.6 0    0  
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i 0 900     900     920 12000    .86 0   - - - - 0 .021 .023 5.7 0    0  
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i 0 900     900     580 11000    .86 0   - - - - 0 .022 .023 5.6 0    0  
memsafety-ext2/split_list_test05_false-valid-deref.i 0 99     98     15000 1100    1.0  0   0 .60 .37 40 0   0     0 .026 .027 5.5 0    0   0 .97 .62 47 0     0    0 .0044 .0055 .52 0     0      -
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i 0 900     900     1700 11000    1.0  0   0 .61 .37 42 0   0     0 .022 .023 5.6 0    0   0 .99 .65 49 0     0    0 .0047 .0057 .52 0     0      -
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i 0 900     900     4300 7500    1.0  0   0 .73 .44 40 0   0     0 .021 .022 5.6 0    0   0 1.0  .67 47 0     0    0 .0015 .0017 .40 0     0      -
memsafety-ext2/length_test03_false-valid-memtrack.i 0 3.1   3.1   45 41    1.0  0   0 94    74    1900 0   0     -32 10     5.8   310   .66 0   0 92    80    1700 0     0    -16 .68   .68   21    .098 0      -
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i 0 900     900     480 12000    .86 0   0 .61 .37 40 0   0     0 .022 .024 5.6 0    0   0 .94 .60 48 0     0    0 .0051 .0063 .67 0     0      -
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i 0 900     900     1900 8700    1.0  0   - - - - 0 .022 .023 5.7 0    0  
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i 0 900     900     4000 8700    .86 0   - - - - 0 .031 .032 5.7 0    0  
memsafety-ext2/length_test03_true-valid-memsafety.i 0 900     900     580 11000    1.0  0   - - - - 0 .027 .027 5.6 0    0  
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i 0 900     900     450 9900    .86 0   - - - - 0 .026 .028 5.6 0    0  
memsafety-ext2/split_list_test05_true-valid-memsafety.i 0 97     97     15000 1300    1.0  0   - - - - 0 .027 .028 5.7 0    0  
list-ext-properties/960521-1_1_false-valid-deref.i 1 .19  .19  27 2.3  .85 0   -32 20    10    1100 0   0     -32 10     5.6   320   .62 0   0 14    130    740 .082 0    1 .66   .67   20    .078 0      -
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 150     150     210 1900    .85 0   -32 18    9.7  690 0   0     0 97     69     1600   2.1  0   0 23    13    1200 0     0    1 .67   .67   21    .082 0      -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i -16 .26  .26  27 2.6  1.0  0   0 94    68    2400 0   0     -16 16     9.4   510   .66 0   0 92    65    2900 0     0    1 .68   .68   21    .082 0      -
list-ext-properties/960521-1_1_false-valid-free.i 1 .19  .19  27 2.5  .85 0   -32 24    12    1100 0   0     -32 9.8   5.7   330   .62 0   0 16    8.1  1100 0     0    1 .66   .65   20    .078 0      -
list-ext-properties/test-0158_1_false-valid-free.i 1 .14  .14  26 1.7  1.0  0   -32 5.8  3.1  270 0   0     1 9.8   5.5   320   .62 0   0 4.1  2.3  250 0     0    1 .65   .65   20    .074 0      -
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i 0 .10  .10  27 1.3  1.0  0   0 2.9  1.6  200 0   0     -32 9.7   5.8   310   .62 0   0 3.2  1.8  200 0     0    -32 .64   .64   20    .074 0      -
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i 0 .088 .088 26 1.1  1.0  0   -32 4.7  2.6  250 0   0     -32 7.8   4.4   310   .62 0   0 4.6  2.6  250 0     0    -32 .64   .65   20    .074 .13   -
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i 0 .10  .11  26 .92 1.0  0   -32 8.7  4.5  410 0   0     -32 9.1   5.0   310   .62 0   0 7.9  4.2  420 0     0    -32 .68   .67   20    .082 0      -
list-ext-properties/960521-1_1_true-valid-memsafety.i 2 6.2   6.1   37 77    .85 0   - - - - 0 960     940     820   .64 0  
list-ext-properties/list-ext_1_true-valid-memsafety.i 2 170     170     200 2500    .85 0   - - - - 0 960     850     2300   .70 0  
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i 2 51     51     120 610    .85 0   - - - - 0 960     880     2200   .63 0  
list-ext-properties/simple-ext_1_true-valid-memsafety.i 2 270     270     180 3400    1.0  0   - - - - 0 960     900     2100   .71 0  
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i 2 .13  .13  26 1.3  1.0  0   - - - - 2 43     29     600   .66 0  
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i 2 .15  .15  26 2.0  .85 0   - - - - 2 13     7.7   340   .66 0  
list-ext-properties/test-0214_1_true-valid-memsafety.i 0 .36  .36  27 4.5  1.0  0   - - - - 0 .023 .024 5.6 0    0  
list-ext-properties/test-0217_1_true-valid-memsafety.i 0 .51  .51  32 7.3  1.0  0   - - - - 0 .025 .027 5.6 0    0  
list-ext-properties/test-0232_1_true-valid-memsafety_true-termination.i 2 120     120     240 1800    .85 0   - - - - 0 960     910     1200   .70 0  
list-ext-properties/test-0504_1_true-valid-memsafety.i 2 270     270     190 3500    .85 0   - - - - 0 960     910     1100   1.5  0  
list-ext-properties/test-0513_1_true-valid-memsafety.i 2 18     18     210 210    1.0  0   - - - - 0 960     880     2100   .70 0  
memory-alloca/c.03-alloca_true-valid-memsafety.i 0 900     900     510 10000    .86 0   - - - - 0 .022 .023 5.6 0    0  
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c 1 .12  .12  26 1.4  .85 0   1 4.2  2.3  250 0   0     -32 12     6.5   330   .62 0   1 3.7  2.2  250 0     0    0 96      96      20    .066 0      -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c 1 .10  .10  26 .75 1.0  0   1 4.0  2.3  250 0   0     1 8.1   4.6   320   .62 0   1 3.6  2.2  250 0     0    0 96      96      20    .066 0      -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c 1 .081 .082 26 .79 1.0  0   1 4.6  2.5  250 0   0     1 7.6   4.4   310   .66 0   1 3.8  2.2  240 0     .13 -32 .59   .59   20    .061 0      -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c 1 .080 .081 26 .80 .85 0   1 3.4  1.9  240 0   0     1 7.9   4.7   320   .26 0   1 3.7  2.2  250 0     .13 -32 .61   .61   20    .061 0      -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c 1 1.7   1.7   38 26    .85 0   1 14    7.1  440 0   0     -32 15     9.1   410   .62 0   1 9.5  5.1  400 0     0    1 .60   .60   20    .061 0      -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c 1 1.7   1.7   37 25    1.0  0   1 12    6.3  550 0   0     -32 14     7.8   380   .62 0   1 9.8  5.3  470 0     0    1 .64   .63   20    .061 0      -
ldv-memsafety/memset2_false-valid-deref-write.c 1 1.3   1.3   41 17    .85 0   -32 3.9  2.2  240 0   0     -32 7.1   4.4   300   .62 0   0 3.3  1.9  250 0     0    1 .62   .62   20    .049 0      -
ldv-memsafety/memset3_false-valid-deref-write.c 1 14     14     340 220    .85 0   -32 3.7  2.1  240 0   0     -32 7.2   4.0   310   .62 0   0 3.4  2.0  240 0     0    1 .59   .59   20    .049 .0041 -
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c 1 1.3   1.3   41 21    1.0  0   -32 3.7  2.0  240 0   0     -32 8.0   4.8   300   .62 0   0 3.6  2.0  250 0     0    1 .59   .59   20    .049 0      -
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c 1 14     14     340 190    .85 0   -32 3.7  2.1  240 0   0     -32 6.6   3.8   300   .62 0   0 3.5  2.0  240 0     0    1 .60   .60   20    .049 .057  -
ldv-memsafety/memsetNonZero_false-valid-deref-write.c 1 14     14     340 210    1.0  0   -32 3.4  2.0  240 0   0     -32 6.8   3.8   310   .62 0   0 3.4  2.0  250 0     0    1 .59   .59   20    .049 0      -
ldv-memsafety/memset_false-valid-deref-write.c 1 14     14     340 190    .85 0   -32 4.0  2.3  240 0   0     -32 8.0   4.8   300   .62 0   0 3.5  2.0  240 0     0    1 .60   .60   20    .049 .78   -
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c 0 900     900     2300 11000    1.0  0   - - - - 0 .026 .027 5.6 0    0  
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c 2 .75  .75  27 9.5  .85 0   - - - - 2 32     23     590   .66 0  
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c 2 1.7   1.7   37 20    1.0  0   - - - - 2 28     17     500   .62 0  
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c 2 .78  .78  27 11    1.0  0   - - - - 2 20     12     470   .66 0  
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c 2 48     48     660 670    1.0  0   - - - - 2 23     14     560   .62 0  
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c 2 1.9   1.9   39 27    1.0  0   - - - - 2 28     17     500   .66 0  
ldv-memsafety/StructInitialization1_true-valid-memsafety.c 2 .11  .11  27 1.2  .85 0   - - - - 2 12     6.5   350   .66 0  
ldv-memsafety/StructInitialization2_true-valid-memsafety.c 2 .10  .10  27 1.3  .85 0   - - - - 2 13     7.2   350   .66 0  
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c 2 .085 .086 26 .97 .85 0   - - - - 2 8.4   4.5   310   .66 0  
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c 2 .084 .089 26 .96 1.0  0   - - - - 2 12     6.6   340   .66 0  
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c 2 .083 .084 26 1.0  1.0  0   - - - - 2 13     7.5   340   .66 0  
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c 2 1.4   1.4   42 17    1.0  0   - - - - 2 9.5   6.0   350   .62 0  
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c 2 15     15     350 190    1.0  0   - - - - 2 10     6.4   330   .66 0  
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c 2 15     15     350 220    1.0  0   - - - - 2 13     7.3   330   .62 0  
ldv-memsafety/memset_true-valid-memsafety_true-termination.c 2 .087 .087 26 .77 1.0  0   - - - - 2 10     5.9   340   .66 0  
ldv-memsafety/memleaks_test14_3_false-valid-deref.i 0 .14  .14  27 1.6  1.0  0   -32 5.5  3.0  250 0   0     0 13     7.8   290   .68 0   0 4.7  2.6  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i 0 .18  .18  27 2.1  1.0  0   -32 6.3  3.4  260 0   0     -32 11     6.4   350   .62 0   0 4.7  2.6  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i 0 .18  .18  27 2.7  1.0  0   -32 5.4  2.9  250 0   .033 -32 11     5.9   330   .62 0   0 4.9  2.7  260 0     0    0 .57   .57   20    .025 .033  -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i 0 2.4   2.4   47 30    1.0  0   -32 6.9  3.6  280 0   0     -32 20     12     400   .68 0   0 5.4  3.0  270 0     0    0 .57   .57   20    .029 0      -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i 0 2.3   2.3   47 33    1.0  0   -32 7.0  3.7  270 0   0     -32 14     7.9   380   .62 0   0 5.3  2.9  270 0     0    0 .58   .58   20    .029 0      -
ldv-memsafety/memleaks_test11_1_false-valid-free.i 0 .44  .44  30 6.1  1.0  0   -32 6.5  3.5  260 0   0     -32 12     6.6   350   .62 0   0 5.0  2.7  260 0     0    0 .57   .57   20    .025 .033  -
ldv-memsafety/memleaks_test12_false-valid-free.i 0 13     13     210 180    .85 0   0 .63 .40 41 0   0     0 .022 .024 5.6 0    0   0 .94 .60 48 0     0    0 .0049 .0061 .53 0     0      -
ldv-memsafety/memleaks_test17_2_false-valid-free.i 0 11     11     120 170    1.0  0   -32 7.9  4.2  350 0   0     0 97     86     760   .63 0   0 6.5  3.5  330 0     0    0 .57   .57   21    .025 0      -
ldv-memsafety/memleaks_test19_false-valid-free.i 1 .13  .13  27 1.6  .85 0   1 4.8  2.6  260 0   0     -32 11     6.3   370   .62 0   0 5.1  3.0  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test1_false-valid-free.i 1 .12  .12  27 1.0  1.0  0   1 4.8  2.6  250 0   0     1 12     7.4   380   .62 0   0 4.7  2.7  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test3_false-valid-free.i 1 .11  .11  27 .98 .85 0   1 5.0  2.7  250 0   0     1 11     6.3   360   .62 0   0 4.9  2.8  280 0     0    0 .58   .58   20    .025 .029  -
ldv-memsafety/memleaks_test6_2_false-valid-free.i 1 .12  .13  27 1.3  .85 0   1 5.8  3.1  250 0   0     1 15     8.3   430   .62 0   0 4.8  2.8  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test8_2_false-valid-free.i 1 .11  .11  28 .99 .85 0   1 5.6  3.0  250 0   0     1 14     7.6   420   .66 0   0 4.6  2.7  250 0     0    0 .58   .58   20    .025 .029  -
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i 0 .33  .33  29 4.3  1.0  0   -32 5.8  3.1  280 0   0     -32 11     6.2   370   .62 0   0 5.0  2.8  260 0     0    0 .59   .58   20    .025 0      -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i 0 .34  .34  29 4.2  .85 0   -32 6.4  3.4  260 0   0     -32 11     6.8   370   .62 0   0 5.0  2.8  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i 0 .10  .10  27 1.2  .85 0   -32 6.2  3.3  250 0   0     -32 11     6.1   320   .62 0   0 4.4  2.4  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i 0 .93  .93  37 12    .85 0   -32 5.3  2.9  260 0   0     -32 13     7.4   350   .62 0   0 4.7  2.6  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i 0 .13  .13  27 1.2  .85 0   -32 5.9  3.2  260 0   0     0 13     7.8   290   .71 0   0 4.4  2.5  260 0     0    0 .59   .59   20    .025 0      -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i 0 .83  .83  36 12    1.0  0   -32 5.5  3.0  250 0   0     0 14     8.1   300   .68 0   0 4.8  2.6  260 0     0    0 .57   .58   20    .025 0      -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i 0 .49  .49  34 6.5  1.0  0   -32 6.4  3.5  260 0   0     -32 12     6.6   380   .62 0   0 4.9  2.7  260 0     0    0 .58   .58   20    .029 0      -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i 0 .13  .13  27 1.0  1.0  0   -32 5.5  2.9  250 0   0     -32 11     6.3   360   .62 0   0 4.2  2.3  250 0     0    0 .59   .59   20    .025 0      -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i 0 .096 .096 27 1.1  1.0  0   -32 4.8  2.6  260 0   0     -32 10     6.2   340   .62 0   0 4.3  2.4  250 0     0    0 .59   .59   20    .025 0      -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i 0 9.6   9.6   120 120    .85 0   -32 7.3  3.8  320 0   0     -32 12     7.2   380   .62 0   0 6.5  3.5  290 0     0    0 .58   .58   21    .025 0      -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i 0 8.4   8.4   82 120    .85 0   -32 8.3  4.4  300 0   0     -32 11     6.8   380   .62 0   0 6.2  3.4  270 0     0    0 .59   .58   21    .025 0      -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i 0 .14  .14  27 1.3  1.0  0   -32 8.8  4.7  400 0   0     -32 11     6.8   360   .62 0   0 7.7  4.1  420 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i 0 27     27     83 330    1.0  0   -32 14    7.3  440 0   0     -32 11     6.4   350   .66 0   0 12    6.3  460 0     0    0 .57   .57   21    .025 0      -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i 0 6.3   6.3   36 77    .85 0   0 95    68    2200 0   0     -32 13     7.1   330   .66 0   0 93    68    2200 0     0    0 .60   .60   20    .025 0      -
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i 0 .097 .098 27 1.0  1.0  0   -32 5.7  3.1  250 0   0     -32 12     6.8   350   .66 0   0 4.2  2.4  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i 0 .094 .095 27 1.5  1.0  0   -32 6.1  3.3  250 0   0     -32 11     6.4   340   .62 0   0 4.3  2.4  260 0     0    0 .59   .59   20    .025 .033  -
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i 0 .096 .096 27 1.4  .85 0   -32 5.5  3.0  250 0   0     -32 11     6.1   330   .62 0   0 4.2  2.4  250 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i 0 .18  .18  27 2.0  1.0  0   -32 5.9  3.2  260 0   0     -32 11     6.1   340   .62 0   0 4.6  2.5  250 0     0    0 .58   .58   21    .025 .029  -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i 0 .11  .11  27 1.3  1.0  0   -32 5.0  2.7  250 0   0     -32 11     5.9   340   .62 0   0 4.6  2.6  250 0     0    0 .58   .58   20    .025 .029  -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i 0 .17  .17  27 1.9  .85 0   -32 5.7  3.0  260 0   0     -32 11     5.9   340   .62 0   0 4.8  2.6  260 0     0    0 .58   .58   21    .025 0      -
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i 0 .15  .15  27 1.3  1.0  0   -32 5.2  2.8  250 0   0     -32 11     6.6   340   .62 0   0 4.8  2.7  260 0     0    0 .60   .60   20    .025 0      -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i 0 .094 .095 27 1.3  1.0  0   -32 4.9  2.7  250 0   0     -32 11     6.7   350   .50 0   0 4.4  2.5  250 0     0    0 .59   .59   20    .025 0      -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i 0 .10  .10  27 1.1  .85 0   -32 5.2  2.8  260 0   0     -32 11     6.4   350   .62 0   0 4.4  2.5  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i 0 .099 .099 27 1.2  .85 0   -32 5.5  3.0  250 0   0     -32 12     6.4   360   .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 .099 .099 27 1.2  1.0  0   -32 5.4  2.9  260 0   0     -32 11     6.8   350   .66 0   0 4.8  2.7  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i 0 .10  .10  27 .96 1.0  0   -32 5.1  2.7  260 0   0     -32 12     6.8   350   .62 0   0 4.8  2.7  260 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i 0 .10  .10  27 1.1  .85 0   -32 5.4  2.9  250 0   0     -32 10     6.2   330   .66 0   0 4.4  2.4  250 0     0    0 .58   .58   20    .025 0      -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i 0 .10  .10  27 1.1  .85 0   -32 5.0  2.7  250 0   0     -32 11     6.7   340   .66 0   0 4.3  2.4  260 0     0    0 .57   .57   20    .025 0      -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i 0 .095 .097 27 1.1  1.0  0   -32 5.0  2.7  250 0   0     -32 12     6.6   340   .66 0   0 4.6  2.5  250 0     0    0 .59   .59   20    .025 0      -
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i 2 .80  .80  31 9.7  .85 0   - - - - 0 960     910     870   .69 0  
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i 2 .82  .82  31 11    1.0  0   - - - - 0 960     910     960   .69 0  
ldv-memsafety/memleaks_test12_true-valid-memsafety.i 0 15     15     190 210    .85 0   - - - - 0 .027 .028 5.5 0    0  
ldv-memsafety/memleaks_test13_true-valid-memsafety.i 2 1.4   1.4   36 23    1.0  0   - - - - 2 100     70     1100   .62 0  
ldv-memsafety/memleaks_test14_true-valid-memsafety.i 2 1.4   1.4   36 23    1.0  0   - - - - 0 14     8.5   300   .75 0  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i 2 3.4   3.4   40 42    1.0  0   - - - - 0 960     920     1200   .63 0  
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i 2 .10  .10  27 1.2  1.0  0   - - - - 2 16     9.1   520   .66 0  
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i 2 68     68     130 950    .85 0   - - - - 0 960     900     2000   .70 0  
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i 0 900     900     350 11000    1.0  0   - - - - 0 .028 .029 5.6 0    0  
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i 2 44     44     92 590    .85 0   - - - - 0 960     930     1100   .69 0  
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i 2 .15  .15  27 1.6  .85 0   - - - - 0 960     910     840   1.6  15  
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i 2 .11  .11  27 1.2  1.0  0   - - - - 2 13     7.4   440   .66 0  
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i 2 .12  .12  27 1.0  1.0  0   - - - - 2 18     10     480   .66 0  
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i 2 .10  .10  27 1.3  .85 0   - - - - 2 17     9.9   520   .66 0  
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i 2 .20  .20  27 2.4  1.0  0   - - - - 0 960     880     2700   1.6  0  
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i 2 .28  .28  27 2.6  .85 0   - - - - 0 960     890     2600   1.5  0  
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i 2 .28  .28  27 2.9  .85 0   - - - - 0 960     920     3700   1.7  0  
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i 0 900     900     1200 9700    .86 0   - - - - 0 .024 .026 5.6 0    0  
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i 0 900     900     640 13000    .86 0   - - - - 0 .022 .022 5.6 0    0  
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i 2 .11  .11  27 1.2  1.0  0   - - - - 2 15     8.7   460   .66 0  
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i 2 .14  .14  27 1.5  .85 0   - - - - 2 35     26     530   .66 0  
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i 2 .11  .11  27 1.2  1.0  0   - - - - 2 18     11     530   .66 0  
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i 2 .11  .11  27 1.3  1.0  0   - - - - 2 24     14     610   .62 0  
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i 2 .14  .15  27 1.4  .85 0   - - - - 2 26     15     550   .66 0  
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i 2 .10  .10  27 1.1  .85 0   - - - - 2 14     8.2   440   .66 0  
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i 2 .12  .12  27 1.0  1.0  0   - - - - 2 14     8.0   470   .66 0  
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i 2 .10  .10  26 .96 1.0  0   - - - - 0 12     7.1   270   .75 0  
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i 2 .16  .16  26 2.0  1.0  0   - - - - 0 10     6.0   280   .74 0  
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i 2 .17  .18  26 1.9  1.0  0   - - - - 0 10     5.5   280   .73 0  
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i 2 .23  .23  26 2.6  1.0  0   - - - - 0 12     7.1   280   .75 0  
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i 2 .27  .27  26 3.0  1.0  0   - - - - 0 10     5.9   280   .74 0  
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i 1 .11  .11  26 1.1  .85 0   1 3.8  2.1  240 0   0     0 11     6.2   300   .70 0   1 3.7  2.1  240 0     0    1 .60   .60   20    .053 0      -
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i 0 .16  .16  26 1.6  1.0  0   -32 4.1  2.3  250 0   0     0 11     5.9   290   .70 0   0 3.4  2.0  250 0     0    -32 .59   .59   20    .053 0      -
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i 0 .32  .32  26 3.6  1.0  0   -32 3.7  2.0  240 0   0     0 12     6.7   280   .67 0   0 3.6  2.0  250 0     0    -32 .59   .59   20    .061 .13   -
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i 1 .28  .28  26 3.3  1.0  0   -32 4.3  2.4  240 0   0     0 11     6.2   280   .74 0   0 3.7  2.1  270 0     0    1 .64   .64   20    .061 0      -
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i 1 .15  .15  26 1.6  .85 0   1 3.6  2.0  240 0   0     0 12     6.7   290   .67 0   0 4.4  2.6  250 0     0    1 .59   .59   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 120 29000    29000    150000 350000   170   0   90 -1744 1600 1100 49000 0   .033 90 -1991 1200 810   37000 56    0   90 7 1700 1400 54000 .97 .26 90 -571 240   240   1700 4.3  1.8  90 60 17000 16000 45000 40 15  
    correct results 83 136 1300    1300    6400 18000   77   0   16 16 110 60 5100 0   0     9 9 96 55   3200 5.3  0   7 7 38 21 2100 0    .26 21 21 13   13   430 1.4  .84 30 60 640 400 14000 19 0  
        correct true 53 106 1100    1100    3900 15000   50   0   0 0 0 0 30 60 640 400 14000 19 0  
        correct false 30 30 230    230    2500 3000   27   0   16 16 110 60 5100 0   0     9 9 96 55   3200 5.3  0   7 7 38 21 2100 0    .26 21 21 13   13   430 1.4  .84 0
    correct-unconfimed results 54 0 210    210    2600 2400   52   0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 54 0 210    210    2600 2400   52   0   0 0 0 0 0
    incorrect results 1 -16 .26 .26 27 2.6 1.0 0   55 -1760 380 200 18000 0   .033 63 -2000 740 440   27000 39    0   0 21 -592 14   14   430 1.8  .78 0
        incorrect true 0 55 -1760 380 200 18000 0   .033 62 -1984 720 430   27000 39    0   0 16 -512 10   10   330 1.2  .31 0
        incorrect false 1 -16 .26 .26 27 2.6 1.0 0   0 1 -16 16 9.4 510 .66 0   0 5 -80 3.4 3.5 100 .51 .47 0
score (180 tasks, max score: 270) 120 -1744 -1991 7 -571 60
Run set esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Heap